back to table · edit · history · where entries came from · files · download
5867 bytes, as of the version from 2026-10-31 22:58 (current). Recorded here, not run.
# Definitions and independent checks for T642
Use {t}=t-floor(t), natural logarithms, positive pi,
chi=1_(0,1), rho_n(x)={1/(nx)}, and the measure dx on (0,infinity).
Set w_(N,n)=mu(n)(1-log(n)/log(N)). The source defines S_N=sum w_(N,n) rho_n
as an approximation to -chi, so E_N=||chi+S_N||^2 has a plus sign.
N>=2; w_(N,1)=1 and w_(N,N)=0 exactly. Vanishing Möbius coefficients are
handled exactly, not inferred from rounded digits. No rational closed form
for any complete E_N in this range is asserted.
## Gram matrix and target inner products
Substitute t=1/(jx), dx=-dt/(j t^2), to get
G_jk=<rho_j,rho_k>=A(j/k)/j, where
A(lambda)=integral_0^infinity {t}{lambda*t} dt/t^2.
For b_n=<chi,rho_n>, the same substitution gives
b_n=(1/n) integral_(1/n)^infinity {t} dt/t^2.
The part from 1/n to 1 is log(n). On each interval [m,m+1],
the other integral is log((m+1)/m)-1/(m+1). Summing through m=M
and taking the defining limit of Euler's constant gives 1-gamma.
Thus b_n=(log(n)+1-gamma)/n.
The checker also tests the finite partial sum with the rigorous remainder
bound 0 <= integral_(M+1)^infinity {t}/t^2 dt <= 1/(M+1).
Expanding the norm gives E_N=1+2 w^T b+w^T G w. At N=2,
w=(1,0); BBLS Proposition 87 gives G_11=log(2*pi)-gamma, hence
E_2=3+log(2*pi)-3*gamma. This nonzero closed form and the opposite-sign
residual are positive and negative controls, respectively.
The generator evaluates A(p/q), gcd(p,q)=1, using BBLS Proposition 89:
A(p/q) = (1-p/q)log(p/q)/2 + (1+p/q)(log(2*pi)-gamma)/2
- pi*(V(p,q)+V(q,p))/(2q),
V(p,q) = sum_(1<=m<q) ((mp mod q)/q) cot(pi*m/q).
An empty sum at denominator 1 is zero. All rational arguments are exact,
and Arb encloses their conversion and subsequent arithmetic. The generator
uses 461 working bits for 100 decimal digits. Its guard is measured in the
attached evidence, not used as a substitute for an error bound.
## Independent integral computation
Write j=dp, k=dq with d=gcd(j,k) and gcd(p,q)=1. The period of
{t/j}{t/k} is l=dpq. Substitute t=l*u and split the integral over
successive periods. Nonnegativity permits exchanging sum and integral:
G_jk = (1/(dpq)) integral_0^1 {pu}{qu} psi_1(u) du,
psi_1(u) = sum_(n>=0) (n+u)^(-2).
The rational breakpoints are all a/p and b/q in [0,1]. On each interval
P(u)={pu}{qu}=a*u^2+b*u+c with exact integer coefficients determined by
the two floors. For n=0,...,K-1, K=16, integrate exactly using
a*(v-u) +(b-2an)*log((v+n)/(u+n))
+(a*n^2-b*n+c)*(1/(u+n)-1/(v+n)).
The interval beginning at 0 has b=c=0. Its n=0 contribution is a*(v-u),
so no infinite or undefined intermediate value is needed.
For n>=K, expand (n+u)^(-2) as
sum_(m=0)^(M-1) (-1)^m(m+1)u^m n^(-m-2), with M=112.
For 0<=u<=1 the alternating terms decrease, so the remainder's absolute
value is at most (M+1)u^M n^(-M-2). Since 0<=P(u)<=1, integrating
and summing bounds the omitted contribution by
sum_(n>=K) n^(-M-2) <= K^(-M-2)+K^(-M-1)/(M+1).
The checker adds this bound as an Arb radius before scaling by 1/(dpq).
It evaluates the finite coefficients as
(-1)^m(m+1)*(zeta(m+2)-sum_(1<=n<K) n^(-m-2)).
This subtraction is enclosed at 640 bits; cancellation reduces precision
but cannot invalidate the bound. All polynomial moments are integrated
analytically. The path contains no cotangent sum, no imported companion
rounded value, and no uncontrolled numerical quadrature.
The known G_11 value is checked before other comparisons, and a 1/100
perturbation must be rejected. Every comparison first requires finite balls
of radius less than 10^-110. All 900 ordered Gram entries are compared;
there are 465 symmetric entries and repeated reduced ratios are cached.
## Least-squares comparison and stored digits
Independent ball Gaussian elimination solves G_N*c=b for every N=2,...,30.
Each pivot must be strictly positive, and d_N^2=1-b^T*c must be positive.
The geometric inequality d_N^2 <= E_N follows by choosing c=-w in the
minimum. Orthogonality gives the stronger identity
E_N-d_N^2 = (w+c)^T G_N (w+c).
The checker verifies this identity with narrow balls and obtains strict
positivity on the computed range. It compares each independently computed
minimum with the live T641 last-place interval, without using T641 as input
to the calculation. A bound on E_N or a conditional asymptotic is not
assumed. Positive definiteness of the finite Gram matrix also follows
from linear independence: a relation among the rho_n, after x -> 1/t,
has jumps at each integer m with coefficients sum_(n|m) c_n; triangular
induction on m=1,...,N makes every c_n zero.
A displayed decimal denotes its centre plus or minus one unit in the final
place. Both independent and generator balls must lie strictly inside that
interval, not merely overlap it. After the draft is filled, the same
comparisons use the live stored strings; perturbations of ten final-place
units must fail. The stored E_N interval must lie entirely above the stored
d_N^2 interval, and the stored order must be exactly N=2,...,30.
`verify(sample=None)` is run separately as the package's reproducibility check.
## Sources and policy
Báez-Duarte, arXiv:math/0202141v2, §1, explicitly names and defines S_N.
Báez-Duarte–Balazard–Landreau–Saias, arXiv:math/0306251, §9,
Propositions 87 and 89 supply A(1) and the finite rational-dilation formula.
Bettin–Conrey, arXiv:1111.0931v2, §2, equation (13), supplies the Vasyunin
formula and its role in the approximation problem.
Bettin–Conrey–Farmer, arXiv:1211.5191, §1, defines the same tapered V_N.
Their conditional asymptotic theorem is not required for any finite value.
The source downloads and SHA-256 hashes are in sources.json.
The controlling archived skill manifest is
`agents/runs/20261031T225043Z-build-skills/manifest.json`.
Both archived versions have SHA-256
`a2b28d9953264d7b0ca62663785c2952190c5be6d6d3597fd695d9a54d606278`.