Kronecker's unit-leading-coefficient lemma for the diagonal modular polynomial (Phase C, B7)

This file discharges the gated hypothesis hlead of ModularPolynomialZ.isIntegral_of_kronecker: for a prime m ≥ 2 and any PhiZ : ℤ[Y][X] satisfying the keystone identity orbitPoly m τ = Φ_m(X, j τ), the diagonal G_m := diagPhiZ PhiZ = Φ_m(X, X) has

• natDegree = 2·m (diagPhiZ_natDegree_eq), and
• leadingCoeff = -1 (diagPhiZ_leadingCoeff_eq_neg_one), hence ±1 (diagPhiZ_leadingCoeff_eq).

The argument — pure limit calculus at the cusp Im τ → ∞

All series manipulation is already packaged upstream; here we only take limits along UpperHalfPlane.atImInfty.

The single analytic input is jq_tendsto_one : j τ · q τ → 1, proved from the fact that the q-expansion of j·q extends analytically across the cusp with value the constant coefficient jqInt.coeff 0 = 1 (UpperHalfPlane.eq_cuspFunction + continuity of cuspFunction). Composing with the isogenies Acol/AInf (which push towards the cusp, tendsto_smul_atImInfty) and using q = wᵐ, q(Acol • τ) = ζᵇ·w, q(AInf • τ) = w^{m²} gives, as Im τ → ∞:

• each some b factor (j τ − f_b τ)·q → 1 (some_factor_tendsto_one);
• the ∞ factor (j τ − f_∞ τ)·qᵐ → −1 (none_factor_tendsto_neg_one);

so the orbit product D(τ)·q^{2m} = G_m(j τ)·q^{2m} → 1^m·(−1) = −1 (orbit_prod_tendsto_neg_one). Matching this against the polynomial expansion G_m(j τ)·q^{d} → leadingCoeff (eval2_qpow_tendsto, using (j·q)ʳ·q^{d−r} → 0 for d > r), uniqueness of limits (atImInfty.NeBot) forces d = 2m and leadingCoeff = −1.

Everything downstream of ±1 is isIntegral_of_kronecker; isIntegral_j_of_cm composes the two so that only the CM relation j τ = f m i τ and the defining identity hPhi are needed.

The cusp limit j·q → 1

theorem Chudnovsky.q_tendsto_zero : Filter.Tendsto (fun (τ : UpperHalfPlane) => q τ) UpperHalfPlane.atImInfty (nhds 0)

q τ → 0 as Im τ → ∞.

theorem Chudnovsky.isBoundedAtImInfty_jq' : UpperHalfPlane.IsBoundedAtImInfty fun (τ : UpperHalfPlane) => j τ * q τ

j·q is bounded at the cusp (it tends to 1); reconstructed from discriminant = q · ∏ (1 − qⁿ)²⁴ and j·Δ = E₄³.

theorem Chudnovsky.jq_tendsto_one : Filter.Tendsto (fun (τ : UpperHalfPlane) => j τ * q τ) UpperHalfPlane.atImInfty (nhds 1)

The single analytic input. j τ · q τ → 1 as Im τ → ∞: the q-expansion of j·q extends analytically across the cusp with value its constant coefficient jqInt.coeff 0 = 1.

theorem Chudnovsky.jq_comp_tendsto_one {A : GL (Fin 2) ℝ} (hA : ↑A 1 0 = 0) : Filter.Tendsto (fun (τ : UpperHalfPlane) => j (A • τ) * q (A • τ)) UpperHalfPlane.atImInfty (nhds 1)

j·q composed with an isogeny A of lower-left entry 0 (which pushes towards i∞) still tends to 1.

theorem Chudnovsky.wParam_tendsto_zero {m : ℕ} [NeZero m] : Filter.Tendsto (fun (τ : UpperHalfPlane) => wParam m τ) UpperHalfPlane.atImInfty (nhds 0)

The base variable w = wParam m τ → 0 at the cusp (it is q of the coset point at b = 0).

Per-factor limits of the orbit product

theorem Chudnovsky.some_factor_tendsto_one {m : ℕ} [Fact (Nat.Prime m)] (b : ZMod m) : Filter.Tendsto (fun (τ : UpperHalfPlane) => (j τ - f m (some b) τ) * q τ) UpperHalfPlane.atImInfty (nhds 1)

Each some b factor of the orbit product, times q, tends to 1.

theorem Chudnovsky.none_factor_tendsto_neg_one {m : ℕ} [Fact (Nat.Prime m)] : Filter.Tendsto (fun (τ : UpperHalfPlane) => (j τ - f m none τ) * q τ ^ m) UpperHalfPlane.atImInfty (nhds (-1))

The ∞ factor of the orbit product, times qᵐ, tends to −1.

theorem Chudnovsky.orbit_prod_tendsto_neg_one {m : ℕ} [Fact (Nat.Prime m)] : Filter.Tendsto (fun (τ : UpperHalfPlane) => (∏ i : Option (ZMod m), (j τ - f m i τ)) * q τ ^ (2 * m)) UpperHalfPlane.atImInfty (nhds (-1))

The orbit product limit. D(τ)·q^{2m} = (∏_i (j τ − f_i τ))·q^{2m} → −1.

The polynomial side

theorem Chudnovsky.term_tendsto (c : ℂ) (r d : ℕ) (hrd : r ≤ d) : Filter.Tendsto (fun (τ : UpperHalfPlane) => c * j τ ^ r * q τ ^ d) UpperHalfPlane.atImInfty (nhds (if r = d then c else 0))

A single monomial term c·(j τ)ʳ·qᵈ tends to c if r = d and to 0 if r < d (with r ≤ d), since it equals c·(j·q)ʳ·q^{d−r} and j·q → 1, q → 0.

theorem Chudnovsky.eval2_qpow_tendsto (G : Polynomial ℤ) : Filter.Tendsto (fun (τ : UpperHalfPlane) => Polynomial.eval₂ (Int.castRingHom ℂ) (j τ) G * q τ ^ G.natDegree) UpperHalfPlane.atImInfty (nhds ↑G.leadingCoeff)

G(j τ)·q^{natDegree G} → (leadingCoeff G : ℂ): matching the polynomial against its top q-power isolates the leading coefficient.

Kronecker's lemma

theorem Chudnovsky.diagPhiZ_natDegree_and_leadingCoeff {m : ℕ} [Fact (Nat.Prime m)] {PhiZ : Polynomial (Polynomial ℤ)} (hPhi : ∀ (τ : UpperHalfPlane), orbitPoly m τ = (specializeZ (j τ)) PhiZ) : (diagPhiZ PhiZ).natDegree = 2 * m ∧ (diagPhiZ PhiZ).leadingCoeff = -1

(B7) Kronecker, sharp form. For prime m and any PhiZ with the keystone identity, the diagonal G_m = diagPhiZ PhiZ has natDegree = 2·m and leadingCoeff = −1.

theorem Chudnovsky.diagPhiZ_natDegree_eq {m : ℕ} [Fact (Nat.Prime m)] {PhiZ : Polynomial (Polynomial ℤ)} (hPhi : ∀ (τ : UpperHalfPlane), orbitPoly m τ = (specializeZ (j τ)) PhiZ) : (diagPhiZ PhiZ).natDegree = 2 * m

natDegree (diagPhiZ PhiZ) = 2·m.

theorem Chudnovsky.diagPhiZ_leadingCoeff_eq_neg_one {m : ℕ} [Fact (Nat.Prime m)] {PhiZ : Polynomial (Polynomial ℤ)} (hPhi : ∀ (τ : UpperHalfPlane), orbitPoly m τ = (specializeZ (j τ)) PhiZ) : (diagPhiZ PhiZ).leadingCoeff = -1

leadingCoeff (diagPhiZ PhiZ) = −1 (the sharp form of Kronecker's lemma).

theorem Chudnovsky.diagPhiZ_leadingCoeff_eq {m : ℕ} [Fact (Nat.Prime m)] {PhiZ : Polynomial (Polynomial ℤ)} (hPhi : ∀ (τ : UpperHalfPlane), orbitPoly m τ = (specializeZ (j τ)) PhiZ) : (diagPhiZ PhiZ).leadingCoeff = 1 ∨ (diagPhiZ PhiZ).leadingCoeff = -1

(B7) Kronecker's unit-leading-coefficient lemma. The diagonal modular polynomial G_m = diagPhiZ PhiZ has leading coefficient ±1. This is exactly the hlead hypothesis of isIntegral_of_kronecker.

theorem Chudnovsky.isIntegral_j_of_cm {m : ℕ} [Fact (Nat.Prime m)] {PhiZ : Polynomial (Polynomial ℤ)} (hPhi : ∀ (τ : UpperHalfPlane), orbitPoly m τ = (specializeZ (j τ)) PhiZ) {τ : UpperHalfPlane} {i : Option (ZMod m)} (hcm : j τ = f m i τ) : IsIntegral ℤ (j τ)

The composed integrality corollary. For a prime m, any PhiZ with the keystone identity, and a CM relation j τ = f m i τ, the value j τ is integral over ℤ. Discharges the hlead argument of isIntegral_of_kronecker, so downstream only the identity hPhi (from exists_PhiZ) and the CM root are needed.