The j-function: definition, invariance, analyticity, q-expansion (Phase C, chunk B1)

This is the first file of Track 1 of Phase C (see Playground/Pi/PhaseC-PLAN.md, §3.1, sub-lemma (B1)). It packages the elementary function-theoretic facts about the modular j-invariant j = 1728·J = E₄³/Δ that the modular-polynomial pipeline (CosetOrbit.lean, ModularPolynomialQ.lean, CMRelations.lean) consumes:

• Chudnovsky.j : the normalization j τ = 1728 · J τ (kept definitionally equal to the 1728 * J τ that SingularModuli.lean's pinned statements refer to);
• j_eq, j_mul_discriminant : the algebraic backbone j = E₄³/Δ, j·Δ = E₄³;
• modular invariance j (γ • τ) = j τ for γ ∈ SL(2,ℤ), plus the S/T generator specializations;
• analyticity MDifferentiable … j on ℍ (from E₄, E₆ holomorphic and Δ ≠ 0);
• integrality of the E₄ and E₄³ q-expansion coefficients (the ℤ-side building blocks of (B1), feeding the ℤ-refinement of ModularPolynomialZ.lean);
• the (B1) headline: j·q ∈ 1 + q·ℤ⟦q⟧, delivered as
  • Chudnovsky.jqInt : PowerSeries ℤ with constantCoeff_jqInt : constantCoeff jqInt = 1,
  • qExpansion_j_mul_q : qExpansion 1 (fun τ ↦ j τ * q τ) = jqInt.map (Int.castRingHom ℂ),
  • hasSum_j_mul_q : HasSum (fun n ↦ (jqInt.coeff n : ℂ) * q τ ^ n) (j τ * q τ) for every τ : ℍ (so j = q⁻¹·(1 + 744q + …) with integer coefficients — the pole-order-1 structure at the cusp), together with the same package for Δ itself (deltaInt, qExpansion_discriminant_int, deltaInt_coeff_zero/one) which CosetOrbit.lean/ModularPolynomialZ.lean can reuse.

Deviation from the plan's decision point 4

The plan recommends the η-product route (option (a)) for the ℤ-integrality of the Δ q-expansion. Here we instead use option (b), the 1728-congruence: Mathlib gives the exact q-expansions of E₄, E₆ with coefficients 240·σ₃(n), -504·σ₅(n), and the coefficientwise divisibility 1728 ∣ (E₄³ - E₆²)-coefficients reduces (via σ₅(n) ≡ σ₃(n) mod 24, i.e. d⁵ ≡ d³ mod 24 for every d, a decide on ZMod 24) to finite arithmetic. Reason for the deviation: option (a) needs "Taylor coefficients of a locally uniform limit of the partial η-products", an analytic limit-interchange with no direct Mathlib support, while option (b) is pure PowerSeries ℤ algebra glued to Mathlib's qExpansion API by qExpansion_mul/sub/smul and qExpansion_coeff_unique — no analytic estimate at all. (The η-product still appears once, harmlessly, in the boundedness of j·q at the cusp, via tendsto_atImInfty_tprod_one_sub_eta_q_pow.)

Definition and the algebraic backbone j = E₄³/Δ

noncomputable def Chudnovsky.j (τ : UpperHalfPlane) : ℂ

The modular j-invariant in this project's normalization, j = 1728·J = E₄³/Δ. Kept definitionally equal to the 1728 * J τ appearing in SingularModuli.lean's pinned statements.

Equations

• Chudnovsky.j τ = 1728 * Chudnovsky.J τ

@[simp]

theorem Chudnovsky.j_def (τ : UpperHalfPlane) : j τ = 1728 * J τ

theorem Chudnovsky.j_eq (τ : UpperHalfPlane) : j τ = ModularForm.E₄ τ ^ 3 / ModularForm.discriminant τ

j = E₄³/Δ.

theorem Chudnovsky.j_mul_discriminant (τ : UpperHalfPlane) : j τ * ModularForm.discriminant τ = ModularForm.E₄ τ ^ 3

The algebraic backbone j·Δ = E₄³.

Modular invariance

theorem Chudnovsky.modularForm_SL_smul {k : ℤ} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane) : f (γ • τ) = UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ ^ k * f τ

The SL(2,ℤ) transformation law of a level-one modular form of weight k: f (γ • τ) = (denom γ τ)ᵏ · f τ. (General γ version of Ramanujan.modularForm_S_smul.)

theorem Chudnovsky.J_smul (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane) : J (γ • τ) = J τ

Klein's J is SL(2,ℤ)-invariant.

theorem Chudnovsky.j_smul (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane) : j (γ • τ) = j τ

The j-invariant is SL(2,ℤ)-invariant: j (γ • τ) = j τ.

theorem Chudnovsky.j_vadd_one (τ : UpperHalfPlane) : j (1 +ᵥ τ) = j τ

T-invariance: j (τ + 1) = j τ.

theorem Chudnovsky.j_S_smul (τ : UpperHalfPlane) : j (ModularGroup.S • τ) = j τ

S-invariance: j (-1/τ) = j τ.

Analyticity

theorem Chudnovsky.mdifferentiable_J : MDiff fun (τ : UpperHalfPlane) => J τ

Klein's J is holomorphic on ℍ.

theorem Chudnovsky.mdifferentiable_j : MDiff fun (τ : UpperHalfPlane) => j τ

The j-invariant is holomorphic on ℍ.

Integrality of the Eisenstein q-expansion coefficients

The ℤ-side building blocks of (B1): E₄ (hence E₄³) has integer q-expansion coefficients. These feed the ℤ-refinement ModularPolynomialZ.lean downstream.

theorem Chudnovsky.E₄_qExpansion_coeff_int (n : ℕ) : ∃ (c : ℤ), (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑ModularForm.E₄) = ↑c

Every q-expansion coefficient of E₄ is an integer (1 at n = 0, 240·σ₃(n) else).

theorem Chudnovsky.E₄_qExpansion_pow_three_coeff_int (n : ℕ) : ∃ (c : ℤ), (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑ModularForm.E₄ ^ 3) = ↑c

Every q-expansion coefficient of the cube (qExpansion E₄)³ — i.e. of E₄³ — is an integer. This is the numerator side of j = E₄³/Δ.

The formal ℤ-side: E₄, E₆, Δ as integer power series

We build the integer q-expansions formally in PowerSeries ℤ and identify them with Mathlib's analytic qExpansions. The only arithmetic input is the classical congruence 1728 ∣ (E₄³ - E₆²)-coefficients, which reduces to d⁵ ≡ d³ (mod 24).

noncomputable def Chudnovsky.deltaInt : PowerSeries ℤ

The integer q-expansion of the discriminant Δ = q·∏(1-qⁿ)²⁴ = ∑ τ(n) qⁿ (Ramanujan-τ coefficients), obtained as (E₄³ - E₆²)/1728 in ℤ⟦q⟧.

Equations

• Chudnovsky.deltaInt = PowerSeries.mk fun (m : ℕ) => ⋯.choose

Analytic identification of deltaInt

theorem Chudnovsky.qExpansion_discriminant_int : UpperHalfPlane.qExpansion 1 ModularForm.discriminant = (PowerSeries.map (Int.castRingHom ℂ)) deltaInt

Δ has integer q-expansion coefficients: Mathlib's qExpansion 1 Δ is the ℤ-power-series deltaInt, cast to ℂ.

theorem Chudnovsky.deltaInt_coeff_zero : (PowerSeries.coeff 0) deltaInt = 0

Δ vanishes at the cusp: constant q-expansion coefficient 0.

theorem Chudnovsky.deltaInt_coeff_one : (PowerSeries.coeff 1) deltaInt = 1

Δ = q + O(q²): the leading q-expansion coefficient of Δ is 1.

noncomputable def Chudnovsky.deltaTail : PowerSeries ℤ

The unit part Δ/q ∈ ℤ⟦q⟧: deltaInt = X · deltaTail with deltaTail(0) = 1.

Equations

• Chudnovsky.deltaTail = PowerSeries.mk fun (n : ℕ) => (PowerSeries.coeff (n + 1)) Chudnovsky.deltaInt

theorem Chudnovsky.deltaInt_eq_X_mul_deltaTail : deltaInt = PowerSeries.X * deltaTail

theorem Chudnovsky.constantCoeff_deltaTail : PowerSeries.constantCoeff deltaTail = 1

noncomputable def Chudnovsky.jqInt : PowerSeries ℤ

The integer q-expansion of j·q: E₄³·(Δ/q)⁻¹ computed in ℤ⟦q⟧ — the formal series 1 + 744q + 196884q² + ….

Equations

• Chudnovsky.jqInt = Chudnovsky.E4Z✝ ^ 3 * Chudnovsky.deltaTail.invOfUnit 1

theorem Chudnovsky.constantCoeff_jqInt : PowerSeries.constantCoeff jqInt = 1

j·q ∈ 1 + q·ℤ⟦q⟧, formal part: the constant coefficient of jqInt is 1.

The analytic side: τ ↦ q τ and τ ↦ j τ · q τ

theorem Chudnovsky.q_vadd_one (τ : UpperHalfPlane) : q (1 +ᵥ τ) = q τ

The nome is 1-periodic on ℍ.

theorem Chudnovsky.mdifferentiable_q : MDiff fun (τ : UpperHalfPlane) => q τ

The nome q : ℍ → ℂ is holomorphic.

theorem Chudnovsky.mdifferentiable_j_mul_q : MDiff fun (τ : UpperHalfPlane) => j τ * q τ

j·q is holomorphic on ℍ.

The keystone: qExpansion (j·q) = jqInt

theorem Chudnovsky.qExpansion_j_mul_q : (UpperHalfPlane.qExpansion 1 fun (τ : UpperHalfPlane) => j τ * q τ) = (PowerSeries.map (Int.castRingHom ℂ)) jqInt

(B1) headline, q-expansion form: the q-expansion of j·q is the integer power series jqInt (so j·q ∈ 1 + q·ℤ⟦q⟧, and j has a simple pole with residue-coefficient 1 at the cusp).

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

(B1) headline, convergent-sum form: for every τ ∈ ℍ, j(τ)·q(τ) = ∑ c(n)·q(τ)ⁿ with the integer coefficients c = jqInt.coeff.

theorem Chudnovsky.j_mul_q_qExpansion_coeff_int (n : ℕ) : ∃ (c : ℤ), (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 fun (τ : UpperHalfPlane) => j τ * q τ) = ↑c

Every q-expansion coefficient of j·q is an integer.

theorem Chudnovsky.j_mul_q_qExpansion_coeff_zero : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 fun (τ : UpperHalfPlane) => j τ * q τ) = 1

The q-expansion of j·q has constant coefficient 1 (equivalently, j ~ 1/q at the cusp with leading coefficient 1 — the pole-order-1 structure needed downstream).

theorem Chudnovsky.j_mul_q_hasSum_int : ∃ (c : ℕ → ℤ), c 0 = 1 ∧ ∀ (τ : UpperHalfPlane), HasSum (fun (n : ℕ) => ↑(c n) * q τ ^ n) (j τ * q τ)

(B1) headline, existential packaging: j·q ∈ 1 + q·ℤ⟦q⟧ — there are integers c 0 = 1, c 1 = 744, c 2 = 196884, … with j τ · q τ = ∑ c n · q τ ^ n for all τ : ℍ.