back to table · edit · history · where entries came from · files · download
4903 bytes, as of the version from 2026-10-30 19:31 (current). Recorded here, not run.
# Root and energy enclosure certificate for T628
The root proof and polynomial algorithm are adapted from the public T627
attachments, read from the database during this build. Their downloaded
bytes and the checked AKM source are identified in source-hashes.json.
The root certificates and all numerical checks were executed anew.
Put x=xi>0, l=2k+2 and a(x)=atan(1/x). Set p_0=1, p_1=x, r_0=0,
r_1=1, and use the exact QQ[x] recurrence
(n+1) v_(n+1) = (2n+1) x v_n + n v_(n-1).
For even l define q_l=p_l a-r_l. The generator verifies exactly
(1+x^2)(r_l p_l' - r_l' p_l) - p_l^2 = -1.
Thus (q_l/p_l)'=-1/((1+x^2)p_l^2). The polynomial p_l has nonnegative
coefficients and positive constant coefficient, so it never vanishes on
x>=0. Also r_l/p_l and a tend to zero at infinity. Integration identifies
q_l with AKM's defining real oblate integral, without a complex branch choice.
Using p_2=(1+3x^2)/2 and q_2=p_2 a-3x/2, AKM (3) is equivalent to
H(x)=a(x)-B(x)/A(x)=0,
A=p_l^2+x^2, B=p_l r_l+x.
The positive denominator of H' is (1+x^2)A^2. Its numerator
N=(1+x^2)(B A'-B' A)-A^2
has a negative constant coefficient, nonnegative other coefficients and a
positive leading coefficient, verified exactly for each l=4,6,...,22.
Therefore N is strictly increasing on x>0 and has one positive zero.
H decreases then increases, starts at pi/2, and tends to zero at infinity
because deg B<deg A. Its increasing tail is negative. It has exactly one
positive zero. Strict Arb signs also show H(1)<0 for every selected k.
Bisection of (0,1) uses only strict signs and exact rational endpoints.
No source decimal initializes or identifies a root.
For 100 requested digits the generator uses 500 bits and 422 bisections.
The entire rational root bracket is converted to an enclosing Arb ball.
Evaluation of
beta(x) = (1+3x^2)/2 - 3x/(2 atan(1/x))
then encloses the exact energy ratio. Its largest radius was below
7.96e-128. A second computation at 700 bits produced identical rational
root brackets. The enclosures, rather than agreement alone, support proven
rigour and the written 100 significant digits.
The conversion beta(e)=3/(2e^2)-1-3 sqrt(1-e^2)/(2e asin(e)) follows from
x=sqrt(1-e^2)/e and asin(e)=atan(1/x). More physically, choose focal length
one and G=rho=1. Then a_equatorial^2=1+x^2, c=x,
M=4*pi*x*(1+x^2)/3. AKM's surface potential is
Phi(eta) = -M [q_0(x)+q_2(x) P_2(eta)].
At the pole, Phi0=Phi_pole=-M(q_0+q_2). At the equator,
Phi_equator=-M(q_0-q_2/2). Hydrostatic equilibrium gives
Omega^2=2(Phi_equator-Phi_pole)/(1+x^2). With I=2M(1+x^2)/5,
T=I Omega^2/2, and AKM's virial expression W=3M Phi0/5+T,
one obtains beta=T/(-W)=q_2/q_0. These identities imply the generator's
formula and the displayed spheroid mass, rotation and energy formulas.
The independent checker calculates even Legendre polynomial coefficients
from factorials, without the generator's recurrence:
[x^(2j)] p_(2m) = (2m+2j)!/[2^(2m)(m-j)!(m+j)!(2j)!].
It evaluates q_l with validated Arb quadrature of the original defining
integral after t=x/u maps its domain to [0,1]. The integrand is
x u^(2l) / [(u^2+x^2) (u^l p_l(x/u))^2].
At both exact rational endpoints of every root bracket it evaluates AKM (3)
using this integral and requires strict opposite signs. These independent
signs, combined with global uniqueness, certify the same root without H.
The integral energy calculation uses the entire root ball as input and
assembles Phi_pole, Phi_equator, Omega^2, I, T and W in that order. It checks
T>0, W<0 and a finite narrow beta enclosure. Its largest beta radius was
below 1.75e-125. Both this independent enclosure and the generator's
narrower enclosure fit strictly inside the interval represented by every
written 100-digit decimal, namely its midpoint plus or minus 10^(-100).
At 600 bits, quadrature uses requested absolute and relative tolerance
2^(-510) for point inputs and 2^(-400) for root-ball inputs. Every returned
integral is required finite with radius below 1e-140 or 1e-115 respectively;
final independent beta radii must be below 1e-110. Controls precede every
entry check: q_0(1)=pi/4, q_2(1)=pi/2-3/2, and beta(1)=2-6/pi are nonzero
and must overlap the independently computed balls. These are substantive
controls against a checker returning zero or an uninformative wide ball.
The checker also verifies every displayed conversion through e, the energy
and rotation formulas, the strict order beta_1<...<beta_10, and agreement
with all ten rounded energy ratios and eccentricities in AKM Table 1.
The same checks are run on the strings read back from the draft. Coarse
source values check conventions; they are not the high-precision evidence.
Policy manifest: agents/runs/20261030T190951Z-build-skills/manifest.json.
Archived local and live SHA-256, identical:
dedecbdca15a728b6e594bfa79f0d149896fca336080ac27b53f513e0b16cd2e.