Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Elliptic Modular Transport

Abstract

Integral changes of basis transport the original period lattice, its regularized Weierstrass function, and the normalized continued annular kernel under every integral determinant-one modular transformation.

Definition 1.1 (The integral period-lattice equivalence).

Lean statement: D5/S3/VertexAlgebra/Characters/EllipticModularTransport.modularLatticeEquiv

Formalization. D5/S3/VertexAlgebra/Characters/EllipticModularTransport.modularLatticeEquiv (✓ std3).

Source. Repository-derived.

Commentary.

Let gamma have entries a,b,c,d, with ad-bc=1, and put j=c tau+d. The coordinate map (m,n) maps to (am-bn,-cm+dn), with inverse (r,s) mapping to (dr+bs,cr+as). Composing these integral linear maps with the original period-pair lattice coordinates gives an actual integer-linear equivalence from the lattice generated by 1,tau to the lattice generated by 1,gamma tau. Its complex action is l mapping to l/j; its inverse is multiplication by j. Consequently w/j belongs to the new lattice if and only if w belongs to the old lattice.

Theorem 1.2 (Covariance of the original Weierstrass function).

Lean statement: D5/S3/VertexAlgebra/Characters/EllipticModularTransport.weierstrassP_modular

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Characters/EllipticModularTransport.weierstrassP_modular (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every gamma in SL(2,Z), every upper-half-plane tau, and every complex w outside the lattice generated by 1,tau, the original PeriodPair.weierstrassP for gamma tau at w/j equals j squared times the original function for tau at w. Reindex the regularized sum using the constructed lattice equivalence. Each complete summand 1/(w-l)^2 - 1/l^2 scales by j squared. The subtraction stays inside the summand, including the zero lattice index, where the total-field value of 1/0 is zero. Both evaluation points are outside their actual lattices; totalized values at poles are not analytic evaluations.

Definition 1.3 (The normalized continued kernel).

Lean statement: D5/S3/VertexAlgebra/Characters/EllipticModularTransport.continuedKernel

Formalization. D5/S3/VertexAlgebra/Characters/EllipticModularTransport.continuedKernel (✓ std3).

Source. Repository-derived.

Commentary.

Define the continued kernel at tau,w to be the original lattice-defined Weierstrass function divided by (2 pi i)^2, minus the normalized EisensteinSeries.E2 tau divided by 12. It is meromorphic in w and agrees with the existing ordinary annular kernel when 0 < Im w < Im tau.

Theorem 1.4 (Full modular covariance of the continued kernel).

Lean statement: D5/S3/VertexAlgebra/Characters/EllipticModularTransport.continuedKernel_modular

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Characters/EllipticModularTransport.continuedKernel_modular (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every gamma,tau,w with w outside the old period lattice, the continued kernel at gamma tau,w/j equals j squared times the kernel at tau,w minus c j/(2 pi i). The Weierstrass covariance supplies the geometric part. The existing full EisensteinSeries.E2_slash_action and riemannZeta_two supply the normalized correction, with its displayed sign and coefficient. No modular law is assumed for the period lattice or for the Weierstrass function.

Theorem 1.5 (The original annular-series consumer).

Lean statement: D5/S3/VertexAlgebra/Characters/EllipticModularTransport.annularKernel_modular_of_strictStrips

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Characters/EllipticModularTransport.annularKernel_modular_of_strictStrips (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every gamma,tau,w satisfying both 0 < Im w < Im tau and 0 < Im(w/j) < Im(gamma tau), let q=exp(2 pi i tau), z=exp(2 pi i w), q’=exp(2 pi i gamma tau), and z’=exp(2 pi i w/j). Then the original annular series at q’,z’ equals j squared times the original series at q,z minus c j/(2 pi i). Apply the existing strict-strip Weierstrass-E2 identity at both points and the continued modular covariance. The first strip excludes lattice points because an integer strictly between zero and one cannot occur as the second lattice coordinate.

The two strict strips are independent convergence requirements. For tau=i, w=(1+i)/2 and gamma=S, the first strip holds while w/j=(1-i)/2 is outside the second. Only the continued identity applies there. The multiplicative substitution remains singular at z=0 and gives no analytic annular boundary value at that point. These classical geometric results concern scalar functions; they supply no original-field thermal trace, four-point convergence, nonunimodular sector closure, full VOA or CFT construction, anomaly or fusion theory, string theory, or AdS/CFT correspondence.

References