back to table · edit · history · where entries came from · files · download
5085 bytes, as of the version from 2026-11-10 20:59 (current). Recorded here, not run.
# Vasyunin squared approximation errors: definition and checks
Put rho_a(x)={1/(a x)}, chi=1_(0,1), mu(1)=1, g_N=sum mu(n)/n,
F_N=sum mu(n)rho_n, and V_N=F_N-g_N rho_1. Store
E_N=integral_0^infinity |chi(x)+V_N(x)|² dx, N=1,2,... .
The measure is dx, signs are retained, and the output is squared. There are
no complex branches or assumptions about RH. Logs are natural. This is
math/0011254v1 (1.17), with (1.4) defining g. Its (1.18) calls our F_N S_n;
math/0202141v2 (1.1) calls it F_n. The first paper's F_n is instead dual.
## Generator formula
Exact rational coefficients are w_1=1-g_N and w_n=mu(n), 2<=n<=N.
They satisfy sum w_n/n=0. Thus V_N(x)=0 for x>1.
For nonsquarefree N>=2, mu(N)=0 leaves both F_N and g_N unchanged, so
E_N=E_(N-1). These are algebraic facts, not deductions from matching decimals.
Substitution t=1/(j x) gives G_jk=<rho_j,rho_k>=A(j/k)/j,
where A(lambda)=integral_0^infinity {t}{lambda t} dt/t².
Also b_n=<chi,rho_n>=(log n+1-gamma)/n, splitting the integral at t=1.
Then E_N=1+2 sum w_n b_n+sum w_j w_k G_jk.
The finite formula is BBLS math/0306251v1 Proposition 89:
A(p/q)=((1-p/q)log(p/q)+(1+p/q)(log(2pi)-gamma))/2
-pi(V(p,q)+V(q,p))/(2q), gcd(p,q)=1,
V(p,q)=sum_{m=1}^{q-1}{mp/q}cot(pi m/q), with V(p,1)=0.
These cotangent sums are auxiliary and are not the approximation V_N.
The generator recomputes all ingredients; no companion decimal is an input.
Arb balls enclose rational coercions and every log, cotangent, and arithmetic
operation at numberdb.bits(100,losing=128)=461 bits. Output radii and accuracy
are measured, not inferred merely from working precision.
## Independent integral kernel and explicit remainder
Splitting the defining A integral into periods t=q(m+u) gives
A(p/q)=1/q integral_0^1 {qu}{pu} sum_{m>=0}(m+u)^(-2) du.
On consecutive cuts i/p and j/q the fractional-part product is an exact
quadratic P(u), 0<=P(u)<=1. Integrate m=0,...,15 analytically. At u=0
its apparent singularity cancels because P(u)=pq u² there.
For m>=K=16 expand (m+u)^(-2) in powers u^r, r=0,...,M=125.
Exact rational moments of P multiply (-1)^r(r+1) zeta(r+2,K), evaluated
by Arb Hurwitz zeta at 720 bits. Alternating terms decrease for 0<=u<=1,
so the omitted contribution before division by q is at most
(M+2) zeta(M+3,K) <= (M+2)/K^(M+3)+1/K^(M+2).
This positive bound is explicitly added to the ball. There is no uncontrolled
quadrature. checks.py freshly checks all 465 symmetric Gram entries, all 30
norms, their positivity, and lower bounds from separately solved Gram systems.
Shared target inner products b_n and the defining convention are common to
both routes; small whole-residual integrals check this remaining common part.
## Whole-residual and known-answer controls
With t=1/x and L=lcm(1,...,N), sum w_n{t/n} is L-periodic.
Since sum w_n/n=0 it equals -sum w_n floor(t/n), constant between jumps.
Split at all k n/L in u=t/L. The t>=1 integral consists of the m=0
period restricted to u>=1/L and all complete periods m>=1. Integrate the
piecewise constant squared residual by the same rational antiderivative;
use the preceding tail bound multiplied by (1+sum |w_n|)²/L.
This bypasses both the cotangent kernel and the b_n formula.
Executed cases: N=1,2,3,4,6. Separate trial division computes mu.
V_1=0, so E_1=1 exactly. For N=2, V_2=.5 rho_1-rho_2 is zero on
2m<t<2m+1 and -1/2 on 2m+1<t<2m+2. The even-interval contribution
is 1-log2 and the odd contribution is log2/4, giving E_2=1-3log2/4.
Finite, narrow-ball comparisons are tested by known integrals 1 and
3/2-2log2, A(1)=log(2pi)-gamma, and E_1,E_2. Deliberate 10^-80
perturbation, radius-one, and NaN controls must fail.
Expanding ||chi+F_N-g_N rho_1||² gives
E_N=U_N-2g_N(b_1+sum mu(n)G_1n)+g_N²G_11.
The checker calculates this separately for all selected N. Because V_N is
in span(rho_1,...,rho_N), E_N>=d_N² by the definition of the minimum,
using coefficients c=-w; numerical checks are corroboration, not a proof
of a universal bound or of any asymptotic claim.
## Evidence and reproducibility
Run `sage -python checks.py > check-output.log`, beside generate.py,
integral_kernel.py, and skill-manifest.json. The FINAL_EVIDENCE_BEGIN marker
precedes the JSON result; prior JSON lines checkpoint each Gram row.
Every endpoint is serialized with RealNumber.exact_rational(), preserving
its binary endpoint exactly. Native Sage Integer/Rational types are checked.
After upload, verify_stored.py checks the entire stored decimal interval
against both saved enclosures using exact fractions; exact E_1 is checked
separately. It also rejects an altered stored last-place value. Generator
verify(sample=None) is an additional reproducibility check only.
The archived skill manifest is ../20261110T205245Z-build-skills/manifest.json,
attached as skill-manifest.json. The matching bundle hash is
d6661c2f21613524889fa3a57d3c95f8330344ca62e5a856211c08a282b7dbab.
These are build checks, not the independent scientific verdict required before
any review offer. A fresh critic must examine the exact live revision and
selection-relevant sources.