back to table · edit · history · where entries came from · files · download
3185 bytes, as of the version from 2026-10-27 18:01 (current). Recorded here, not run.
# Checked sources and derivations for T555
The defining source is the 50-page author PDF of F. Calegari, V. Dimitrov and
Y. Tang, *The Unbounded Denominators Conjecture*:
https://web.math.princeton.edu/~yunqingt/UDC.pdf.
Section 5.1, Definition 5.1.1 normalizes the universal cover at zero;
Theorem 5.1.4 and equation (5.1.5) give the Gamma quotient used here.
The boundary normalization F_n(1)=1 in that source is not needed for the
absolute derivative. Choosing F_n'(0)>0 fixes the source rotation instead.
The Gamma arguments are positive for n >= 2 and the positive real n-th root
of 16 is used. The author PDF is archived with SHA-256
5161130f8d3c3353444c315747c771d9eeffe963d80d7ae6a63c3027f0a28604.
The current bibliographic record is https://arxiv.org/abs/2109.09040;
the locator 5.1.5 refers specifically to the linked author PDF.
https://dlmf.nist.gov/5.7.E3 gives a convergent expansion of log Gamma.
Expanding -log(1+z) yields the familiar coefficients zeta(m)/m.
In the defining quotient, the linear and even-degree terms cancel, leaving
log(gamma_n) = log(16)/n + sum_{k>=1}
2(1-2^(-2k))*zeta(2k+1)/((2k+1)*n^(2k+1)).
For the first omitted odd degree M, each coefficient is less than 4/m
because 0 < 1-2^(1-m) < 1 and zeta(m) < 2 for m >= 3. Summing the geometric
majorant gives the positive tail bound
0 < tail <= 4/(M*n^M*(1-n^(-2))).
Checks.py takes 240 terms (degrees 3 through 481), so M=483, and performs all
arithmetic with 600-bit balls. It shares no Gamma evaluations or computation
code with the generator for its comparison of every order. This tests the
Gamma implementation and formula transcription, not a second proof of the
uniformization theorem. Positivity of the series coefficients also shows
that the radius decreases to 1 as n tends to infinity, explaining the choice
not to extend only to large indices.
For n=2, the Gamma functional equation and reflection at 1/4 reduce the
quotient to Gamma(1/4)^4/(4*pi^2). DLMF 19.20.2 gives
R_F(0,1,2)=Gamma(1/4)^2/(4*sqrt(2*pi)); homogeneity of R_F and DLMF 19.25.1
then give K(m=1/2)=Gamma(1/4)^2/(4*sqrt(pi)). Thus gamma_2=4*K(1/2)^2/pi.
Checked sources:
https://dlmf.nist.gov/19.20.E2 and https://dlmf.nist.gov/19.25.E1.
DLMF 19.8.1 and 19.8.5 give the independently implemented AGM iteration
and K=pi/(2*AGM(1,1/sqrt(2))). The successive geometric and arithmetic
iterates bound the limit. Twelve iterations at 600 bits give a narrow
rigorous enclosure; the equal-argument controls AGM(1,1)=1 and AGM(2,2)=2
are checked before using it. The DLMF uses the modulus k=1/sqrt(2), whereas
the NumberDB K table uses the parameter m=k^2=1/2.
https://dlmf.nist.gov/19.8#i.
The generator's 461-bit Arb calculation is the source of the `proven` claim.
The zeta-series and AGM checks are independent computational checks with
explicit enclosures. None substitutes agreement alone for an error bound.
All serialized decimals are checked using exact rational endpoints, not
rounded midpoints.
The policy read for this build is archived at
agents/runs/20261027T175211Z-build-skills/manifest.json.
Its local and live copies both have SHA-256
e37efb7e2ededf6c1d7134c673f152f648f26e0267c556aebdf3ec65765d8b4c.