Complex multiplication and the integrality of E₂* (Milla, Appendix B)

For a CM point τ with A + Bτ + Cτ² = 0 (A, B, C ∈ ℤ, gcd = 1, discriminant D = B² − 4AC < 0), the paper defines κ·ω₂ := A·η₁ − C·τ·η₂ and proves (PLAN B2):

• lemkapa1 : κ = −√D·(π²/(3ω₁²))·E₂*(τ) (via Legendre and η₁ = π²E₂/3);
• lemkapa2 : Cτ·κ = −∑_{v ∈ DIV(Cτ)} ℘(v) (via the elliptic ζ-combination and theowpsum);
• theoezweisternrest : √D·(E₂*(τ)/η(τ)⁴)·(AC)² is an algebraic integer, where η is the Dedekind eta function (1728·η²⁴ = E₄³ − E₆², Mathlib's discriminant).

Branch convention: for the root of A + Bτ + Cτ² = 0 in ℍ we have √D = 2Cτ + B (the paper's choice of √D); all statements below use 2Cτ + B in place of √D, which keeps them branch-free.

At τ₁₆₃ : 41 − τ + τ² = 0, i.e. A = 41, B = −1, C = 1, D = −163, √D = 2τ − 1 = i√163, AC = 41 — the specialization used in Coefficients.lean.

noncomputable def Chudnovsky.kappa (τ : UpperHalfPlane) (A C : ℤ) : ℂ

Milla's κ (Def. defkappa), for the lattice L_τ = ℤ + ℤτ (so ω₁ = 1, ω₂ = τ): κ = (A·η₁ − C·τ·η₂)/τ.

Equations

• Chudnovsky.kappa τ A C = (↑A * (Chudnovsky.Lτ τ).eta₁ - ↑C * ↑τ * (Chudnovsky.Lτ τ).eta₂) / ↑τ

theorem Chudnovsky.lemkapa1 {τ : UpperHalfPlane} {A B C : ℤ} (hCM : ↑A + ↑B * ↑τ + ↑C * ↑τ ^ 2 = 0) : kappa τ A C = -(2 * ↑C * ↑τ + ↑B) * ↑Real.pi ^ 2 / 3 * E₂star τ

Milla's lemkapa1: κ = −√D·(π²/3)·E₂*(τ) (with ω₁ = 1 and √D = 2Cτ + B). Uses the Legendre relation and η₁ = π²E₂/3.

theorem Chudnovsky.isIntegral_C_mul_conj {τ : UpperHalfPlane} {A B C : ℤ} (hCM : ↑A + ↑B * ↑τ + ↑C * ↑τ ^ 2 = 0) : IsIntegral ℤ (↑C * (starRingEnd ℂ) ↑τ)

Intermediate step towards theoezweisternrest (Milla's final "product of algebraic integers" step): C·τbar is an algebraic integer, being a root of the monic integer polynomial X² + B·X + AC. Indeed τbar = conj τ satisfies the conjugate CM relation A + B·τbar + C·τbar² = 0 (the coefficients A, B, C are real), and multiplying by C gives (Cτbar)² + B·(Cτbar) + AC = 0.

theorem Chudnovsky.isIntegral_E₄_div_eta_pow (τ : UpperHalfPlane) (hj : IsIntegral ℤ (1728 * J τ)) : IsIntegral ℤ (ModularForm.E₄ τ / ModularForm.eta ↑τ ^ 8)

Easy part of Milla's satzezweistern: E₄/η⁸ is an algebraic integer whenever j = 1728·J is (it is a root of X³ − j).

theorem Chudnovsky.isIntegral_E₆_div_eta_pow (τ : UpperHalfPlane) (hj : IsIntegral ℤ (1728 * J τ)) : IsIntegral ℤ (ModularForm.E₆ τ / ModularForm.eta ↑τ ^ 12)

Easy part of Milla's satzezweistern: E₆/η¹² is an algebraic integer whenever j = 1728·J is (it is a root of X² − (j − 1728)).

Rescaling to the lattice L̂ = (π/√3)·η²·L_τ and the final integrality

Milla's proofzweistern rescales L_τ to L̂ = a·L_τ with a = (π/√3)·η(τ)², so that ω₁(L̂) = a, π²/(3ω₁(L̂)²) = 1/η⁴, and ¼g₂(L̂) = 3E₄/η⁸, ¼g₃(L̂) = 2E₆/η¹² become algebraic integers (given the integrality of j = 1728J). The identity of Prop. lemkapppppa applied to L̂ then reads √D·(E₂*/η⁴)·(AC)² = (∑_{v ∈ DIV(Cτ)} AC·℘(v;L̂))·Cτbar, whose right-hand side is a product of algebraic integers (theomwpu with m = AC, plus isIntegral_C_mul_conj).

lemkapa2: the elliptic ζ-combination (Milla's lemfellip–lemkapa2 + lemctau)

We prove ∑_{v ∈ DIV(Cτ)} ℘(v) = −AC·η₁ + C²τ·η₂ (= −Cτ·κ) by the theowpsum template of DivisionValues.lean, applied to multiplication by α = Cτ (which maps L_τ into itself with index AC): the difference ∑_u ℘(z+u) − α²·℘(αz), summed over a transversal u of α⁻¹L/L, is entire and elliptic, hence a constant c; the ζ-combination ∑_u ζ(z+u) − α·ζ(αz) has derivative −(that difference) and additive period defect AC·η₁ − C²τ·η₂ in the direction ω₁ = 1, so F(z) = ζ-comb + c·z, being locally constant on the connected complement of α⁻¹L, forces c = −AC·η₁ + C²τ·η₂. Evaluating at z = 0 identifies c with the division-value sum. The transversal is Milla's lemctau (eq. ctauu): the M = AC points u = (v₁/M) + (v₂/M)·τ with C ∣ v₂ and M ∣ C·v₁ − B·v₂.

The remaining analytic + combinatorial core

The following lemma is the paper's lemkapa2/lemkapppppa (the elliptic ζ-combination, Laurent-residue argument via Liouville 1 and theowpsum) rescaled to the lattice L̂ and combined with lemctau (DIV(Cτ) ⊂ DIV(AC), |DIV(Cτ)| = AC − 1). It packages exactly

√D·(E₂*/η⁴)·(AC)² = (∑_{v ∈ DIV(Cτ)} AC·℘(v; L̂))·Cτbar

as an existential over the (nonzero) AC-division-point index set carrying the sum. Everything else in theoezweisternrest_of_isIntegral_j is proved from it.

This is the sole remaining gap in Appendix B: it needs (i) the Laurent-coefficient extraction for ζ at z = 0 and (ii) the explicit DIV(Cτ) ↪ DIV(AC) embedding (paper Lemma lemctau), neither of which is available in the current toolbox (theowpsum/theomwpu in DivisionValues.lean are themselves pinned interfaces).

theorem Chudnovsky.theoezweisternrest_of_isIntegral_j (τ : UpperHalfPlane) {A B C : ℤ} (hgcd : (↑(A.gcd B)).gcd C = 1) (hCM : ↑A + ↑B * ↑τ + ↑C * ↑τ ^ 2 = 0) (hj : IsIntegral ℤ (1728 * J τ)) : IsIntegral ℤ ((2 * ↑C * ↑τ + ↑B) * (E₂star τ / ModularForm.eta ↑τ ^ 4) * (↑A * ↑C) ^ 2)

Conditional form of theoezweisternrest (the honest, provable statement): if j = 1728·J(τ) is an algebraic integer, then so is √D·(E₂*/η⁴)·(AC)².

This is the full content of Milla's proofzweistern except the CM input that j(τ) is an algebraic integer. For a general CM point that input is Silverman's theorem (PLAN Phase C, SingularModuli.lean), which is only pinned here at τ₁₆₃; the unconditional theoezweisternrest below therefore genuinely requires it (see the statement audit note).