The modular polynomial Φ_m ∈ ℤ[X, Y] and Kronecker's lemma (Phase C, chunks B6–B7)

Fourth file of Track 1 of Phase C (see Playground/Pi/PhaseC-PLAN.md, §3.1 sub-lemmas (B6)–(B7)). It refines the ℚ-coefficient modular polynomial of ModularPolynomialQ.lean to a ℤ-coefficient one (needed for m = 41, the smallest usable index), and packages Kronecker's unit-leading-coefficient lemma into the form Integrality.lean consumes.

What is delivered

• (ℤ[ζ_m] ∩ ℚ = ℤ) isInt_of_integral_of_rat / mem_bot_of_integral_of_rat: a self-contained algebra tool — a complex number that is both rational and an algebraic integer lies in the image of ℤ (i.e. in the bottom subring ⊥ ⊆ ℂ). This is the pointwise mechanism by which the ℤ[ζ_m]-integrality of the un-averaged w-expansion coefficients, once combined with the rationality of the averaged q-coefficients (the (B3)/Sk_eq_poly_j output), upgrades a coefficient from ℚ to ℤ. Provided now, standalone.

• (B6) exists_PhiZ: given that each coefficient of the orbit polynomial ∏_i (X − f_i τ) is cusp-meromorphic of finite order with coefficients in ⊥ (the hypothesis hZ, mirroring the hrat gate of ModularPolynomialQ.lean's exists_PhiQ, but with the integer subring ⊥ in place of a ℚ-subring — the hrat-closing machinery yields both, since the coefficient-tracking of Sk_eq_poly_j is generic in the subring R), the file produces PhiZ : Polynomial (Polynomial ℤ) with the keystone identity ∏_i (X − f_i τ) = Φ_m(X, j τ) (orbitPoly m τ = specializeZ (j τ) PhiZ). The proof runs the unconditional Sk_eq_poly_j_closed at R = ⊥ and lifts each ⊥-coefficient polynomial to ℤ.

• API for Rationality.lean / MasserA1.lean / Integrality.lean:

  • orbitPoly_eval_eq_prod : (∏_i (X − f_i τ)).eval z = ∏_i (z − f_i τ);
  • PhiQ_eval_j_root (the bridge §4.2/§5 consume): if j σ = f m i τ for some coset index i, then Φ_m(j σ, j τ) = 0 — one factor of the orbit product vanishes. Stated against an abstract PhiQ + its defining identity, so that plugging in the parallel agent's exists_PhiQ_closed is a three-line follow-up;
  • diagPhiZ and diagPhiZ_map_eval : the diagonal polynomial G_m(X) := Φ_m(X, X) ∈ ℤ[X] with G_m(j τ) = ∏_i (j τ − f_i τ);
  • isIntegral_of_kronecker : the (B9) bridge — if G_m has leading coefficient ±1 (Kronecker) and j τ is a root of G_m (a CM relation), then IsIntegral ℤ (j τ).

Status of the two remaining deep inputs (zero sorry)

1. DISCHARGED (see the appended w-expansion section, orbitPoly_coeff_isCuspMeroR_bot, yielding exists_PhiZ_closed). The ⊥-coefficient cusp-meromorphy hypothesis hZ of exists_PhiZ was originally taken as an argument; it is now closed unconditionally. Route (per PhaseC-PLAN.md §3.1 (B6)): each q-expansion coefficient of (orbitPoly m τ).coeff n · qᴺ is (i) rational — the (B3) root-of-unity averaging / Sk_eq_poly_j output, exactly the datum the parallel agent produces for exists_PhiQ; and (ii) an algebraic integer — the un-averaged w = exp(2πiτ/m)-expansion of each orbit piece f_i has coefficients in the subring ℤ[ζ_m] ⊆ ℂ (substitute q ↦ ζ^{b}·wⁿ into jqInt's integer coefficients, hasSum_f_some/hasSum_f_none of CosetOrbit.lean), whose elements are integral over ℤ (ζ_m is a root of unity; the integral elements form a subring). By mem_bot_of_integral_of_rat each coefficient then lies in ⊥. No Galois descent is used — this is the plan's main simplification (§6.6): rationality from averaging, integrality from ring closure, combined pointwise.

2. (B7) Kronecker G_m.leadingCoeff = ±1 is taken as the hypothesis hlead of isIntegral_of_kronecker. Route (per PhaseC-PLAN.md §3.1 (B7); m non-square, here the prime 41): the product D(τ) = ∏_i (j τ − f_i τ) = G_m(j τ) has a leading q-Laurent term computable from the w-expansions of CosetOrbit.lean. With q = wᵐ: j ~ w^{-m} (leading coeff 1, from jqInt.coeff 0 = 1), f_b ~ ζ^{-b} w^{-1} (from hasSum_f_some, jqInt.coeff 0 = 1), f_∞ ~ w^{-m²} (from hasSum_f_none). As m ≥ 2: j − f_b ~ w^{-m} (leading coeff 1) and j − f_∞ ~ −w^{-m²} (leading coeff −1); the product is −w^{-2m²}·(1 + O(w)) = −q^{-2m}·(1 + …), so D ~ −(j)^{2m}. Since G_m(j τ) = D(τ) and j has a simple pole with leading coefficient 1, matching the most negative q-powers gives natDegree G_m = 2m and G_m.leadingCoeff = −1 (a ±1, up to the sign bookkeeping ζ^{−Σb} = ζ^{−m(m−1)/2} = 1 for m odd). Formalizing the leading-term extraction of the product D and matching against ∑ a_r (j)^r is the cuspLeadCoeff-level work flagged in the plan (§6.3, "ModularPolynomialZ + Kronecker", medium risk). Everything downstream of ±1 (the monic-up-to-sign annihilator ⇒ IsIntegral) is proved here in full, so once the extraction lands, hlead is discharged and Integrality.lean closes.

The (B8) CM relation ∃ i, j τ₁₆₃ = f m i τ₁₆₃ that feeds both the root bridge and Kronecker lives in CMRelations.lean (a two-line Möbius computation), consumed via diagPhiZ_eval_eq_zero / PhiQ_eval_j_root.

(ℤ[ζ_m] ∩ ℚ = ℤ) : rational + algebraic-integer ⇒ integer

The self-contained algebra tool. A complex number that is rational and integral over ℤ is an integer (IsIntegrallyClosed for ℤ ⊆ ℚ); packaged as membership in the bottom subring ⊥ ⊆ ℂ (which, by Subring.mem_bot, is exactly the image of ℤ). Re-derived from Mathlib here (the identical fact is private in Coefficients.lean).

theorem Chudnovsky.isInt_of_integral_of_rat {x : ℂ} (hint : IsIntegral ℤ x) {r : ℚ} (hr : x = ↑r) : ∃ (m : ℤ), x = ↑m

Rational algebraic integer is an integer. If x : ℂ is integral over ℤ and equals a rational r, then x = (m : ℂ) for some m : ℤ.

theorem Chudnovsky.mem_bot_of_integral_of_rat {x : ℂ} (hint : IsIntegral ℤ x) (hrat : ∃ (r : ℚ), x = ↑r) : x ∈ ⊥

ℤ[ζ_m] ∩ ℚ = ℤ, packaged. A complex number that is integral over ℤ (e.g. an element of ℤ[ζ_m]) and rational lies in the bottom subring ⊥ ⊆ ℂ (the image of ℤ). This is the pointwise upgrade ℚ-coefficient ⇒ ℤ-coefficient of (B6).

Lifting ⊥-coefficient complex polynomials to ℤ

A Polynomial ℂ all of whose coefficients lie in ⊥ (i.e. are integers) is the image of a Polynomial ℤ under Int.castRingHom ℂ.

theorem Chudnovsky.exists_intPoly_of_coeff_mem_bot {P : Polynomial ℂ} (hP : ∀ (i : ℕ), P.coeff i ∈ ⊥) : ∃ (Q : Polynomial ℤ), P = Polynomial.map (Int.castRingHom ℂ) Q

If every coefficient of P : ℂ[X] lies in ⊥ (is an integer), then P = Q.map (ℤ → ℂ) for some Q : ℤ[X].

(B6) The modular polynomial Φ_m ∈ ℤ[Y][X]

The ℤ-analogue of ModularPolynomialQ.lean's specializeY / exists_PhiQ.

noncomputable def Chudnovsky.specializeZ (Y₀ : ℂ) : Polynomial (Polynomial ℤ) →+* Polynomial ℂ

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

Equations

• Chudnovsky.specializeZ Y₀ = Polynomial.mapRingHom (Polynomial.eval₂RingHom (Int.castRingHom ℂ) Y₀)

theorem Chudnovsky.orbitPoly_coeff_intPoly {m : ℕ} [Fact (Nat.Prime m)] (hZ : ∀ (n : ℕ), ∃ (N : ℕ), IsCuspMeroR (fun (τ : UpperHalfPlane) => (orbitPoly m τ).coeff n) N ⊥) (n : ℕ) : ∃ (Q : Polynomial ℤ), ∀ (τ : UpperHalfPlane), (orbitPoly m τ).coeff n = Polynomial.eval₂ (Int.castRingHom ℂ) (j τ) Q

Per-coefficient ℤ-refinement: assuming the coefficient (orbitPoly m τ).coeff n is cusp-meromorphic of finite order with coefficients in ⊥, it equals a ℤ-polynomial in j τ. Uses the unconditional Sk_eq_poly_j_closed at R = ⊥ and lifts the resulting ⊥-coefficient polynomial to ℤ.

theorem Chudnovsky.exists_PhiZ {m : ℕ} [Fact (Nat.Prime m)] (hZ : ∀ (n : ℕ), ∃ (N : ℕ), IsCuspMeroR (fun (τ : UpperHalfPlane) => (orbitPoly m τ).coeff n) N ⊥) : ∃ (PhiZ : Polynomial (Polynomial ℤ)), ∀ (τ : UpperHalfPlane), orbitPoly m τ = (specializeZ (j τ)) PhiZ

(B6) The modular polynomial Φ_m ∈ ℤ[Y][X]. Given the ⊥-coefficient cusp-meromorphy of every orbit-polynomial coefficient (hZ), there is PhiZ : Polynomial (Polynomial ℤ) with the keystone identity ∏_i (X − f_i τ) = Φ_m(X, j τ) for every τ. This is the object consumed by Integrality.lean (through diagPhiZ / Kronecker).

Evaluation of the orbit polynomial and the root bridge

The keystone identity orbitPoly m τ = Φ_m(X, j τ) turns coset coincidences j σ = f_i τ into roots Φ_m(j σ, j τ) = 0. Stated against an abstract PhiQ + its defining property (so the parallel agent's exists_PhiQ_closed, of the same shape as exists_PhiQ, discharges it in three lines), and mirrored for PhiZ.

theorem Chudnovsky.orbitPoly_eval_eq_prod {m : ℕ} [NeZero m] (τ : UpperHalfPlane) (z : ℂ) : Polynomial.eval z (orbitPoly m τ) = ∏ i : Option (ZMod m), (z - f m i τ)

Evaluating the orbit polynomial at z : ℂ gives the product ∏_i (z − f_i τ).

theorem Chudnovsky.orbitPoly_eval_eq_zero {m : ℕ} [NeZero m] {τ σ : UpperHalfPlane} {i : Option (ZMod m)} (h : j σ = f m i τ) : Polynomial.eval (j σ) (orbitPoly m τ) = 0

If j σ = f m i τ for some coset index i, then j σ is a root of the orbit polynomial ∏_i (X − f_i τ).

theorem Chudnovsky.PhiQ_eval_j_root {m : ℕ} [NeZero m] (PhiQ : Polynomial (Polynomial ℚ)) (hPhiQ : ∀ (τ : UpperHalfPlane), orbitPoly m τ = (specializeY (j τ)) PhiQ) {τ σ : UpperHalfPlane} {i : Option (ZMod m)} (h : j σ = f m i τ) : Polynomial.eval (j σ) ((specializeY (j τ)) PhiQ) = 0

The root bridge (§4.2/§5), ℚ-version. If j σ coincides with some coset value f m i τ (a CM relation), then Φ_m(j σ, j τ) = 0. Consumed by Rationality.lean (C2, applied under a field embedding σ : ℚ(j₀) → ℂ) and MasserA1.lean (F(z) = Φ₁₆₃(j(Λz), j z) ≡ 0).

Stated against an abstract PhiQ : Polynomial (Polynomial ℚ) together with its defining identity hPhiQ — exactly the pair produced by ModularPolynomialQ.exists_PhiQ; supply the parallel agent's exists_PhiQ_closed to obtain it unconditionally.

(B7) The diagonal polynomial G_m(X) = Φ_m(X, X) and Kronecker's lemma

noncomputable def Chudnovsky.diagPhiZ (PhiZ : Polynomial (Polynomial ℤ)) : Polynomial ℤ

The diagonal polynomial G_m(X) := Φ_m(X, X) ∈ ℤ[X], obtained by substituting the coefficient variable Y by the outer variable X (evaluating the outer PhiZ at X : ℤ[X]).

Equations

• Chudnovsky.diagPhiZ PhiZ = Polynomial.eval Polynomial.X PhiZ

theorem Chudnovsky.diag_eval₂_eq (PhiZ : Polynomial (Polynomial ℤ)) (z : ℂ) : Polynomial.eval₂ (Int.castRingHom ℂ) z (Polynomial.eval Polynomial.X PhiZ) = Polynomial.eval z ((specializeZ z) PhiZ)

The diagonal substitution commutes with Y ↦ z: evaluating G_m (mapped to ℂ) at z equals evaluating Φ_m(X, z) at z. Both are the two ways to compute Φ_m(z, z).

theorem Chudnovsky.diagPhiZ_map_eval {m : ℕ} [NeZero m] {PhiZ : Polynomial (Polynomial ℤ)} (hPhiZ : ∀ (τ : UpperHalfPlane), orbitPoly m τ = (specializeZ (j τ)) PhiZ) (τ : UpperHalfPlane) : Polynomial.eval₂ (Int.castRingHom ℂ) (j τ) (diagPhiZ PhiZ) = ∏ i : Option (ZMod m), (j τ - f m i τ)

G_m(j τ) = ∏_i (j τ − f_i τ). Evaluating the diagonal polynomial (mapped to ℂ) at j τ recovers the orbit product. The bridge Kronecker / Integrality.lean extract from.

theorem Chudnovsky.diagPhiZ_eval_eq_zero {m : ℕ} [NeZero m] {PhiZ : Polynomial (Polynomial ℤ)} (hPhiZ : ∀ (τ : UpperHalfPlane), orbitPoly m τ = (specializeZ (j τ)) PhiZ) {τ : UpperHalfPlane} {i : Option (ZMod m)} (h : j τ = f m i τ) : Polynomial.eval₂ (Int.castRingHom ℂ) (j τ) (diagPhiZ PhiZ) = 0

The diagonal CM root. If j τ = f m i τ for some coset index i (a fixing relation at a CM point), then j τ is a root of G_m (mapped to ℂ). Combined with Kronecker's ±1 leading coefficient this yields integrality.

theorem Chudnovsky.isIntegral_of_kronecker {m : ℕ} [NeZero m] {PhiZ : Polynomial (Polynomial ℤ)} (hlead : (diagPhiZ PhiZ).leadingCoeff = 1 ∨ (diagPhiZ PhiZ).leadingCoeff = -1) {τ : UpperHalfPlane} (hroot : Polynomial.eval₂ (Int.castRingHom ℂ) (j τ) (diagPhiZ PhiZ) = 0) : IsIntegral ℤ (j τ)

(B9) The integrality bridge. If G_m = Φ_m(X, X) has leading coefficient ±1 (Kronecker's lemma, (B7) — the gated input, see the module TODO) and j τ is a root of G_m (a CM relation (B8), from CMRelations.lean via diagPhiZ_eval_eq_zero), then j τ is integral over ℤ. This is exactly the shape Integrality.lean needs for isIntegral_j_τ₁₆₃ at m = 41. The ±1 monic-up-to-sign annihilator argument is proved here in full.

Discharging the hZ gate of exists_PhiZ: the w-expansion integrality machinery

This appended section closes the hZ hypothesis of exists_PhiZ unconditionally, yielding exists_PhiZ_closed. Each q-coefficient of (orbitPoly m τ).coeff n · qᴺ is (i) rational (the ℚ-averaging of ModularPolynomialQ.lean, via a generic qExpansion-ring-hom toolkit GoodQ) and (ii) an algebraic integer (the un-averaged width-m w = wParam m-expansion of ∏_i (X − f_i) has coefficients in ℤ[ζ_m], matched to the q-coefficient at index m·p by a width-m uniqueness argument). By mem_bot_of_integral_of_rat each coefficient lies in ⊥.

structure Chudnovsky.GoodQ (h : ℝ) (R : Subring ℂ) (g : UpperHalfPlane → ℂ) : Prop

Cusp-analytic with q-expansion coefficients in R, at width h.

• per : Function.Periodic (g ∘ ↑UpperHalfPlane.ofComplex) ↑h
• holo : MDiff g
• bdd : UpperHalfPlane.IsBoundedAtImInfty g
• mem (n : ℕ) : (PowerSeries.coeff n) (UpperHalfPlane.qExpansion h g) ∈ R

theorem Chudnovsky.GoodQ.ana {h : ℝ} (hh : 0 < h) {R : Subring ℂ} {g : UpperHalfPlane → ℂ} (hg : GoodQ h R g) : AnalyticAt ℂ (UpperHalfPlane.cuspFunction h g) 0

theorem Chudnovsky.GoodQ.add {h : ℝ} (hh : 0 < h) {R : Subring ℂ} {g₁ g₂ : UpperHalfPlane → ℂ} (h₁ : GoodQ h R g₁) (h₂ : GoodQ h R g₂) : GoodQ h R fun (τ : UpperHalfPlane) => g₁ τ + g₂ τ

theorem Chudnovsky.GoodQ.mul {h : ℝ} (hh : 0 < h) {R : Subring ℂ} {g₁ g₂ : UpperHalfPlane → ℂ} (h₁ : GoodQ h R g₁) (h₂ : GoodQ h R g₂) : GoodQ h R fun (τ : UpperHalfPlane) => g₁ τ * g₂ τ

theorem Chudnovsky.goodQ_one {h : ℝ} (_hh : 0 < h) {R : Subring ℂ} : GoodQ h R fun (x : UpperHalfPlane) => 1

theorem Chudnovsky.goodQ_smul {h : ℝ} (hh : 0 < h) {R : Subring ℂ} {g : UpperHalfPlane → ℂ} (hg : GoodQ h R g) {c : ℂ} (hc : c ∈ R) : GoodQ h R fun (τ : UpperHalfPlane) => c * g τ

theorem Chudnovsky.goodQ_const {h : ℝ} (hh : 0 < h) {R : Subring ℂ} {c : ℂ} (hc : c ∈ R) : GoodQ h R fun (x : UpperHalfPlane) => c

theorem Chudnovsky.GoodQ.neg {h : ℝ} (hh : 0 < h) {R : Subring ℂ} {g : UpperHalfPlane → ℂ} (hg : GoodQ h R g) : GoodQ h R fun (τ : UpperHalfPlane) => -g τ

theorem Chudnovsky.GoodQ.sub {h : ℝ} (hh : 0 < h) {R : Subring ℂ} {g₁ g₂ : UpperHalfPlane → ℂ} (h₁ : GoodQ h R g₁) (h₂ : GoodQ h R g₂) : GoodQ h R fun (τ : UpperHalfPlane) => g₁ τ - g₂ τ

theorem Chudnovsky.mdifferentiable_wParam {m : ℕ} : MDiff fun (τ : UpperHalfPlane) => wParam m τ

wParam is holomorphic.

theorem Chudnovsky.isBoundedAtImInfty_jqPow (k : ℕ) : UpperHalfPlane.IsBoundedAtImInfty fun (τ : UpperHalfPlane) => (j τ * q τ) ^ k

(j·q)^k is bounded at i∞ (public, via the identity isogeny).

theorem Chudnovsky.isBoundedAtImInfty_q : UpperHalfPlane.IsBoundedAtImInfty fun (τ : UpperHalfPlane) => q τ

q is bounded at i∞.

theorem Chudnovsky.GoodQ.pow {h : ℝ} (hh : 0 < h) {R : Subring ℂ} {g : UpperHalfPlane → ℂ} (hg : GoodQ h R g) (k : ℕ) : GoodQ h R fun (τ : UpperHalfPlane) => g τ ^ k

Powers preserve GoodQ.

theorem Chudnovsky.goodQ_q (R : Subring ℂ) : GoodQ 1 R fun (τ : UpperHalfPlane) => q τ

theorem Chudnovsky.goodQ_jq (R : Subring ℂ) : GoodQ 1 R fun (τ : UpperHalfPlane) => j τ * q τ

theorem Chudnovsky.GoodQ.of_eq {h : ℝ} {R : Subring ℂ} {g g' : UpperHalfPlane → ℂ} (hg : GoodQ h R g) (he : ∀ (τ : UpperHalfPlane), g' τ = g τ) : GoodQ h R g'

theorem Chudnovsky.goodQ_sum {h : ℝ} (hh : 0 < h) {R : Subring ℂ} {ι : Type u_1} (s : Finset ι) (g : ι → UpperHalfPlane → ℂ) (hg : ∀ i ∈ s, GoodQ h R (g i)) : GoodQ h R fun (τ : UpperHalfPlane) => ∑ i ∈ s, g i τ

theorem Chudnovsky.orbitPoly_coeff_isCuspMeroR_RQ {m : ℕ} [NeZero m] (n : ℕ) (P : Polynomial ℚ) (hP : ∀ (τ : UpperHalfPlane), (orbitPoly m τ).coeff n = (Polynomial.aeval (j τ)) P) (N : ℕ) (hN : P.natDegree ≤ N) : IsCuspMeroR (fun (τ : UpperHalfPlane) => (orbitPoly m τ).coeff n) N RQ

Rationality of the orbit-polynomial coefficients (structure + ℚ-coefficients). If (orbitPoly m τ).coeff n = aeval (j τ) P for a ℚ-polynomial P of degree ≤ N, then that coefficient is cusp-meromorphic of pole order ≤ N with ℚ-coefficients.

theorem Chudnovsky.wParam_eq_qParam {m : ℕ} (τ : UpperHalfPlane) : wParam m τ = Function.Periodic.qParam ↑m ↑τ

The base variable w = wParam m τ is the width-m q-parameter.

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

Width-m raw w-expansion coefficient uniqueness (mirrors qExpansion_coeff_unique_raw at width m, with w = wParam m in place of q).

Width-m machinery: algebraic integrality of the w-expansion

def Chudnovsky.RI : Subring ℂ

The subring of algebraic integers ℤbar ⊆ ℂ.

Equations

• Chudnovsky.RI = (integralClosure ℤ ℂ).toSubring

theorem Chudnovsky.mem_RI_iff {x : ℂ} : x ∈ RI ↔ IsIntegral ℤ x

theorem Chudnovsky.intCast_mem_RI (n : ℤ) : ↑n ∈ RI

theorem Chudnovsky.zetaM_mem_RI {m : ℕ} [NeZero m] : zetaM m ∈ RI

Roots of unity are algebraic integers: ζ_m ∈ ℤbar.

theorem Chudnovsky.zetaM_zpow_mem_RI {m : ℕ} [NeZero m] (n : ℤ) : zetaM m ^ n ∈ RI

theorem Chudnovsky.periodic_comp_ofComplex_of_vadd_gen {f : UpperHalfPlane → ℂ} {p : ℝ} (_hp : 0 < p) (hf : ∀ (τ : UpperHalfPlane), f (p +ᵥ τ) = f τ) : Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑p

General period-p version of periodic_comp_ofComplex_of_vadd.

theorem Chudnovsky.wParam_vadd_m {m : ℕ} [NeZero m] (τ : UpperHalfPlane) : wParam m (↑m +ᵥ τ) = wParam m τ

theorem Chudnovsky.f_vadd_m {m : ℕ} [NeZero m] (i : Option (ZMod m)) (τ : UpperHalfPlane) : f m i (↑m +ᵥ τ) = f m i τ

theorem Chudnovsky.isBoundedAtImInfty_wParam {m : ℕ} [NeZero m] : UpperHalfPlane.IsBoundedAtImInfty fun (τ : UpperHalfPlane) => wParam m τ

theorem Chudnovsky.goodQ_of_wHasSum {m : ℕ} [NeZero m] {F : UpperHalfPlane → ℂ} {a : ℕ → ℂ} {e : ℕ → ℕ} (hpe : Function.Periodic (F ∘ ↑UpperHalfPlane.ofComplex) ↑↑m) (hho : MDiff F) (hbd : UpperHalfPlane.IsBoundedAtImInfty F) (hei : Function.Injective e) (ha : ∀ (n : ℕ), a n ∈ RI) (hHS : ∀ (τ : UpperHalfPlane), HasSum (fun (n : ℕ) => a n • wParam m τ ^ e n) (F τ)) : GoodQ (↑m) RI F

Reindexing helper: a function with a w-expansion supported on the (injective) image of e with ℤbar-coefficients is GoodQ at width m over ℤbar.

theorem Chudnovsky.goodQ_G_none {m : ℕ} [NeZero m] : GoodQ (↑m) RI fun (τ : UpperHalfPlane) => f m none τ * wParam m τ ^ m ^ 2

G_∞ = f_∞ · w^{m²} is GoodQ at width m over ℤbar (its w-expansion has integer coefficients).

theorem Chudnovsky.goodQ_G_some {m : ℕ} [NeZero m] (b : ZMod m) : GoodQ (↑m) RI fun (τ : UpperHalfPlane) => f m (some b) τ * wParam m τ ^ m ^ 2

G_b = f_b · w^{m²} is GoodQ at width m over ℤbar (its w-expansion has ℤ[ζ_m] coefficients).

theorem Chudnovsky.goodQ_w {m : ℕ} [NeZero m] (R : Subring ℂ) : GoodQ (↑m) R fun (τ : UpperHalfPlane) => wParam m τ

theorem Chudnovsky.goodQ_G {m : ℕ} [NeZero m] (i : Option (ZMod m)) : GoodQ (↑m) RI fun (τ : UpperHalfPlane) => f m i τ * wParam m τ ^ m ^ 2

theorem Chudnovsky.coeff_linMul_zero (α β : ℂ) (Q : Polynomial ℂ) : ((Polynomial.C α * Polynomial.X - Polynomial.C β) * Q).coeff 0 = -(β * Q.coeff 0)

theorem Chudnovsky.coeff_linMul_succ (α β : ℂ) (Q : Polynomial ℂ) (k : ℕ) : ((Polynomial.C α * Polynomial.X - Polynomial.C β) * Q).coeff (k + 1) = α * Q.coeff k - β * Q.coeff (k + 1)

theorem Chudnovsky.goodQ_prod_coeff {m : ℕ} [NeZero m] (s : Finset (Option (ZMod m))) (n : ℕ) : GoodQ (↑m) RI fun (τ : UpperHalfPlane) => (∏ i ∈ s, (Polynomial.C (wParam m τ ^ m ^ 2) * Polynomial.X - Polynomial.C (f m i τ * wParam m τ ^ m ^ 2))).coeff n

The product induction. Every coefficient of the pole-cleared orbit polynomial ∏_i (w^{m²}·X − f_i·w^{m²}) is GoodQ at width m over the algebraic integers ℤbar.

theorem Chudnovsky.goodQ_orbitPoly_coeff_mul_qpow {m : ℕ} [NeZero m] (n N : ℕ) (hN : m ^ 2 * (m + 1) ≤ m * N) : GoodQ (↑m) RI fun (τ : UpperHalfPlane) => (orbitPoly m τ).coeff n * q τ ^ N

Width-m integrality of (orbitPoly).coeff n · q^N. For m² (m+1) ≤ m·N, the function (orbitPoly m τ).coeff n · q^N is GoodQ at width m over the algebraic integers: its w-expansion has algebraic-integer coefficients.

theorem Chudnovsky.widthm_coeff_eq {m : ℕ} [NeZero m] {F : UpperHalfPlane → ℂ} (hp1 : Function.Periodic (F ∘ ↑UpperHalfPlane.ofComplex) 1) (hpm : Function.Periodic (F ∘ ↑UpperHalfPlane.ofComplex) ↑↑m) (hho : MDiff F) (hbd : UpperHalfPlane.IsBoundedAtImInfty F) (p : ℕ) : (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 F) = (PowerSeries.coeff (m * p)) (UpperHalfPlane.qExpansion (↑m) F)

Matching width-1 and width-m coefficients. For a function F that is both 1-periodic and m-periodic, holomorphic and bounded at the cusp, the p-th ordinary q-coefficient equals the (m·p)-th w-coefficient (q = w^m).

theorem Chudnovsky.orbitPoly_coeff_isCuspMeroR_bot {m : ℕ} [Fact (Nat.Prime m)] (n : ℕ) : ∃ (N : ℕ), IsCuspMeroR (fun (τ : UpperHalfPlane) => (orbitPoly m τ).coeff n) N ⊥

The ⊥-gate hZ, discharged for each n. Each orbit-polynomial coefficient is cusp-meromorphic of finite order with coefficients in ⊥ ⊆ ℂ (the integers): rational (averaging) and an algebraic integer (the ℤ[ζ_m] w-expansion), hence in ⊥.

The unconditional keystone Φ_m ∈ ℤ[Y][X] and the unconditional ℚ-root bridge

theorem Chudnovsky.exists_PhiZ_closed {m : ℕ} [Fact (Nat.Prime m)] : ∃ (PhiZ : Polynomial (Polynomial ℤ)), ∀ (τ : UpperHalfPlane), orbitPoly m τ = (specializeZ (j τ)) PhiZ

(B6) fully closed. For a prime m, the modular polynomial Φ_m ∈ ℤ[Y][X] exists with the keystone identity ∏_i (X − f_i τ) = Φ_m(X, j τ) for every τ. The ⊥-coefficient cusp-meromorphy gate hZ of exists_PhiZ is discharged by the w-expansion integrality machinery (orbitPoly_coeff_isCuspMeroR_bot): rationality from the ℚ-averaging, algebraic integrality from the ℤ[ζ_m]-coefficient w-expansion, combined pointwise by mem_bot_of_integral_of_rat.

theorem Chudnovsky.exists_PhiQ_j_root {m : ℕ} [Fact (Nat.Prime m)] {τ σ : UpperHalfPlane} {i : Option (ZMod m)} (h : j σ = f m i τ) : ∃ (PhiQ : Polynomial (Polynomial ℚ)), (∀ (ρ : UpperHalfPlane), orbitPoly m ρ = (specializeY (j ρ)) PhiQ) ∧ Polynomial.eval (j σ) ((specializeY (j τ)) PhiQ) = 0

The root bridge, unconditional ℚ-version. Instantiating PhiQ_eval_j_root with the parallel agent's exists_PhiQ_closed: for a prime m, if j σ = f m i τ for some coset index i (a CM relation), then there is a modular polynomial Φ_m ∈ ℚ[Y][X] with the keystone identity for which Φ_m(j σ, j τ) = 0. This is the shape Rationality.lean / MasserA1.lean consume.