The modular polynomial Φ_m ∈ ℚ[X, Y] (Phase C, chunks B3–B5)

Third file of Track 1 of Phase C (see Playground/Pi/PhaseC-PLAN.md, §3.1 sub-lemmas (B3)–(B5), §6.4). This is the keystone of the whole singular-moduli program: every downstream statement funnels through the identity Φ_m(X, j τ) = ∏_i (X − f_i τ) with ℚ-coefficients, and no route avoids it.

For a prime m (kept generic; m ∈ {41, 43, 61, 163} are instantiated later) the file builds, from the m-isogeny coset orbit f m i of CosetOrbit.lean:

• (A) Root-of-unity averaging sum_zetaM_zpow_mul (∑_{b : ZMod m} ζ^{b·n} = m·[m ∣ n]), the arithmetic heart of (B3): it kills every power of the base variable w that is not a genuine power of the nome q = w^m. Proved in full.
• (B) Power sums powerSum m k τ = ∑_i (f m i τ)^k: SL(2,ℤ)-invariance (powerSum_smul, from the S/T-permutations of the orbit) and holomorphy (mdifferentiable_powerSum). Proved in full. Likewise the orbit polynomial orbitPoly m τ = ∏_i (X − f_i τ) and the SL(2,ℤ)-invariance / holomorphy of its coefficients (the elementary symmetric functions of the orbit).
• (B4/B5) The q-expansion principle Sk_eq_poly_j (the critical lemma): an SL(2,ℤ)-invariant, holomorphic function that is meromorphic of finite order at the cusp with coefficients in a subring R ⊆ ℂ is a polynomial in j of bounded degree with R-coefficients. Proved by pole-order induction with coefficient tracking; the algebraic heart (leading-coefficient cancellation against j^N, coefficients staying in R) is unconditional, and the two genuinely-analytic primitives — the removable singularity / pole-reduction step and the Liouville base case (bounded + invariant + holomorphic ⇒ constant) — are gated behind explicit hypotheses, Valence.lean-style, with their routes documented. (See PhaseC-PLAN.md §6.4 / §6.6: the base case is the plan-sanctioned single gate.)
• (B5) Assembly PhiQ: gated on Sk_eq_poly_j + the (B3) q-expansion structure, the modular polynomial Φ_m ∈ ℚ[X][Y] with Φ_m(X, j τ) = ∏_i (X − f_i τ).

Status of the analytic gates (see PhaseC-PLAN.md §6.4)

Sk_eq_poly_j and PhiQ take the deep analytic facts as hypotheses rather than sorry. The whole file is sorry-free. The gated pieces, with routes, are documented at their TODO blocks:

1. poleReduction — the removable-singularity step: subtracting c·j^N from a pole-order-N cusp-meromorphic function yields a pole-order-(N−1) one. Route: the cusp function of (h − c j^N)·q^N is analytic at 0 with value 0, hence = w·(analytic), so dividing by one power of the nome stays bounded. Mathlib: AnalyticAt, cuspFunction, the qExpansion ring-hom API of NumberTheory/ModularForms/QExpansion.lean.
2. liouvilleBaseCase — bounded + SL(2,ℤ)-invariant + holomorphic ⇒ constant. Route (PhaseC-PLAN.md §6.4): descend to the disc via the cusp function, use exists_smul_mem_fd_j (from Valence.lean) to reduce every value to a compact truncation of the fundamental domain, and conclude via the open-mapping / clopen argument.
3. (B3) q-expansion structure of the power sums (the w-averaging producing the honest q-Laurent expansion with ℚ-coefficients and finite pole order) — the input to PhiQ, documented at PhiQ.

(A) Root-of-unity averaging

The clean arithmetic fact powering (B3): summing ζ^{b·n} over b : ZMod m (with ζ = zetaM m = exp(2πi/m)) gives m when m ∣ n and 0 otherwise. In the w-expansion of the orbit this averages the coset variable ζ^b·w down to the honest nome q = w^m.

theorem Chudnovsky.sum_zmod_eq_range {M : Type u_1} [AddCommMonoid M] (m : ℕ) [NeZero m] (g : ℕ → M) : ∑ b : ZMod m, g b.val = ∑ k ∈ Finset.range m, g k

Reindex a sum over ZMod m by ZMod.val to a sum over Finset.range m.

theorem Chudnovsky.zetaM_zpow_eq_one_iff {m : ℕ} [NeZero m] (n : ℤ) : zetaM m ^ n = 1 ↔ ↑m ∣ n

ζ^n = 1 ↔ m ∣ n for ζ = zetaM m a primitive m-th root of unity.

theorem Chudnovsky.sum_zetaM_zpow_mul {m : ℕ} [NeZero m] (n : ℤ) : ∑ b : ZMod m, zetaM m ^ (↑b.val * n) = if ↑m ∣ n then ↑m else 0

Root-of-unity averaging ∑_{b : ZMod m} ζ^{b·n} = m·[m ∣ n]. The ζ^{bn} factor is exactly the b-dependence of the w-expansion of the coset orbit (hasSum_f_some), so this lemma is what makes the power sums have honest q-Laurent expansions in (B3).

SL(2,ℤ)-invariance from the S, T generators

A plain function h : ℍ → ℂ invariant under the two generators S, T is invariant under all of SL(2,ℤ) — the invariant matrices form a subgroup containing the generators.

theorem Chudnovsky.invariant_of_S_T {h : UpperHalfPlane → ℂ} (hS : ∀ (τ : UpperHalfPlane), h (ModularGroup.S • τ) = h τ) (hT : ∀ (τ : UpperHalfPlane), h (ModularGroup.T • τ) = h τ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane) : h (γ • τ) = h τ

If h is invariant under S and T then it is invariant under all of SL(2,ℤ).

(B) Power sums of the orbit

powerSum m k τ = ∑_i (f m i τ)^k. Being a symmetric function of the SL(2,ℤ)-permuted orbit, it is SL(2,ℤ)-invariant; being a finite sum of powers of the holomorphic f_i, it is holomorphic.

noncomputable def Chudnovsky.powerSum (m : ℕ) [NeZero m] (k : ℕ) (τ : UpperHalfPlane) : ℂ

The k-th power sum ∑_i (f m i τ)^k of the coset orbit.

Equations

• Chudnovsky.powerSum m k τ = ∑ i : Option (ZMod m), Chudnovsky.f m i τ ^ k

theorem Chudnovsky.powerSum_T {m : ℕ} [NeZero m] (k : ℕ) (τ : UpperHalfPlane) : powerSum m k (ModularGroup.T • τ) = powerSum m k τ

T-invariance of the power sums (from sum_orbit_T_smul).

theorem Chudnovsky.powerSum_S {m : ℕ} [Fact (Nat.Prime m)] (k : ℕ) (τ : UpperHalfPlane) : powerSum m k (ModularGroup.S • τ) = powerSum m k τ

S-invariance of the power sums (from sum_orbit_S_smul; needs m prime).

theorem Chudnovsky.powerSum_smul {m : ℕ} [Fact (Nat.Prime m)] (k : ℕ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane) : powerSum m k (γ • τ) = powerSum m k τ

SL(2,ℤ)-invariance of the power sums.

theorem Chudnovsky.mdifferentiable_powerSum {m : ℕ} [NeZero m] (k : ℕ) : MDiff (powerSum m k)

Each power sum is holomorphic on ℍ.

(B) The orbit polynomial ∏_i (X − f_i τ)

The generating polynomial of the orbit; its coefficients are (up to sign) the elementary symmetric functions of {f_i τ}, which are SL(2,ℤ)-invariant and holomorphic.

noncomputable def Chudnovsky.orbitPoly (m : ℕ) [NeZero m] (τ : UpperHalfPlane) : Polynomial ℂ

The orbit polynomial ∏_i (X − f_i τ) ∈ ℂ[X].

Equations

• Chudnovsky.orbitPoly m τ = ∏ i : Option (ZMod m), (Polynomial.X - Polynomial.C (Chudnovsky.f m i τ))

theorem Chudnovsky.orbitPoly_monic {m : ℕ} [NeZero m] (τ : UpperHalfPlane) : (orbitPoly m τ).Monic

The orbit polynomial is monic of degree m + 1.

theorem Chudnovsky.orbitPoly_S {m : ℕ} [Fact (Nat.Prime m)] (τ : UpperHalfPlane) : orbitPoly m (ModularGroup.S • τ) = orbitPoly m τ

The orbit polynomial is S-invariant.

theorem Chudnovsky.orbitPoly_T {m : ℕ} [NeZero m] (τ : UpperHalfPlane) : orbitPoly m (ModularGroup.T • τ) = orbitPoly m τ

The orbit polynomial is T-invariant.

theorem Chudnovsky.orbitPoly_smul {m : ℕ} [Fact (Nat.Prime m)] (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane) : orbitPoly m (γ • τ) = orbitPoly m τ

SL(2,ℤ)-invariance of every coefficient of the orbit polynomial: the coset orbit is permuted by γ, so the product ∏_i (X − f_i τ) — and hence each coefficient (an elementary symmetric function of the orbit) — is unchanged.

Holomorphy of the elementary symmetric functions

Each coefficient of ∏_i (X − C (a i τ)) is a polynomial expression in the holomorphic a i τ, hence holomorphic. Proved by induction on the index finset (all coefficients at once).

theorem Chudnovsky.mdifferentiable_coeff_prod_X_sub_C {ι : Type u_1} (a : ι → UpperHalfPlane → ℂ) (ha : ∀ (i : ι), MDiff (a i)) (s : Finset ι) (n : ℕ) : MDiff fun (τ : UpperHalfPlane) => (∏ i ∈ s, (Polynomial.X - Polynomial.C (a i τ))).coeff n

Every coefficient of a product ∏_{i ∈ s} (X − C (a i τ)) of monic linear factors with holomorphic roots a i is a holomorphic function of τ.

theorem Chudnovsky.mdifferentiable_orbitPoly_coeff {m : ℕ} [NeZero m] (n : ℕ) : MDiff fun (τ : UpperHalfPlane) => (orbitPoly m τ).coeff n

Each coefficient of the orbit polynomial is a holomorphic function of τ.

(B4/B5) The q-expansion principle Sk_eq_poly_j

The critical lemma of the whole singular-moduli program (PhaseC-PLAN.md §6.4). It says: an SL(2,ℤ)-invariant, holomorphic function that is meromorphic of finite order at the cusp with coefficients in a subring R ⊆ ℂ equals a polynomial in j of bounded degree with R-coefficients. The proof is a pole-order downward induction with coefficient tracking: the leading Laurent coefficient c lies in R; since j = q⁻¹(1 + 744q + …) is monic with integer q-expansion, h − c·jᴺ has strictly smaller pole order while keeping R-coefficients; the base case N = 0 is bounded + invariant + holomorphic, hence constant (Liouville).

Cusp-meromorphy data

We package "meromorphic at the cusp, pole order ≤ N, coefficients in R" as the property that τ ↦ h τ · q τ ^ N is a genuine holomorphic q-expansion function (1-periodic on the disc side, holomorphic on ℍ, bounded at i∞) whose q-expansion has all coefficients in R. Then h = q⁻ᴺ · (that holomorphic function) is exactly a Laurent series of pole order ≤ N with R-coefficients.

structure Chudnovsky.IsCuspMeroR (h : UpperHalfPlane → ℂ) (N : ℕ) (R : Subring ℂ) : Prop

h is cusp-meromorphic of pole order ≤ N with R-coefficients: the product h · qᴺ is a holomorphic function with a q-expansion whose coefficients all lie in the subring R ⊆ ℂ.

• periodic : Function.Periodic ((fun (τ : UpperHalfPlane) => h τ * q τ ^ N) ∘ ↑UpperHalfPlane.ofComplex) 1
• holo : MDiff fun (τ : UpperHalfPlane) => h τ * q τ ^ N
• bdd : UpperHalfPlane.IsBoundedAtImInfty fun (τ : UpperHalfPlane) => h τ * q τ ^ N
• coeff_mem (n : ℕ) : (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 fun (τ : UpperHalfPlane) => h τ * q τ ^ N) ∈ R

noncomputable def Chudnovsky.cuspLeadCoeff (h : UpperHalfPlane → ℂ) (N : ℕ) : ℂ

The leading Laurent coefficient of a cusp-meromorphic function of pole order ≤ N: the constant q-expansion coefficient of h · qᴺ (i.e. the coefficient of q⁻ᴺ in h).

Equations

• Chudnovsky.cuspLeadCoeff h N = (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 fun (τ : UpperHalfPlane) => h τ * Chudnovsky.q τ ^ N)

theorem Chudnovsky.liouvilleBaseCase (R : Subring ℂ) (h : UpperHalfPlane → ℂ) (hinv : ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane), h (γ • τ) = h τ) (hholo : MDiff h) (hmero : IsCuspMeroR h 0 R) : ∃ c ∈ R, ∀ (τ : UpperHalfPlane), h τ = c

Liouville base case (analytic gate 1 — now discharged). A holomorphic, SL(2,ℤ)-invariant function on ℍ that is cusp-meromorphic of pole order ≤ 0 with R-coefficients (i.e. 1-periodic, holomorphic and bounded at i∞, its q-expansion having coefficients in R) is constant, and its value is the q-expansion constant term, which lies in R.

Route (maximum modulus, PhaseC-PLAN.md §6.4). Descend to the unit disc via the cusp function H := cuspFunction 1 h, which is analytic on Metric.ball 0 1 (differentiableOn_cuspFunction_ball) and satisfies H (q τ) = h τ (eq_cuspFunction). By SL(2,ℤ)-invariance and the fundamental-domain reduction ModularGroup.exists_smul_mem_fd, every value H z on the punctured disc is matched in modulus by a value H w with ‖w‖ ≤ e^{-π}: the pre-image τ of z ≠ 0 moves into 𝒟, where 3 ≤ 4·(Im)² forces Im ≥ 1/2 and hence ‖q‖ ≤ e^{-π}. The maximum-modulus principle in the form Complex.eq_const_of_exists_le then makes H constant on the whole disc, so h τ = H 0; and H 0 = (qExpansion 1 h).coeff 0 ∈ R by cuspFunction_apply_zero / qExpansion_coeff_zero.

theorem Chudnovsky.Sk_eq_poly_j (base : ∀ (R : Subring ℂ) (h : UpperHalfPlane → ℂ), (∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane), h (γ • τ) = h τ) → MDiff h → IsCuspMeroR h 0 R → ∃ c ∈ R, ∀ (τ : UpperHalfPlane), h τ = c) (step : ∀ (N : ℕ) (R : Subring ℂ) (h : UpperHalfPlane → ℂ), (∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane), h (γ • τ) = h τ) → MDiff h → IsCuspMeroR h (N + 1) R → IsCuspMeroR (fun (τ : UpperHalfPlane) => h τ - cuspLeadCoeff h (N + 1) * j τ ^ (N + 1)) N R) (N : ℕ) (R : Subring ℂ) (h : UpperHalfPlane → ℂ) : (∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane), h (γ • τ) = h τ) → MDiff h → IsCuspMeroR h N R → ∃ (P : Polynomial ℂ), (∀ (i : ℕ), P.coeff i ∈ R) ∧ P.natDegree ≤ N ∧ ∀ (τ : UpperHalfPlane), h τ = Polynomial.eval (j τ) P

The q-expansion principle (critical lemma Sk_eq_poly_j), gated on the two analytic primitives. Any SL(2,ℤ)-invariant holomorphic function h that is cusp-meromorphic of pole order ≤ N with R-coefficients equals a polynomial in j of degree ≤ N with all coefficients in the subring R. The pole-order downward induction with coefficient tracking is proved here in full; the two genuinely-analytic inputs — the Liouville base case (base) and the removable-singularity pole-reduction step (step) — are taken as hypotheses (see the TODO blocks above for their routes).

theorem Chudnovsky.Sk_eq_poly_j_of_step (step : ∀ (N : ℕ) (R : Subring ℂ) (h : UpperHalfPlane → ℂ), (∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane), h (γ • τ) = h τ) → MDiff h → IsCuspMeroR h (N + 1) R → IsCuspMeroR (fun (τ : UpperHalfPlane) => h τ - cuspLeadCoeff h (N + 1) * j τ ^ (N + 1)) N R) (N : ℕ) (R : Subring ℂ) (h : UpperHalfPlane → ℂ) : (∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane), h (γ • τ) = h τ) → MDiff h → IsCuspMeroR h N R → ∃ (P : Polynomial ℂ), (∀ (i : ℕ), P.coeff i ∈ R) ∧ P.natDegree ≤ N ∧ ∀ (τ : UpperHalfPlane), h τ = Polynomial.eval (j τ) P

The q-expansion principle with the Liouville base case discharged. Since liouvilleBaseCase closes the base-case gate of Sk_eq_poly_j, only the pole-reduction / removable-singularity step step remains as a hypothesis: any SL(2,ℤ)-invariant holomorphic h that is cusp-meromorphic of pole order ≤ N with R-coefficients equals a degree-≤ N polynomial in j with coefficients in R.

(B5) Assembly: the modular polynomial Φ_m ∈ ℚ[X][Y]

The SL(2,ℤ)-invariant coefficients of orbitPoly m τ = ∏_i (X − f_i τ) are the elementary symmetric functions of the orbit. Feeding each (via Newton's identities from the power sums, plus Sk_eq_poly_j) to the q-expansion principle expresses it as a ℚ-polynomial in j. Packaging those ℚ-polynomials as the Y-coefficients yields Φ_m ∈ ℚ[Y][X] with the defining identity Φ_m(X, j τ) = ∏_i (X − f_i τ).

Here we deliver the final packaging step unconditionally: given the per-coefficient ℚ-rationality (hrat, the output of (B3) + Sk_eq_poly_j), we build Φ_m and prove the identity.

noncomputable def Chudnovsky.specializeY (Y₀ : ℂ) : Polynomial (Polynomial ℚ) →+* Polynomial ℂ

Specialization of a ℚ[Y][X]-polynomial at Y = Y₀ ∈ ℂ: map each ℚ[Y]-coefficient to its value at Y₀, landing in ℂ[X]. Applied at Y₀ = j τ this is Φ_m(X, j τ).

Equations

• Chudnovsky.specializeY Y₀ = Polynomial.mapRingHom (Polynomial.aeval Y₀).toRingHom

theorem Chudnovsky.orbitPoly_natDegree_le {m : ℕ} [NeZero m] (τ : UpperHalfPlane) : (orbitPoly m τ).natDegree ≤ m + 1

The degree of the orbit polynomial is at most m + 1 (it is the product of m + 1 linear factors).

theorem Chudnovsky.exists_PhiQ {m : ℕ} [Fact (Nat.Prime m)] (hrat : ∀ (n : ℕ), ∃ (Q : Polynomial ℚ), ∀ (τ : UpperHalfPlane), (orbitPoly m τ).coeff n = (Polynomial.aeval (j τ)) Q) : ∃ (PhiQ : Polynomial (Polynomial ℚ)), ∀ (τ : UpperHalfPlane), orbitPoly m τ = (specializeY (j τ)) PhiQ

The modular polynomial Φ_m ∈ ℚ[Y][X], assembled from the per-coefficient ℚ-rationality. Given that each coefficient of ∏_i (X − f_i τ) is a ℚ-polynomial in j τ (the output of (B3) + Sk_eq_poly_j), there is Φ_m ∈ ℚ[Y][X] with the keystone identity ∏_i (X − f_i τ) = Φ_m(X, j τ) for every τ. This is the object consumed by ModularPolynomialZ.lean / Rationality.lean / MasserA1.lean.

Analytic gate 2 (pole reduction): poleReduction

This appended section discharges the step hypothesis of Sk_eq_poly_j — the removable-singularity / pole-order-reduction step. Given h cusp-meromorphic of pole order ≤ N+1 with R-coefficients and leading Laurent coefficient c = cuspLeadCoeff h (N+1), the function h − c·j^{N+1} is cusp-meromorphic of pole order ≤ N with R-coefficients.

The analytic heart is the general lemma divByQ: if F is a holomorphic q-expansion function whose expansion has zero constant term, then F/q is again such a function, with q-expansion coefficients shifted down by one (dslope/removable-singularity at the cusp). The algebraic heart (j·q has integer q-expansion with leading coefficient 1, so the q^{-(N+1)} term cancels and all coefficients stay in R) is done via the qExpansion ring-hom API from JFunction.lean.

theorem Chudnovsky.qExpansion_coeff_unique_raw {F : UpperHalfPlane → ℂ} {c : ℕ → ℂ} (hFan : AnalyticAt ℂ (UpperHalfPlane.cuspFunction 1 F) 0) (hFper : Function.Periodic (F ∘ ↑UpperHalfPlane.ofComplex) 1) (hFholo : MDiff F) (hFbdd : UpperHalfPlane.IsBoundedAtImInfty F) (hF : ∀ (τ : UpperHalfPlane), HasSum (fun (n : ℕ) => c n • q τ ^ n) (F τ)) (n : ℕ) : c n = (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 F)

Raw-function version of qExpansion_coeff_unique: if cuspFunction 1 F is analytic at 0 and F τ = ∑ c n · q τ ^ n for all τ, then c n is the n-th q-expansion coefficient.

theorem Chudnovsky.cuspFunction_one_eq : UpperHalfPlane.cuspFunction 1 1 = 1

The cusp function of the constant function 1 is the constant function 1.

theorem Chudnovsky.qExpansion_pow_of_analytic {F : UpperHalfPlane → ℂ} (hF : AnalyticAt ℂ (UpperHalfPlane.cuspFunction 1 F) 0) (n : ℕ) : AnalyticAt ℂ (UpperHalfPlane.cuspFunction 1 (F ^ n)) 0 ∧ UpperHalfPlane.qExpansion 1 (F ^ n) = UpperHalfPlane.qExpansion 1 F ^ n

Powers preserve cusp-analyticity, and the q-expansion of a power is the power of the q-expansion.

theorem Chudnovsky.divByQ {F G : UpperHalfPlane → ℂ} (hFper : Function.Periodic (F ∘ ↑UpperHalfPlane.ofComplex) 1) (hFholo : MDiff F) (hFbdd : UpperHalfPlane.IsBoundedAtImInfty F) (hF0 : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 F) = 0) (hGper : Function.Periodic (G ∘ ↑UpperHalfPlane.ofComplex) 1) (hGholo : MDiff G) (hGF : ∀ (τ : UpperHalfPlane), G τ * q τ = F τ) : UpperHalfPlane.IsBoundedAtImInfty G ∧ ∀ (n : ℕ), (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 G) = (PowerSeries.coeff (n + 1)) (UpperHalfPlane.qExpansion 1 F)

The pole-reduction primitive. If F is 1-periodic, holomorphic and bounded at i∞, its q-expansion has zero constant term, and G·q = F, then G is bounded at i∞ and its q-expansion is that of F shifted down by one coefficient. Proof: G τ = dslope (cuspFunction 1 F) 0 (q τ), which is analytic/continuous at 0 since cuspFunction 1 F 0 = 0 (removable singularity); boundedness follows by continuity, and the coefficient shift from the HasSum expansion of F after dividing by q.

theorem Chudnovsky.poleReduction (N : ℕ) (R : Subring ℂ) (h : UpperHalfPlane → ℂ) (hinv : ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane), h (γ • τ) = h τ) (hholo : MDiff h) (hmero : IsCuspMeroR h (N + 1) R) : IsCuspMeroR (fun (τ : UpperHalfPlane) => h τ - cuspLeadCoeff h (N + 1) * j τ ^ (N + 1)) N R

Analytic gate 2 — the pole-reduction step of Sk_eq_poly_j. Subtracting the leading Laurent term c·j^{N+1} (with c = cuspLeadCoeff h (N+1)) from a pole-order-(N+1) cusp-meromorphic function of R-coefficients yields a pole-order-N one, still with R-coefficients. This closes the step hypothesis of Sk_eq_poly_j.

theorem Chudnovsky.Sk_eq_poly_j_closed (N : ℕ) (R : Subring ℂ) (h : UpperHalfPlane → ℂ) : (∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane), h (γ • τ) = h τ) → MDiff h → IsCuspMeroR h N R → ∃ (P : Polynomial ℂ), (∀ (i : ℕ), P.coeff i ∈ R) ∧ P.natDegree ≤ N ∧ ∀ (τ : UpperHalfPlane), h τ = Polynomial.eval (j τ) P

The q-expansion principle, fully unconditional. Both analytic gates of Sk_eq_poly_j are now discharged — the Liouville base case (liouvilleBaseCase) and the pole-reduction step (poleReduction) — so an SL(2,ℤ)-invariant holomorphic h that is cusp-meromorphic of pole order ≤ N with R-coefficients equals a degree-≤ N polynomial in j with R-coefficients, with no remaining hypotheses.

(B3) The power sums are cusp-meromorphic with ℚ-coefficients

This appended section discharges the last remaining gate of the keystone: the hrat input of exists_PhiQ. For a prime m, every power sum powerSum m k is SL(2,ℤ)-invariant, holomorphic and cusp-meromorphic of pole order ≤ m·k with ℚ (indeed ℤ)-coefficients, hence (via Sk_eq_poly_j_closed) a ℚ-polynomial in j. Newton's identities then push this to the elementary symmetric functions (the orbit-polynomial coefficients), delivering the unconditional keystone exists_PhiQ_closed.

The analytic heart is the root-of-unity averaging sum_zetaM_zpow_mul: writing each orbit value's q-expansion in the honest base variable w = wParam m τ (with w^m = q τ), the coset points contribute w-powers ζ^{b·n} whose b-sum collapses to a genuine q-Laurent series.

noncomputable def Chudnovsky.RQ : Subring ℂ

The subring ℚ ⊆ ℂ (image of the rational cast).

Equations

• Chudnovsky.RQ = (Rat.castHom ℂ).range

theorem Chudnovsky.intCast_mem_RQ (n : ℤ) : ↑n ∈ RQ

theorem Chudnovsky.wParam_pow_mk {m : ℕ} [NeZero m] (k : ℕ) (τ : UpperHalfPlane) : wParam m τ ^ (m ^ 2 * k) = q τ ^ (m * k)

w^{m²·k} = q^{m·k}: the top w-power equals the q-power that clears the pole.

theorem Chudnovsky.hasSum_jqPow_at (k : ℕ) (σ : UpperHalfPlane) : HasSum (fun (n : ℕ) => ↑((PowerSeries.coeff n) (jqInt ^ k)) * q σ ^ n) ((j σ * q σ) ^ k)

Per-point k-fold q-expansion of j·q. For any σ : ℍ, (j σ · q σ)^k = ∑ₙ (jqInt^k)ₙ · q σ ^ n with the integer coefficients of jqInt^k.

theorem Chudnovsky.norm_wParam_le_one {m : ℕ} [NeZero m] (τ : UpperHalfPlane) : ‖wParam m τ‖ ≤ 1

‖wParam m τ‖ ≤ 1 (since ‖wParam‖^m = ‖q τ‖ < 1).

theorem Chudnovsky.norm_zetaM_eq_one {m : ℕ} [NeZero m] : ‖zetaM m‖ = 1

‖zetaM m‖ = 1 (a root of unity).

theorem Chudnovsky.norm_gB_le_one {m : ℕ} [NeZero m] (k : ℕ) (b : ZMod m) (τ : UpperHalfPlane) : ‖zetaM m ^ (-(↑b.val * ↑k)) * wParam m τ ^ ((m ^ 2 - 1) * k)‖ ≤ 1

‖gB‖ ≤ 1, where gB is the bounded multiplier appearing in the some b orbit term.

theorem Chudnovsky.Fi_none_eq {m : ℕ} [NeZero m] (k : ℕ) (τ : UpperHalfPlane) : f m none τ ^ k * q τ ^ (m * k) = (j (AInf m • τ) * q (AInf m • τ)) ^ k

The none orbit term of powerSum·q^{mk} is (j·q)ᵏ composed with the isogeny τ ↦ m·τ.

theorem Chudnovsky.Fi_some_eq {m : ℕ} [NeZero m] (k : ℕ) (b : ZMod m) (τ : UpperHalfPlane) : f m (some b) τ ^ k * q τ ^ (m * k) = (j (Acol m ↑b.val • τ) * q (Acol m ↑b.val • τ)) ^ k * (zetaM m ^ (-(↑b.val * ↑k)) * wParam m τ ^ ((m ^ 2 - 1) * k))

The some b orbit term of powerSum·q^{mk} factors as (j·q)ᵏ∘(coset) · gB with ‖gB‖≤1.

theorem Chudnovsky.isBoundedAtImInfty_of_norm_le_one {g : UpperHalfPlane → ℂ} (hg : ∀ (τ : UpperHalfPlane), ‖g τ‖ ≤ 1) : UpperHalfPlane.IsBoundedAtImInfty g

A function bounded by 1 in norm is bounded at i∞.

theorem Chudnovsky.isBoundedAtImInfty_jqPow_comp (k : ℕ) (A : GL (Fin 2) ℝ) (hA : ↑A 1 0 = 0) : UpperHalfPlane.IsBoundedAtImInfty fun (τ : UpperHalfPlane) => (j (A • τ) * q (A • τ)) ^ k

(j·q)ᵏ composed with an upper-triangular isogeny A (lower-left entry 0) is bounded at i∞, since the isogeny pushes towards the cusp.

theorem Chudnovsky.isBoundedAtImInfty_powerSum_mul_qpow {m : ℕ} [Fact (Nat.Prime m)] (k : ℕ) : UpperHalfPlane.IsBoundedAtImInfty fun (τ : UpperHalfPlane) => powerSum m k τ * q τ ^ (m * k)

Boundedness at the cusp. powerSum m k · q^{mk} is bounded at i∞: each orbit term is a bounded (j·q)ᵏ-value (composed with an isogeny) times a factor of norm ≤ 1.

The averaging: q-series of the some b orbit terms

theorem Chudnovsky.coset_summand_eq {m : ℕ} [NeZero m] (k : ℕ) (b : ZMod m) (τ : UpperHalfPlane) (n : ℕ) : ↑((PowerSeries.coeff n) (jqInt ^ k)) * (zetaM m ^ ↑b.val * wParam m τ) ^ n * (zetaM m ^ (-(↑b.val * ↑k)) * wParam m τ ^ ((m ^ 2 - 1) * k)) = ↑((PowerSeries.coeff n) (jqInt ^ k)) * zetaM m ^ (↑b.val * (↑n - ↑k)) * wParam m τ ^ ((m ^ 2 - 1) * k + n)

The summand identity feeding the root-of-unity average: the n-th term of the some b orbit q-expansion, rewritten so the b-dependence is exactly ζ^{b·(n-k)}.

theorem Chudnovsky.hasSum_coset_some {m : ℕ} [NeZero m] (k : ℕ) (b : ZMod m) (τ : UpperHalfPlane) : HasSum (fun (n : ℕ) => ↑((PowerSeries.coeff n) (jqInt ^ k)) * zetaM m ^ (↑b.val * (↑n - ↑k)) * wParam m τ ^ ((m ^ 2 - 1) * k + n)) (f m (some b) τ ^ k * q τ ^ (m * k))

Per-coset q-expansion of the some b orbit term. After multiplying (j·q)ᵏ∘(coset) by the pole-clearing factor, the n-th coefficient carries the b-dependence ζ^{b·(n-k)}.

noncomputable def Chudnovsky.CAint (m k p : ℕ) : ℤ

Integer q-coefficients of the averaged coset contribution ∑_b (f_b)ᵏ·q^{mk}.

Equations

• Chudnovsky.CAint m k p = if (m ^ 2 - 1) * k ≤ m * p then ↑m * (PowerSeries.coeff (m * p - (m ^ 2 - 1) * k)) (Chudnovsky.jqInt ^ k) else 0

noncomputable def Chudnovsky.CIint (m k p : ℕ) : ℤ

Integer q-coefficients of the ∞-coset contribution (f_∞)ᵏ·q^{mk}.

Equations

• Chudnovsky.CIint m k p = if m ∣ p then (PowerSeries.coeff (p / m)) (Chudnovsky.jqInt ^ k) else 0

theorem Chudnovsky.aux_kadd {m : ℕ} [NeZero m] (k : ℕ) : k + (m ^ 2 - 1) * k = m ^ 2 * k

theorem Chudnovsky.hasSum_I {m : ℕ} [NeZero m] (k : ℕ) (τ : UpperHalfPlane) : HasSum (fun (p : ℕ) => ↑(CIint m k p) * q τ ^ p) (f m none τ ^ k * q τ ^ (m * k))

q-expansion of the ∞-coset term. (f_∞)ᵏ·q^{mk} is the honest q-series with integer coefficients CIint.

theorem Chudnovsky.cast_c {m : ℕ} [NeZero m] (k : ℕ) : ↑((m ^ 2 - 1) * k) = ↑m ^ 2 * ↑k - ↑k

Cast helper: ((m²-1)·k : ℤ) = m²·k − k.

theorem Chudnovsky.hasSum_A {m : ℕ} [NeZero m] (k : ℕ) (τ : UpperHalfPlane) : HasSum (fun (p : ℕ) => ↑(CAint m k p) * q τ ^ p) (∑ b : ZMod m, f m (some b) τ ^ k * q τ ^ (m * k))

q-expansion of the averaged coset contribution ∑_b (f_b)ᵏ·q^{mk}. The root-of-unity average sum_zetaM_zpow_mul collapses the b-dependence, leaving an honest q-series with integer coefficients CAint.

noncomputable def Chudnovsky.Cq (m k p : ℕ) : ℤ

Integer q-coefficients of powerSum·q^{mk}.

Equations

• Chudnovsky.Cq m k p = Chudnovsky.CAint m k p + Chudnovsky.CIint m k p

theorem Chudnovsky.hasSum_powerSum_mul_qpow {m : ℕ} [Fact (Nat.Prime m)] (k : ℕ) (τ : UpperHalfPlane) : HasSum (fun (p : ℕ) => ↑(Cq m k p) * q τ ^ p) (powerSum m k τ * q τ ^ (m * k))

The full q-series for powerSum·q^{mk}.

theorem Chudnovsky.powerSum_isCuspMeroR {m : ℕ} [Fact (Nat.Prime m)] (k : ℕ) : IsCuspMeroR (powerSum m k) (m * k) RQ

(B3) The power sums are cusp-meromorphic of pole order ≤ m·k with ℚ-coefficients.

theorem Chudnovsky.powerSum_eq_aeval_j {m : ℕ} [Fact (Nat.Prime m)] (k : ℕ) : ∃ (Q : Polynomial ℚ), ∀ (τ : UpperHalfPlane), powerSum m k τ = (Polynomial.aeval (j τ)) Q

(B3) conclusion: each power sum of the coset orbit is a ℚ-polynomial in j.

(B4/B5) Newton's identities: the orbit-polynomial coefficients are ℚ-polynomials in j

noncomputable def Chudnovsky.polyJ : Subalgebra ℚ (UpperHalfPlane → ℂ)

The ℚ-subalgebra of ℍ → ℂ of functions that are ℚ-polynomials in j.

Equations

• Chudnovsky.polyJ = (Polynomial.aeval fun (τ : UpperHalfPlane) => Chudnovsky.j τ).range

theorem Chudnovsky.aeval_j_apply (Q : Polynomial ℚ) (τ : UpperHalfPlane) : (Polynomial.aeval fun (τ : UpperHalfPlane) => j τ) Q τ = (Polynomial.aeval (j τ)) Q

Evaluating aeval (τ ↦ j τ) Q at a point τ gives aeval (j τ) Q.

theorem Chudnovsky.mem_polyJ_iff {g : UpperHalfPlane → ℂ} : g ∈ polyJ ↔ ∃ (Q : Polynomial ℚ), ∀ (τ : UpperHalfPlane), g τ = (Polynomial.aeval (j τ)) Q

theorem Chudnovsky.powerSum_mem_polyJ {m : ℕ} [Fact (Nat.Prime m)] (l : ℕ) : powerSum m l ∈ polyJ

Each power sum lies in polyJ.

noncomputable def Chudnovsky.esf (m : ℕ) [NeZero m] (l : ℕ) (τ : UpperHalfPlane) : ℂ

The elementary symmetric functions of the orbit values, as functions of τ.

Equations

• Chudnovsky.esf m l τ = (MvPolynomial.aeval fun (i : Option (ZMod m)) => Chudnovsky.f m i τ) (MvPolynomial.esymm (Option (ZMod m)) ℂ l)

theorem Chudnovsky.aeval_psum_eq_powerSum {m : ℕ} [NeZero m] (l : ℕ) (τ : UpperHalfPlane) : (MvPolynomial.aeval fun (i : Option (ZMod m)) => f m i τ) (MvPolynomial.psum (Option (ZMod m)) ℂ l) = powerSum m l τ

aeval of a power sum polynomial is the orbit power sum.

theorem Chudnovsky.newton_esf {m : ℕ} [NeZero m] (l : ℕ) (τ : UpperHalfPlane) : ↑l * esf m l τ = (-1) ^ (l + 1) * ∑ a ∈ Finset.antidiagonal l with a.1 < l, (-1) ^ a.1 * esf m a.1 τ * powerSum m a.2 τ

Newton's identity for the orbit (pointwise), obtained by evaluating MvPolynomial.mul_esymm_eq_sum at the orbit values.

theorem Chudnovsky.algebraMap_polyJ_apply (c : ℚ) (τ : UpperHalfPlane) : (algebraMap ℚ (UpperHalfPlane → ℂ)) c τ = ↑c

algebraMap ℚ (ℍ → ℂ) evaluated at τ is the rational cast.

theorem Chudnovsky.esf_mem_polyJ {m : ℕ} [Fact (Nat.Prime m)] (l : ℕ) : (fun (τ : UpperHalfPlane) => esf m l τ) ∈ polyJ

Each elementary symmetric function of the orbit lies in polyJ (Newton induction).

theorem Chudnovsky.orbitPoly_coeff_mem_polyJ {m : ℕ} [Fact (Nat.Prime m)] (n : ℕ) : (fun (τ : UpperHalfPlane) => (orbitPoly m τ).coeff n) ∈ polyJ

Each coefficient of the orbit polynomial lies in polyJ.

theorem Chudnovsky.exists_PhiQ_closed {m : ℕ} [Fact (Nat.Prime m)] : ∃ (PhiQ : Polynomial (Polynomial ℚ)), ∀ (τ : UpperHalfPlane), orbitPoly m τ = (specializeY (j τ)) PhiQ

The unconditional keystone. For a prime m, the modular polynomial Φ_m ∈ ℚ[Y][X] exists with the defining identity ∏_i (X − f_i τ) = Φ_m(X, j τ) for every τ. All analytic gates are discharged: the hrat input is now proved via the (B3) root-of-unity averaging, Sk_eq_poly_j_closed, and Newton's identities.