Valence theory of the j-function (Phase C, Track 2, §4.3)

This file develops the valence theory of the modular j-invariant that the Rationality track (Rationality.lean, statement 2 of SingularModuli.lean) consumes: injectivity mod Γ and surjectivity. See Playground/Pi/PhaseC-PLAN.md, §4.2 (the three-prime argument, input (C3)) and §4.3 (this sub-plan). The Isabelle/AFP "Complex Lattices, Elliptic Functions, and the Modular Group" development is the design blueprint (§1).

What is proved here (sorry-free)

• Fundamental-domain reduction exists_smul_mem_fd_j: every τ is SL(2,ℤ)-equivalent to a point of the closed fundamental domain 𝒟, with equal j-value (a thin wrapper of Mathlib's ModularGroup.exists_smul_mem_fd and j_smul).
• Lattice reformulation j_eq_iff_J, j_eq_iff_periodPair_J: j τ₁ = j τ₂ iff Klein's invariants of the lattices L_{τ₁}, L_{τ₂} agree (via Fourier.J_eq_J_Lτ).
• The weighted-projective identity E₄E₆_proj_eq_of_j_eq / g₂g₃_proj_eq_of_j_eq: j τ₁ = j τ₂ ⇒ E₄(τ₁)³·E₆(τ₂)² = E₄(τ₂)³·E₆(τ₁)², equivalently g₂(L₁)³·g₃(L₂)² = g₂(L₂)³·g₃(L₁)² — the (g₂³ : g₃²) proportionality of §4.3.
• Lattice-rigidity step 1 exists_units_smul_g₂_g₃: for two lattices with L₁.J = L₂.J (and nonzero discriminants) there is a homothety a : ℂˣ with g₂(a·L₂) = g₂(L₁) and g₃(a·L₂) = g₃(L₁). This is the "there is λ ∈ ℂˣ with g₂(λ L_{τ′}) = g₂(L_τ), g₃(λ L_{τ′}) = g₃(L_τ)" of §4.3, done in full (the 4th/6th-root bookkeeping). It reduces injectivity to the lattice-recovery core (see TODO below).
• Gated injectivity j_injective_mod_Γ_of_lattice_core: injectivity mod Γ follows from the isolated lattice-recovery core (equal (g₂,g₃) of homothetic lattices ⇒ the base points are Γ-equivalent).
• The lattice-recovery core, discharged in full (see the section "The lattice-recovery core, discharged"): PeriodPair.weierstrassP_eventuallyEq_of_g₂_g₃ (equal (g₂,g₃) ⇒ equal ℘ near 0, via the Eisenstein-coefficient recursion extracted from the ODE ℘'' = 6℘² − g₂/2 of DivisionValues.lean), PeriodPair.lattice_eq_of_weierstrassP_eventuallyEq (identity theorem + pole-set comparison ⇒ equal lattices), exists_sl2_of_lattice_eq (equal lattices ⇒ Γ-related base points), combined in lattice_recovery_core.
• Injectivity mod Γ, unconditional j_injective_mod_Γ: j τ₁ = j τ₂ → ∃ γ : SL(2,ℤ), τ₂ = γ • τ₁.
• Surjectivity, unconditional j_surjective: Function.Surjective (j : ℍ → ℂ). Proved by the open-and-closed argument of §4.3 (isOpen_range_j via the open mapping theorem for the nonconstant holomorphic j, isClosed_range_j via the cusp estimate + compactness of a truncation of the fundamental domain, assembled with IsClopen.eq_univ on the preconnected ℂ). See the "Surjectivity" section.

Both halves of the §4.3 valence theory (j_injective_mod_Γ and j_surjective) are now sorry-free.

Fundamental-domain reduction

theorem Chudnovsky.exists_smul_mem_fd_j (τ : UpperHalfPlane) : ∃ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), γ • τ ∈ ModularGroup.fd ∧ j (γ • τ) = j τ

Every τ : ℍ is SL(2,ℤ)-equivalent to a point of the closed fundamental domain 𝒟, and j is constant along this move. Wrapper of ModularGroup.exists_smul_mem_fd and j_smul; used by the surjectivity argument (move a would-be limit point into 𝒟).

Lattice reformulation of j-equality

theorem Chudnovsky.j_eq_iff_J (τ₁ τ₂ : UpperHalfPlane) : j τ₁ = j τ₂ ↔ J τ₁ = J τ₂

j τ₁ = j τ₂ ↔ J τ₁ = J τ₂ (the factor 1728 is a unit).

theorem Chudnovsky.j_eq_iff_periodPair_J (τ₁ τ₂ : UpperHalfPlane) : j τ₁ = j τ₂ ↔ (Lτ τ₁).J = (Lτ τ₂).J

j τ₁ = j τ₂ iff Klein's absolute invariants of the lattices L_{τ₁}, L_{τ₂} agree. This is the entry point for the lattice-rigidity route to injectivity (§4.3).

The weighted-projective (g₂³ : g₃²) identity

theorem Chudnovsky.E₄E₆_proj_eq_of_j_eq {τ₁ τ₂ : UpperHalfPlane} (h : j τ₁ = j τ₂) : ModularForm.E₄ τ₁ ^ 3 * ModularForm.E₆ τ₂ ^ 2 = ModularForm.E₄ τ₂ ^ 3 * ModularForm.E₆ τ₁ ^ 2

j τ₁ = j τ₂ ⇒ E₄(τ₁)³·E₆(τ₂)² = E₄(τ₂)³·E₆(τ₁)². Cross-multiplying J τ₁ = J τ₂ kills the E₄³·E₄³ terms and leaves the weighted-projective equality of §4.3.

theorem Chudnovsky.g₂g₃_proj_eq_of_j_eq {τ₁ τ₂ : UpperHalfPlane} (h : j τ₁ = j τ₂) : (Lτ τ₁).g₂ ^ 3 * (Lτ τ₂).g₃ ^ 2 = (Lτ τ₂).g₂ ^ 3 * (Lτ τ₁).g₃ ^ 2

The lattice form of E₄E₆_proj_eq_of_j_eq: g₂(L₁)³·g₃(L₂)² = g₂(L₂)³·g₃(L₁)².

Lattice rigidity, step 1: matching g₂ and g₃ by a homothety

§4.3: from J(L₁) = J(L₂) there is a scaling a ∈ ℂˣ with g₂(a·L₂) = g₂(L₁) and g₃(a·L₂) = g₃(L₁). Proof: J-equality gives the projective relation g₂(L₁)³ g₃(L₂)² = g₂(L₂)³ g₃(L₁)²; then a case split on which of g₂, g₃ vanish, with the 4th/6th-root of unity juggling handled by a square/6th/4th root in ℂ (ℂ algebraically closed).

theorem Chudnovsky.g₂cube_g₃sq_eq_of_periodPair_J {L₁ L₂ : PeriodPair} (hd₁ : L₁.discr ≠ 0) (hd₂ : L₂.discr ≠ 0) (hJ : L₁.J = L₂.J) : L₁.g₂ ^ 3 * L₂.g₃ ^ 2 = L₂.g₂ ^ 3 * L₁.g₃ ^ 2

The auxiliary projective relation extracted from L₁.J = L₂.J (both discriminants ≠ 0): g₂(L₁)³·g₃(L₂)² = g₂(L₂)³·g₃(L₁)².

theorem Chudnovsky.exists_units_smul_g₂_g₃ (L₁ L₂ : PeriodPair) (hd₁ : L₁.discr ≠ 0) (hd₂ : L₂.discr ≠ 0) (hJ : L₁.J = L₂.J) : ∃ (a : ℂˣ), (a • L₂).g₂ = L₁.g₂ ∧ (a • L₂).g₃ = L₁.g₃

Lattice-rigidity step 1 (§4.3). If two lattices have the same Klein invariant (with nonzero discriminants) then there is a homothety a : ℂˣ scaling L₂ so that its g₂ and g₃ match those of L₁.

Injectivity mod Γ

theorem Chudnovsky.discr_Lτ_ne_zero (τ : UpperHalfPlane) : (Lτ τ).discr ≠ 0

(Lτ τ).discr ≠ 0 (the discriminant of the lattice ℤ + ℤτ is nonzero).

theorem Chudnovsky.j_injective_mod_Γ_of_lattice_core (lattice_core : ∀ (σ₁ σ₂ : UpperHalfPlane) (a : ℂˣ), (a • Lτ σ₂).g₂ = (Lτ σ₁).g₂ → (a • Lτ σ₂).g₃ = (Lτ σ₁).g₃ → ∃ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), σ₂ = γ • σ₁) {τ₁ τ₂ : UpperHalfPlane} (h : j τ₁ = j τ₂) : ∃ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), τ₂ = γ • τ₁

Injectivity mod Γ, gated on the lattice-recovery core. Once the core (equal (g₂,g₃) of homothetic lattices ⇒ base points Γ-equivalent — see the TODO above for its route) is available, j τ₁ = j τ₂ forces τ₂ = γ • τ₁ for some γ ∈ SL(2,ℤ). The scaling a is produced here in full by exists_units_smul_g₂_g₃.

The lattice-recovery core, discharged

The TODO route above is now carried out in full:

1. Equal (g₂, g₃) ⇒ equal ℘ near 0 (PeriodPair.weierstrassP_eventuallyEq_of_g₂_g₃): the analytic part h := ℘ − z⁻² of ℘ at 0 satisfies (from the project's second-order ODE ℘'' = 6℘² − g₂/2, PeriodPair.lemwp2str) the classical Eisenstein-coefficient recursion; by strong induction all Taylor coefficients of h at 0 are universal polynomials in (g₂, g₃), so the two ℘'s agree on a punctured neighbourhood of 0.
2. Equal near 0 ⇒ equal lattices (PeriodPair.lattice_eq_of_weierstrassP_eventuallyEq): by the identity theorem on the connected set ℂ ∖ (L₁ ∪ L₂) (complement of a countable set), ℘₁ = ℘₂ wherever both are defined; a lattice point of L₁ not in L₂ would be a double pole of ℘₁ (PeriodPair.order_weierstrassP) at which ℘₂ is analytic (meromorphic order ≥ 0) — contradiction, since meromorphic order only depends on the germ on the punctured neighbourhood.
3. Equal lattices ⇒ Γ-related base points (exists_sl2_of_lattice_eq): the two bases (1, τ₁) and (a, a·τ₂) of the common lattice are related by an integer matrix in each direction; the imaginary-part identity det·Im τ₁ = |a|²·Im τ₂ (and its inverse-homothety mirror) forces both determinants positive with product 1, hence det = 1, and the Möbius formula gives τ₂ = γ • τ₁ with γ ∈ SL(2, ℤ).

Combining the three yields lattice_recovery_core, and with j_injective_mod_Γ_of_lattice_core the unconditional injectivity j_injective_mod_Γ.

theorem Chudnovsky.PeriodPair.lattice_countable (L : PeriodPair) : (↑L.lattice).Countable

The lattice of a PeriodPair is countable (it is an image of ℤ × ℤ).

theorem Chudnovsky.PeriodPair.iteratedDeriv_sq_mul (f : ℂ → ℂ) (hf : AnalyticAt ℂ f 0) (m : ℕ) : iteratedDeriv m (fun (z : ℂ) => z ^ 2 * f z) 0 = ↑m * (↑m - 1) * iteratedDeriv (m - 2) f 0

iteratedDeriv of z ↦ z² · f z at 0: only the i = 2 Leibniz term survives.

theorem Chudnovsky.PeriodPair.iteratedDeriv_add_two (m : ℕ) (f : ℂ → ℂ) : iteratedDeriv (m + 2) f = iteratedDeriv m (iteratedDeriv 2 f)

iteratedDeriv (m+2) f = iteratedDeriv m (iteratedDeriv 2 f).

theorem Chudnovsky.PeriodPair.weierstrassP_eventuallyEq_of_g₂_g₃ (L₁ L₂ : PeriodPair) (h2 : L₁.g₂ = L₂.g₂) (h3 : L₁.g₃ = L₂.g₃) : L₁.weierstrassP =ᶠ[nhdsWithin 0 {0}ᶜ] L₂.weierstrassP

Step 1 of the lattice-recovery core: two period pairs with equal g₂ and g₃ have equal ℘ on a punctured neighbourhood of 0.

Proof: let w := ℘₁Except − ℘₂Except be the difference of the analytic parts at 0. The second-order ODE ℘'' = 6℘² − g₂/2 (PeriodPair.lemwp2str, from DivisionValues.lean) turns — after the shared g₂-terms cancel — into the linear relation z²·w'' = z²·6·w·(h₁+h₂) + 12·w near 0. Taking m-th Taylor coefficients at 0 yields the classical Eisenstein recursion with coefficient m(m−1) − 12 = (m−4)(m+3); strong induction (with the resonances m = 0, 1, 4 handled by g₂ = g₂, G₃ = G₅ = 0, and g₃ = g₃) kills every Taylor coefficient of w, so w ≡ 0 near 0.

theorem Chudnovsky.PeriodPair.lattice_subset_of_eqOn (L₁ L₂ : PeriodPair) (heqOn : Set.EqOn L₁.weierstrassP L₂.weierstrassP (↑L₁.lattice ∪ ↑L₂.lattice)ᶜ) : L₁.lattice ≤ L₂.lattice

If ℘₁ = ℘₂ off the union of the two lattices, then L₁ ⊆ L₂: a point of L₁ ∖ L₂ would be a double pole of ℘₁ at which ℘₂ is analytic, contradicting equality of the meromorphic orders (which only depend on punctured-neighbourhood germs).

theorem Chudnovsky.PeriodPair.lattice_eq_of_weierstrassP_eventuallyEq (L₁ L₂ : PeriodPair) (h : L₁.weierstrassP =ᶠ[nhdsWithin 0 {0}ᶜ] L₂.weierstrassP) : L₁.lattice = L₂.lattice

Steps 2–3 of the lattice-recovery core: if ℘₁ = ℘₂ on a punctured neighbourhood of 0, then L₁ = L₂. Identity theorem on the connected complement of the two (countable) lattices, then pole-set comparison.

theorem Chudnovsky.orient_eq {b s t : ℂ} {m₁ n₁ m₂ n₂ : ℤ} (h1 : b = ↑m₁ + ↑n₁ * s) (h2 : b * t = ↑m₂ + ↑n₂ * s) : ↑(m₁ * n₂ - n₁ * m₂) * s.im = Complex.normSq b * t.im

Orientation / imaginary-part identity: if b = m₁ + n₁·s and b·t = m₂ + n₂·s, then (m₁n₂ − n₁m₂)·Im s = |b|²·Im t. Applied twice (to a homothety and its inverse) it forces the two change-of-basis determinants to be positive with product 1.

theorem Chudnovsky.exists_sl2_of_lattice_eq {σ₁ σ₂ : UpperHalfPlane} {a : ℂˣ} (hlat : (Lτ σ₁).lattice = (a • Lτ σ₂).lattice) : ∃ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), σ₂ = γ • σ₁

Step 4 of the lattice-recovery core: if the lattice of L_{σ₁} equals the lattice of the homothety a • L_{σ₂}, then σ₂ = γ • σ₁ for some γ ∈ SL(2, ℤ). The two bases (1, σ₁) and (a, a·σ₂) of the common lattice are related by integer matrices in both directions; orient_eq forces both determinants to be 1, and the Möbius formula finishes.

theorem Chudnovsky.lattice_recovery_core (σ₁ σ₂ : UpperHalfPlane) (a : ℂˣ) (hg2 : (a • Lτ σ₂).g₂ = (Lτ σ₁).g₂) (hg3 : (a • Lτ σ₂).g₃ = (Lτ σ₁).g₃) : ∃ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), σ₂ = γ • σ₁

The lattice-recovery core (the hypothesis of j_injective_mod_Γ_of_lattice_core, now a theorem): a homothety matching g₂ and g₃ forces the base points to be Γ-equivalent. Chains steps 1–4 above.

theorem Chudnovsky.j_injective_mod_Γ {τ₁ τ₂ : UpperHalfPlane} (h : j τ₁ = j τ₂) : ∃ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), τ₂ = γ • τ₁

Injectivity of j mod Γ (§4.3, unconditional): j τ₁ = j τ₂ forces τ₂ = γ • τ₁ for some γ ∈ SL(2, ℤ).

Surjectivity (§4.3, unconditional)

j : ℍ → ℂ is surjective, proved by the open-and-closed argument of §4.3: the image j(ℍ) = Set.range j is nonempty, open and closed in the (pre)connected space ℂ, hence all of ℂ.

• Open image (isOpen_range_j): j is holomorphic (mdifferentiable_j) and nonconstant (j_two_values), so by Mathlib's open mapping theorem AnalyticOnNhd.is_constant_or_isOpen on the connected open set {z : ℂ | 0 < z.im} (transferring MDifferentiable to DifferentiableOn (j ∘ ofComplex) via UpperHalfPlane.mdifferentiable_iff), j(ℍ) is open.
• Closed image (isClosed_range_j): if j τ_n → w, move each τ_n into the closed fundamental domain 𝒟 (exists_smul_mem_fd_j). The cusp estimate theonaeherJ_lower (0.737/‖q‖ < ‖1728·J‖ on Im τ > 5/4) bounds Im τ_n above (else ‖j τ_n‖ → ∞) while 𝒟 bounds it below (three_le_four_mul_im_sq_of_mem_fd), so the τ_n lie in a compact truncation of 𝒟; a convergent subsequence (Heine–Borel + IsCompact.tendsto_subseq) has limit in ℍ, and continuity of j gives w = j(limit) ∈ j(ℍ).
• Clopen ⇒ ℂ (j_surjective): IsClopen.eq_univ on the preconnected space ℂ.

theorem Chudnovsky.j_two_values : ∃ (τ₁ : UpperHalfPlane) (τ₂ : UpperHalfPlane), j τ₁ ≠ j τ₂

Two explicit points of ℍ at which j takes different values (the nonconstancy witness for the open mapping theorem). Uses the cusp bracketing theonaeherJ_lower/theonaeherJ_upper: at im = 3 the lower bound 0.737·e^{6π} exceeds the upper bound 1.321·e^{4π} at im = 2.

theorem Chudnovsky.range_j_eq_image : j ∘ ↑UpperHalfPlane.ofComplex '' UpperHalfPlane.upperHalfPlaneSet = Set.range j

Set.range j = (j ∘ ofComplex) '' {z : ℂ | 0 < z.im}, the ℂ-picture of the image.

theorem Chudnovsky.isOpen_range_j : IsOpen (Set.range j)

The image of j is open (open mapping theorem for the nonconstant holomorphic j).

theorem Chudnovsky.isClosed_range_j : IsClosed (Set.range j)

The image of j is closed: a limit w of j-values is a j-value. Move the approximating points into 𝒟, bound their imaginary parts (above by the cusp estimate, below by 𝒟), extract a convergent subsequence in a compact truncation of 𝒟, and use continuity.

theorem Chudnovsky.j_surjective : Function.Surjective j

Surjectivity of the modular j-function (§4.3, unconditional): every complex number is a j-value. The image Set.range j is nonempty, open (isOpen_range_j) and closed (isClosed_range_j) in the preconnected space ℂ, hence all of ℂ.