back to table · edit · history · where entries came from · files · download
5302 bytes, as of the version from 2026-10-30 08:47 (current). Recorded here, not run.
# Formula conversions and independent checks for T620
This build uses the matching archived skills in
`../20261030T071029Z-build-skills/manifest.json`, SHA-256
`28ecbeeccb0c5e5d6eb541b5a5b0f88aec47b154374d909085116d34f5629199`.
The source files and hashes are in source-manifest.json. The mathematical
sources are Aurell–Salomonson (hep-th/9304031), Kalvin (1910.00104v2 and
2610.35383v1), and Mårdby–Rowlett (doi:10.1007/s00041-025-10202-6).
## Normalization and proof hypotheses
Aurell–Salomonson Proposition 6 gives Z'_Pn(0) at physical circumradius R.
Set R=1 and negate their equation (24). Their auxiliary R_n is the radius
of the Schwarz–Christoffel image with derivative one at the origin, not our
physical radius. Thus its reciprocal is the interior conformal radius in
T554. Their square has area 2 at circumradius one. The text saying n=2
before equation (25) is a typo; the displayed object is P_4.
Write a=1-2/n, c=(n-1)/(6(n-2)), and
log R_n = log Gamma(1+1/n)+log Gamma(1-2/n)-log Gamma(1-1/n).
Then L_n=2c log R_n+log n/[3(n-2)]-n F(a).
Kalvin 2020 equation (3.15) gives F via the Barnes derivative; Appendix A,
Lemma A.1 gives the finite rational formula. Reduce a=p/q before evaluating
it. Since p and q are coprime, all nonterminal sawtooth inputs in its sums
are nonintegral. The Gamma arguments are their fractional parts.
Kalvin 2026 Section 7 applies to a bounded simply connected Euclidean polygon
with N>=3, positive angles pi alpha_j, alpha_j in (0,2), and sum alpha_j=N-2.
Our regular polygons satisfy these conditions, have smooth flat interior,
straight geodesic sides, no interior singularities, genus zero and one boundary
component. Their Dirichlet Friedrichs Laplacians are strictly positive.
Equations (7.2)--(7.5) prove the polygon formula; Remark 3.4 of the 2020
paper identifies the corner normalization with Aurell–Salomonson. This is
a source-based proof justification, not a claim that a build reproduced
the analytic proof of the 2026 preprint. Numerical independence is checked
separately. The preprint status and date remain explicit in the references.
The heat coefficient is n(1/a-a)/24=c, by exact rational algebra. Eigenvalue
scaling lambda(tP)=lambda(P)/t^2 implies L(tP)=L(P)-2c log t.
For side one, t=1/[2 sin(pi/n)]; for area one, t=A_n^(-1/2).
These are conversions, not additional stored values.
## Independent corner integral
Equations (18) and (20) of Aurell–Salomonson give
F(a)=(1/a-a)(gamma-log 2)/12-(1/a+3+a)log(a)/12+Jtilde(a),
where Jtilde is the integral from zero to infinity of
[ (coth(x/(2a))-a coth(x/2))/(2x) - (1/a-a)/12 ] / (exp(x)-1).
Near zero, the bracket is evaluated as
sum_(k>=2) B_(2k)/(2k)! (a^(1-2k)-a) x^(2k-2).
This cancels the poles and constant term algebraically, rather than subtracting
large floating-point quantities. checks.py uses k=2,...,111 for x<=1/8.
The identity |B_(2k)|/(2k)!=2 zeta(2k)/(2pi)^(2k) gives an elementary bound
on the remainder. Since 1/3<=a<=1, the integrated omitted absolute contribution
on [0,delta] is at most
8 a/delta^2 * (delta/(2pi a))^224 /
[(1-(delta/(2pi a))^2)*222], delta=1/8.
Here 1/(exp(x)-1)<=1/x and zeta(2k)<2 were used. The bound is less than
10^(-269) uniformly on the selected angles. This is only a bound on the
series truncation, not on quadrature over a finite interval.
At T=(dps+20)log 10 the omitted infinite tail has absolute bound
exp(-T)/(1-exp(-T)) *
[ (1+a)(1+2/(exp(T)-1))/(2T) + (1/a-a)/12 ].
It follows from coth(x/(2a))<=coth(x/2)<=1+2/(exp(T)-1), x>=T, a<=1.
The log-determinant tail bound is n times this bound. The integral is
computed at 150 and 200 decimal digits with 40 guard digits. Agreement
corroborates the finite formula, but does not certify mpmath's quadrature.
Certification of the stored digits uses the finite Arb computation.
Controls precede comparisons: integrate exp(-x) and recover 1-exp(-T);
F(1)=0; F(1/2)=log(2)/12+log(2pi)/8, a nonzero corner value.
## Independent integrable domains
For the square, separated eigenvalues give D_4=eta(i)/2^(3/4).
The eta product is evaluated as -pi/12+sum log(1-exp(-2pi j)).
For rho=exp(-2pi), the absolute logarithmic tail after M terms is at most
rho^(M+1)/[(1-rho)(1-rho^(M+1))]. The bound is included in the Arb ball.
This gives D_4=Gamma(1/4)/(2^(7/4) pi^(3/4)).
For the equilateral triangle of side sqrt(3), Mårdby–Rowlett Corollary 3.3
provides the independently separated spectral expression
-Z'_3(0) = -2/3 log(3sqrt(3)/2)-pi sqrt(3)/36
-2/3 sum_(j>=1) (-1)^j sigma_1(j) exp(-pi sqrt(3)j)/j.
Because sigma_1(j)/j<=j, its absolute tail is bounded by
rho^(M+1)*((M+1)-M*rho)/(1-rho)^2, rho=exp(-pi sqrt(3)).
Both checks use M=160. The equivalent closed form is
D_3=Gamma(1/3)/(pi^(2/3) 3^(11/12)). Both sides are finite and narrow
before comparison. A deliberate 10^-6 displacement must fail each control.
Each serialized 100-significant-digit decimal denotes its midpoint plus or
minus one last-place unit. The 750-bit recomputation must lie strictly
inside that interval, not merely overlap it. The independent integral values
must also lie inside it. Post-fill checks repeat containment on the values
read from NumberDB, check log(det)=logdet with those stored intervals, and
repeat both separated-spectrum controls on stored rows.