back to table · edit · history · where entries came from · files · download
5679 bytes, as of the version from 2026-10-31 21:13 (current). Recorded here, not run.
# Definition, kernel and certificates for T641
Write rho_n(x) = {1/(n x)}, chi(x) = 1_(0,1)(x), and use Lebesgue measure dx
on the entire positive half-line. All fractional parts are ordinary fractional
parts, all logarithms are natural, and pi is positive. Endpoint values on a
countable set do not affect any integral. There is no anchoring, constraint on
the coefficients, or normalization of the rho_n.
## The target vector and Gram matrix
With t = 1/(j x),
G_jk = integral_0^infinity rho_j(x) rho_k(x) dx = A(j/k)/j,
A(lambda) = integral_0^infinity {t}{lambda t} dt/t^2.
With t = 1/(n x),
b_n = (1/n) integral_(1/n)^infinity {t} dt/t^2.
The portion from 1/n to 1 is log n. On [m,m+1], m >= 1, the integral is
log((m+1)/m)-1/(m+1). Summing through m=L gives
log(L+1)-H_(L+1)+1, which tends to 1-gamma. Hence
b_n = (log n+1-gamma)/n, and ||chi||^2 = 1.
The basis is linearly independent for every finite N. After t=1/x, a linear
combination of {t/n} that vanishes almost everywhere must have zero jumps at
t=1,...,N. The jump at integer k is minus the sum of c_n for n dividing k.
Induction gives c_1=...=c_N=0. Thus G is positive definite and the unique
optimal vector satisfies G c = b. The squared minimum is 1-b^T G^(-1)b.
For a reduced positive ratio p/q, BBLS Proposition 89 gives
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_(m=1)^(q-1) ((m p mod q)/q) cot(pi m/q), V(p,1)=0.
This is the generator's kernel. All arguments are exact rationals embedded in
Arb balls, and every cotangent and logarithm is enclosed. Reduction of j/k is
performed before the finite sums. Stored companion decimals are never inputs.
## Enclosed minimization
For G=L D L^T with unit lower triangular L, let y=L^(-1)b. All leading
principal minima follow at once:
d_N^2 = 1 - sum_(i=1)^N y_i^2 / D_i.
The scalar recurrences use only ball addition, multiplication and division;
every D_i must be strictly positive before division. Induction on elimination
steps then proves each computed ball contains its exact counterpart. This is
a direct enclosure, not a point solve followed by an asserted error interval.
The generator uses 589 working bits at its default 100 decimal digits.
The attached evidence reports the smallest accuracy and largest propagated
radius actually observed. Coefficients come from solving L^T c = D^(-1)y
for each prefix. Every normal-equation residual contains zero within the
reported small bound. Every quadratic norm 1-2 b^T c+c^T G c agrees with its
minimum. Successive differences agree with y_N^2/D_N.
## Independent integral kernel
For p,q coprime and positive, splitting into periods of length q gives
A(p/q) = (1/q) integral_0^1 f(u) psi'(u) du,
f(u) = {q u}{p u}, psi'(u) = sum_(n=0)^infinity (n+u)^(-2).
On intervals between consecutive points i/q and j/p, f is the exact
quadratic alpha u^2+beta u+delta. The first K=16 terms of psi' are integrated
analytically. For v=n+u an antiderivative is
alpha v + (beta-2 alpha n) log v
- (alpha n^2-beta n+delta)/v.
At n=0, u=0, the initial segment has beta=delta=0 and integrand alpha;
this removable endpoint is handled exactly rather than by singular quadrature.
For n>=K, expand
(n+u)^(-2) = sum_(m=0)^M (-1)^m (m+1) u^m n^(-m-2) + remainder.
Summation over n gives coefficients (-1)^m (m+1) zeta(m+2,K). Each moment
of f(u) u^m is evaluated with exact rational arithmetic. For 0<=u<=1 and
n>=16 the series is alternating with decreasing term magnitudes. The pointwise
remainder is at most (M+2) u^(M+1) zeta(M+3,K). Since 0<=f<=1, a valid
absolute bound for the integral error before division by q is
(M+2)/K^(M+3) + 1/K^(M+2).
Here M=125, and this positive exact rational bound is explicitly added to the
computed ball. The 720-bit checker therefore produces rigorous enclosures
without sharing the finite cotangent representation. Known-answer controls are
run before using this method: integral u^2/u^2 = 1,
integral u^2/(1+u)^2 = 3/2-2 log 2, and A(1)=log(2 pi)-gamma. A deliberately
perturbed control must be rejected. These checks guard both endpoint handling
and false agreement of wide or nonfinite balls.
Every symmetric Gram entry through N=30 is checked against this independent
kernel. Each prefix is solved independently by Gaussian elimination. A diagonal
system with a known nonzero solution controls the solver. The coefficient
vectors and all 30 minima must agree as finite, narrow balls. This checks both
the kernel formula and the minimization implementation.
## One-dimensional value, order and conventions
The base case is d_1^2 = 1-(1-gamma)^2/(log(2 pi)-gamma). A separate explicit
2 by 2 inverse also checks N=2. Nested spaces imply nonincreasing minima.
The computations certify positivity and strict decreases throughout N=1,...,30;
strictness is not assumed from apparent decimal differences.
The Mellin transforms are chi-hat(s)=1/s and
rho_n-hat(s)=-zeta(s)/(s n^s) for 0<Re(s)<1. Hence the residual chi-sum c_n rho_n
has Mellin transform (1+zeta(s) sum c_n n^(-s))/s. The commonly published
Dirichlet polynomial uses a_n=-c_n and residual 1-zeta(s) sum a_n n^(-s).
This sign change is a coefficient convention, and leaves the minimum unchanged.
No Riemann-hypothesis assumption is used for any finite computation here.
After filling, checks.py interprets every stored decimal by its exact last-place
interval and requires that interval to contain both independently computed
balls strictly. It also checks the order and strict monotonicity of the stored
intervals. Generator.verify(sample=None) is an additional round-trip check.