# Root and enclosure certificate for T627

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.

Bisection takes 422 steps for digits=100 (numberdb.bits(122)); each decision
requires a strict Arb sign, otherwise it fails. The exact rational endpoints
are retained. Their closed interval is converted into a ball containing it,
and propagated through e=1/sqrt(1+x^2). The generator asserts a finite ball
in (0,1) with radius below 10^(-118). A second computation at 700 bits must
produce the same exact bracket as the 500-bit computation. The numerical
record gives the actual steps indirectly through the rational denominator
and gives every actual output radius.

Independent check: checks.py computes the coefficients of p_(2m) from

    coefficient of x^(2j) = (2m+2j)! / [2^(2m)(m-j)!(m+j)!(2j)!],

and evaluates q_l from its defining integral with Arb's validated quadrature.
The substitution t=x/u converts the domain to [0,1], with integrand

    x u^(2l) / [(u^2+x^2) (u^l p_l(x/u))^2].

This is a rational integrand, with a polynomial denominator and no logarithm
branch. The independent path uses neither the q recurrence nor H nor B/A.
Before checking entries it verifies nonzero controls q_0(1)=pi/4 and
q_2(1)=pi/2-3/2, requiring finite quadrature balls of radius <10^(-130).
It uses the same radius threshold on every subsequent integral.

Each written 100-digit value m denotes [m-10^(-100),m+10^(-100)]. At both
endpoints the independent check evaluates the original AKM (3) residual,
including q_2 from quadrature. Its signs must be strictly negative and
positive, respectively. These signs prove a zero in the represented interval;
the polynomial certificate identifies it as the unique positive root for k.
The same checks are repeated on the strings read back from the draft.

The source's ten eccentricities and ten axis ratios are checked against
their rounding intervals. They identify the indexing and normalization;
the validated integral endpoint signs support the high precision.
The checks also certify the strict order 0<e_1<...<e_10<1.

Instructions: agents/runs/20261030T141911Z-build-skills/manifest.json.
Local and live instruction SHA-256:
28ecbeeccb0c5e5d6eb541b5a5b0f88aec47b154374d909085116d34f5629199.