# Formula conversion and checks for T621

## Object and conventions

Let P_n be the interior of the convex hull of exp(2*pi*i*j/n), 0 <= j < n,
and let alpha=(n-2)/n, A=(n/2)*sin(2*pi/n). The operator is -d_x^2-d_y^2,
with homogeneous Neumann conditions on all sides. The unique constant zero
mode is omitted from the spectral zeta function. Every other eigenvalue is
counted with multiplicity. D=exp(-Z'(0)) and L=log D use real natural logarithms.
There is no implicit mass term or division by area.

The governing archived skill manifest is
`../20261030T080603Z-build-skills/manifest.json`; both versions read have SHA-256
`28ecbeeccb0c5e5d6eb541b5a5b0f88aec47b154374d909085116d34f5629199`.
See `skill-evidence.json` and `sources.json` for recorded provenance.

## Neumann/Dirichlet conversion

Kalvin 2610.35383v1, Section 1, excludes zero eigenvalues in both determinants.
For a topological disk the squared torsion/L2 norm quotient is the area A.
Dividing the two identities in Theorem 1.1 gives

    D_N / D_D = A * product_j alpha_j^(-1/2)
              = A * alpha^(-n/2).
    L_N = L_D + log A - (n/2)*log alpha.

The inverse area, the reciprocal angle product, and inclusion of the zero mode
would each give a different quantity. Our polygons satisfy the theorem's
flat-interior, straight-boundary, positive-angle hypotheses. The 2026 source is
a preprint; this run checks its hypotheses and conversion, not its entire proof.
Its Section 7 derives the Aurell-Salomonson polygon formula.

Put c=(n-1)/(6*(n-2)), and
R=Gamma(1+1/n)*Gamma(1-2/n)/Gamma(1-1/n).
Aurell-Salomonson Proposition 6, (23)-(24), with physical circumradius 1, gives
L_D=2*c*log R+log(n)/(3*(n-2))-n*F(alpha).
The auxiliary R is reciprocal to the Euclidean conformal radius in T554;
it is not the physical circumradius. Kalvin 1910.00104v2, (3.15), expresses F
through the Barnes zeta derivative. Lemma A.1 reduces that derivative at
reduced p/q to finite log-Gamma sums, a Dedekind sum and zeta_R'(-1).
The generator implements these formulas with exact rational coefficients.
The finite corner routine is adapted from T620's live attached generator,
downloaded during this run; the full source and its hash are preserved locally.

The corner heat coefficient is n*(1/alpha-alpha)/24=c. Removing the constant
Neumann mode gives Z_N(0)=c-1. Dilation by t multiplies eigenvalues by t^(-2),
so L_N(t P_n)=L_N(P_n)-2*(c-1)*log t. It also multiplies the determinant ratio
by t^2, agreeing with the area factor. Side length one corresponds to
 t=1/[2*sin(pi/n)], and area one to t=A^(-1/2).

## Independent integrable-domain controls

For a square of side a, Neumann adds to the Dirichlet spectrum the two positive
axis sequences pi^2*k^2/a^2. For an equilateral triangle of side ell, the
positive Dirichlet indices j,k>=1 become j,k>=0, omitting (0,0); the two added
axis sequences are 16*pi^2*k^2/(9*ell^2). These enumerations are recorded in
T485 and the integrable-polygon sources, independently of the corner formula.
The added zeta function is 2*K^(-s)*zeta_R(2*s). Using zeta_R(0)=-1/2 and
zeta_R'(0)=-log(2*pi)/2, its contribution to log determinant is log(4*pi^2/K).
Thus the square ratio is 4*a^2, and the triangle ratio is 9*ell^2/4.
Our sizes a=sqrt(2), ell=sqrt(3) give 8 and 27/4 respectively.

For the square we use the convergent product for eta(i), not the finite corner
code. With rho=exp(-2*pi) and M=160, the omitted absolute log sum is at most
rho^(M+1)/[(1-rho)*(1-rho^(M+1))].
For the triangle we use Mårdby-Rowlett Corollary 3.3's convergent divisor sum,
with rho=exp(-pi*sqrt(3)). The bound sigma_1(j)/j<=j gives absolute tail at most
rho^(M+1)*[(M+1)-M*rho]/(1-rho)^2 after M=160 terms. These tails are added as
ball radii. Neither control uses Gamma values or the corner determinant code.
The equivalent closed forms are checked separately:

    D_3^N = 3^(25/12)*Gamma(1/3)/(4*pi^(2/3)),
    D_4^N = 2^(9/4)*eta(i) = 2^(5/4)*Gamma(1/4)/pi^(3/4).

Both controls are finite, narrow and nonzero; shifting a log determinant by
10^(-6) must fail the comparison. Decimal-containment tests similarly reject
a deliberate perturbation by ten units of the serialized last place.

## Independent corner integral

Aurell-Salomonson (18), (20) gives F(a) as two elementary terms plus

    integral_0^infinity B_a(x)/(exp(x)-1) dx,
    B_a(x)=[coth(x/(2*a))-a*coth(x/2)]/(2*x)-(1/a-a)/12.

The integral code is adapted from the attached T620 checks, which use a
mathematically different computation from the finite Dedekind/Gamma sums.
For 0<=x<=delta=1/8 it uses the cancelled series

    B_a(x)=sum_{k>=2} B_(2k)/(2k)! * (a^(1-2k)-a)*x^(2k-2).

Terms k=2,...,111 are kept. As |B_(2k)/(2k)!|<=4/(2*pi)^(2k) and
exp(x)-1>=x, the omitted integral beginning at K=112 is bounded by

    4*a/[(2*K-2)*delta^2] *
    [r_a^(2*K)/(1-r_a^2) + r_1^(2*K)/(1-r_1^2)],
    r_a=delta/(2*pi*a), r_1=delta/(2*pi).

This is uniformly far below 10^(-260) for 1/3<=a<=1. At the other endpoint,
T=(dps+20)*log(10) and the integral from T to infinity is bounded by

    exp(-T)/(1-exp(-T)) *
    [(1+a)*(1+2/(exp(T)-1))/(2*T)+(1/a-a)/12].

The remaining finite quadrature uses mpmath at 150 and 200 decimal digits,
with 40 guard digits. Agreement is corroboration, not a certified quadrature
error bound. A nonzero exp(-x) integral is checked first at each precision;
F(1)=0 and the nonzero F(1/2)=log(2)/12+log(2*pi)/8 are also controls.
We add the Neumann area/angle ratio to both independent integral computations.

## Certification and readback

Certification of the table comes from the finite formula evaluated by Arb,
not the quadrature. Production uses 100 significant digits plus 180 guard bits
(513 working bits), and a fresh 750-bit evaluation tests every serialized
interval. All balls must be finite and have at least 400 relative accuracy bits;
comparison balls require 680 bits. The measured minimum is in the evidence.
Every written decimal denotes its exact center plus or minus one last-place
unit, and rational comparisons test containment of the entire fresh ball.

After filling, checks repeat on all values fetched from T621. They test the
56 integral comparisons, both spectral controls, all exp/log pairs and all 28
ratios against the stored T620 intervals. The separate family checks also
compare area and conformal-radius ingredients with the live companion tables.
`verify(sample=None)` provides the package's additional generator comparison.
No build check replaces the separate independent critique required by the campaign.