back to table · edit · history · where entries came from · files · download
5141 bytes, as of the version from 2026-11-10 22:01 (current). Recorded here, not run.
# T707: definition, normalization and bounded calculations
Checked definition: Báez-Duarte, math/0011254v1 §1.1 (1.4) and §1.2 (1.14):
B_N=sum_{n=1}^N mu(n)rho_n - N g_N rho_N, with rho_n(x)={1/(nx)} and
g_N=sum_{n=1}^N mu(n)/n. We tabulate E_N=||chi+B_N||^2 in
L^2((0,infinity),dx), chi=1_(0,1), N>=1. Ordinary fractional parts,
mu(1)=1, real natural logarithms, and no weighted measure or optimization.
The same paper calls the untapered sum S_n (1.18) and the dual sum F_n
(1.19); math/0202141v2 (1.1) calls the untapered sum F_n. Here F_N denotes
only the untapered sum. No numerical/asymptotic inference is needed to
establish this notation or definition.
Write w_n=mu(n) for n<N and w_N=mu(N)-N g_N. Then sum w_n/n=0 exactly.
For x>1 all rho_n=1/(nx), so B_N=0. For 1/N<x<1, put t=1/x<N:
B_N(x)=-sum_{n<=N}mu(n)floor(t/n)=-1. The last equality follows from
sum_{d|m}mu(d)=1 if m=1 and 0 otherwise, summed over m<=floor(t).
Thus the residual is supported, up to endpoints, on (0,1/N).
The squared norm equals its integral on that interval. No endpoint claim
at x=1 is required. This is a deduction from the source definition.
B_1=0, so E_1=1 exactly. B_2=rho_1-2rho_2. For t>1 its residual is
1 on [2m,2m+1), m>=1, and 0 on [2m-1,2m). Hence
E_2=sum_{m>=1}(1/(2m)-1/(2m+1))=1-log 2.
These provide a zero-approximant control and a nontrivial closed-form control.
The coefficients change at nonsquarefree endpoints too: N g_N and rho_N
both depend on the endpoint. No repeat rule, monotonicity or asymptotic decay
is asserted for this table.
Changing variables gives G_jk=A(j/k)/j, where
A(r)=integral_0^infinity {t}{rt}dt/t^2, and
b_n=(log n+1-gamma)/n. Indeed b_n=(1/n)integral_(1/n)^infinity {t}dt/t^2;
the portion below 1 gives log n and the remainder telescopes to 1-gamma.
Then E_N=1+2 sum w_n b_n+sum w_j w_k G_jk. Setting c_n=-w_n in the
unrestricted minimum of T641 proves E_N>=d_N^2 for every N, independently
of numerical checks of the stored prefix.
BBLS math/0306251v1 §4 and §9, Propositions 87 and 89, were inspected:
A(p/q)=((1-p/q)log(p/q)+(1+p/q)C)/2
-pi(V(p,q)+V(q,p))/(2q), C=log(2pi)-gamma,
V(p,q)=sum_{m=1}^{q-1}{mp/q}cot(pi m/q), V(p,1)=0.
The generator's gram_system is reused from T706/T641 (source hash in its
docstring). Each required kernel is freshly enclosed with Arb from exact
rational arguments. The cotangent inputs avoid poles. All arithmetic,
including cancellation in the quadratic form, propagates ball errors.
## Separate period-integral calculation
For coprime positive p,q, t=q(n+u) yields
A(p/q)=(1/q)integral_0^1 {qu}{pu} sum_{n>=0}(n+u)^(-2)du.
Split at i/q and j/p. The numerator is an exact quadratic
P(u)=alpha*u^2+beta*u+delta. Integrate P(u)/(n+u)^2 by the antiderivative
alpha*(n+u)+(beta-2alpha*n)log(n+u)
-(alpha*n^2-beta*n+delta)/(n+u).
The apparent singularity for n=u=0 is removable: beta=delta=0 there.
Integrate n=0,...,15 directly. For n>=K=16 expand
(n+u)^(-2)=sum_{m=0}^M(-1)^m(m+1)u^m/n^(m+2)+remainder, M=125.
Moments are exact rationals; summed coefficients are Arb enclosures of
Hurwitz zeta(m+2,K). Terms decrease uniformly on 0<=u<=1. Since 0<=P<=1,
the integrated remainder is at most
(M+2)/K^(M+3)+1/K^(M+2), before division by q, by the first omitted term
and the integral bound for the positive zeta tail. That explicit bound is
added to the ball. This route uses no cotangent sums. Its implementation,
reused from T641 with original hash in integral_kernel.py, is checked here
against the derivation; inherited conclusions or sibling decimal values are
not independent evidence. Both routes share Arb and the mathematical kernel.
checks.py recomputes all 465 symmetric Gram entries and every E_N. Its Möbius
function uses separate trial division. Its endpoint weight is independently
formed as -N sum_{n<N}mu(n)/n, eliminating mu(N) algebraically.
For N=1,2,3,4,6, it also directly integrates the whole residual in t=1/x,
with period L=lcm(1,...,N). Since sum w_n/n=0 the residual is piecewise
constant. Its squared values are rational. Integrate [1,L] directly and
all later periods with the bounded expansion above, multiplying the remainder
by (1+sum|w_n|)^2/L. This avoids both the cotangent kernel and b_n formula.
Known answers for nonzero elementary integrals, A(1), E_1, E_2 and wrong-value,
wide-ball and NaN controls exercise the checker. All 30 lower bounds are
also independently recomputed by enclosed elimination on the integral Gram
matrix. Exact cancellation and sample interior residual identities are checked.
Checkpoints preserve exact rational endpoints, computation versions and code
hashes. Post-upload checks compare both routes with the full stored intervals,
not only midpoints. For exact E_1, mathematical proof supplies exactness;
the direct integral enclosure must contain 1 and be narrow. Generator verify
is a separate reproducibility check. These checks are build evidence; only
an independent critic can issue the scientific and argument-selection verdicts.
Instructions: skill-manifest.json records the archived matching core/reference
bundle d6661c2f21613524889fa3a57d3c95f8330344ca62e5a856211c08a282b7dbab.