back to table · edit · history · where entries came from · files · download
3018 bytes, as of the version from 2026-10-31 20:52 (current). Recorded here, not run.
# Conventions and independent integration for T640
The archived policy manifest is
`agents/runs/20261031T203213Z-build-skills/manifest.json`; the matching local/live
SHA-256 is `a2b28d9953264d7b0ca62663785c2952190c5be6d6d3597fd695d9a54d606278`.
A(λ) = ∫₀∞ {t}{λt} dt/t² uses ordinary fractional parts and λ>0.
For λ=p/q in lowest terms, substitution t=q(n+u), n≥0, 0≤u≤1, gives
A(p/q) = (1/q) ∫₀¹ f(u) ψ'(u) du,
f(u) = {qu}{pu}, ψ'(u) = Σ_{n≥0} (n+u)^(-2).
Tonelli applies to the nonnegative summands. At u=0, f(u)=pq*u² in a
neighborhood, so the n=0 term has a removable singularity. Break at every
j/q and k/p. On each open subinterval f(u)=a*u²+b*u+c, with exact rational
endpoints and integer coefficients obtained from the constant floors.
The independent checker integrates n=0,...,15 analytically. For n≥0,
put B=b−2an and D=an²−bn+c. An antiderivative is
a*u + B*log(n+u) − D/(n+u).
At the first endpoint u=0,n=0, B=D=0 and the primitive is simply a*u.
No quadrature rule evaluates across a fractional-part jump.
For the remaining n≥M=16 terms, use the uniformly convergent expansion
Σ_{n≥M} (n+u)^(-2)
= Σ_{r≥0} (-1)^r (r+1) ζ(r+2,M) u^r.
The checker integrates the polynomial through r=L=100. The moments
∫₀¹ f(u)u^r du are exact rationals. For 0≤u≤1 each n-series is alternating
with decreasing term magnitude. Its tail after r=L has absolute value at
most (L+2)*u^(L+1)*n^(-L-3). Since 0≤f≤1, the omitted contribution to A
is bounded by
(L+2)/q * Σ_{n≥M} n^(-L-3)
≤ ((L+2)*M^(-L-3) + M^(-L-2))/q.
The last inequality is the integral bound for a positive decreasing series.
This explicit exact rational bound is added as a ball radius. Elementary
logarithms and Hurwitz zeta are evaluated by Arb at 512 bits. The checker
therefore has its own rigorous enclosure, obtained without Vasyunin sums,
cotangents, Euler's constant, or the rational closed form used by the generator.
The integration primitive is first tested on ∫₀¹(1+u)^(-2)du=1/2 and on
∫₀¹u²/u² du=1. The full period integration at p=q=1 is tested against
log(2π)−γ (BBLS, Proposition 87). Bounds must be finite and narrow, and a
perturbation of 10^(-90) must fail agreement. Checks compare every selected
input and then verify the actual stored intervals after filling.
For the family's Hilbert-space convention, t=1/(j*x) gives
G_jk=⟨rho_j,rho_k⟩=A(j/k)/j with rho_n(x)={1/(n*x)}. This also implies
G_jk=G_kj using A(λ)=λA(1/λ). With chi=1_(0,1), the same substitution gives
b_n = ⟨chi,rho_n⟩ = (1/n) ∫_{1/n}∞ {t} dt/t²
= (log n + 1 − γ)/n.
Indeed, ∫_{1/n}¹ dt/t=log n. Splitting [1,M] at integers gives
∫₁ᴹ {t}dt/t² = log M − H_M + 1, which tends to 1−γ.
The endpoint convention for chi does not change an integral. These derivations
fix the scale for later family tables; neither Gram entries nor target inner
products are added as extra quantities to this table.