back to table · edit · history · where entries came from · files · download
5391 bytes, as of the version from 2026-10-30 20:20 (current). Recorded here, not run.
# Root and enclosure certificate for T630
Write x=xi>0, l=2k+2 and a(x)=atan(1/x). Let p_0=1, p_1=x, r_0=0,
r_1=1. Both polynomial sequences obey
(n+1) v_(n+1) = (2n+1) x v_n + n v_(n-1).
For even l, set q_l=p_l a-r_l. All polynomial arithmetic uses QQ[x].
The generator verifies the polynomial identity
(1+x^2)(r_l p_l' - r_l' p_l) - p_l^2 = -1.
Consequently (q_l/p_l)'=-1/((1+x^2)p_l^2). The coefficients of p_l are
nonnegative and its constant coefficient is positive. Since r_l has degree
l-1, q_l/p_l tends to zero at infinity. Integration proves that q_l is exactly
the real oblate function in the source's defining integral. This also fixes
its branch. There is no appeal to a numerical fit of a special function.
For p_2=(1+3x^2)/2 and q_2=p_2 a-3x/2, the right side of AKM (3)
simplifies to 2x(1-xa). Thus the original equation is equivalent to
H(x) = a(x) - B(x)/A(x) = 0,
A=p_l^2+x^2, B=p_l r_l+x.
Its derivative has the positive denominator (1+x^2)A^2 and numerator
N=(1+x^2)(B A'-B' A)-A^2.
For each l=4,6,...,22 the generator verifies exactly that N has a negative
constant coefficient, only nonnegative other coefficients, and positive
leading coefficient. Hence N is strictly increasing on x>0 and has exactly
one positive zero. H first decreases, then increases. H(0+)=pi/2; deg B<deg A
implies H(infinity)=0. On its increasing tail H is therefore negative.
There is exactly one positive zero of H. Arb also certifies H(1)<0, giving
a finite starting bracket (0,1). No source decimal is used for initialization.
The exact root certificate is adapted from the public T627 generator and
certification, downloaded from the website. Source hashes are recorded in
source-provenance.json. The attached generator is standalone and recalculates
every root. It does not fetch or use any stored eccentricity.
Bisection takes 422 steps at 100 requested digits. Every branch decision has
a strict Arb sign. At 500 and 700 working bits the exact rational brackets
are identical. A ball enclosing the whole bracket is propagated through
w2 = [x (1+3x^2) atan(1/x) - 3x^2]/2,
j2 = (4/25) [3/(4 pi)]^(4/3) w2 [(1+x^2)/x^2]^(2/3).
All powers have positive real bases. The largest output radius is less than
2.23e-127, amply supporting 100 significant digits. No rounded eccentricity
from the source or another table is used as an input.
## Independent numerical check
The checker uses the explicit coefficients
[x^(2j)] p_(2m) = (2m+2j)! / [2^(2m)(m-j)!(m+j)!(2j)!].
It evaluates q_l from the defining integral by Arb validated quadrature,
substituting t=x/u to integrate the rational integrand
x u^(2l) / [(u^2+x^2) (u^l p_l(x/u))^2]
on [0,1]. This computation uses neither the q recurrence nor the reduced H.
The original AKM (3) residual has strict opposite signs at every exact
rational root-bracket endpoint. Nonzero controls q_0(1)=pi/4 and
q_2(1)=pi/2-3/2 precede these checks. Quadrature balls must be finite,
have imaginary part containing zero, and meet explicit radius bounds.
For a separate physical computation, choose positive focal length b, density
rho and gravitational constant G. Then a^2=b^2(1+x^2), c=bx. AKM's surface
potential gives
Phi_pole = -(4 pi/3) G rho b^2 x(1+x^2) (q_0+q_2),
Phi_equator = -(4 pi/3) G rho b^2 x(1+x^2) (q_0-q_2/2).
Equating Phi-Omega^2 R^2/2 on the surface gives
Omega^2=2(Phi_equator-Phi_pole)/a^2. Independent volume integrals give
M = pi rho a^2 c integral_-1^1 (1-z^2) dz,
I = (pi/2) rho a^4 c integral_-1^1 (1-z^2)^2 dz,
J^2 = I^2 Omega^2.
The dimensionless result is assembled directly as J^2 rho^(1/3)/(4 pi G
M^(10/3)). Controls verify the two nonzero integrals equal 4/3 and 16/15.
The ratios I/(Ma^2)=2/5 are checked on every branch. Runs at (b,rho,G)=(1,1,1)
and (2,3,5) agree, testing cancellation of physical scales.
The largest independent j2 radius is less than 1.43e-126. Every independent
and generated enclosure must lie strictly inside the written decimal interval,
not merely overlap it. Values are between 0.01 and 0.1, so the 100 significant
digits are written with 101 decimal places and mean plus or minus 1e-101.
The stored strings are read back and the same checks repeated on them.
All ten coarse j2, eccentricity and squared-angular-velocity values in AKM
Table 1 agree with their rounding intervals. The generated j2 values strictly
increase on the selected prefix. Displayed eccentricity conversions and the
energy-ratio conversion are also checked for all ten branches.
## Resolved local discrepancy
The first checker run used 8/75 instead of 4/25 as the coefficient of the
auxiliary energy-ratio conversion. The independently reconstructed j2 and the
generator agreed, while that auxiliary identity was smaller by 2/3. From
T=I Omega^2/2 and W=-(3GM^2/(5a)) theta/e one obtains
beta=w2 e/(s theta), and hence
j2=(4/25) [3/(4 pi)]^(4/3) beta theta/(e s^(1/3)).
This derivation identifies the error rather than selecting a preferred result.
The checker was corrected before any entries were sent. Its original failure
log is retained as an artifact; all corrected checks passed.
Instructions: agents/runs/20261030T195647Z-build-skills/manifest.json.
Both archived local/live SHA-256:
dedecbdca15a728b6e594bfa79f0d149896fca336080ac27b53f513e0b16cd2e.
This build evidence does not constitute the separate campaign critique.