The m-isogeny coset orbit of j (Phase C, chunk B2)

Second file of Track 1 of Phase C (see Playground/Pi/PhaseC-PLAN.md, §3.1 sub-lemma (B2) and §6.5 decision point 2). For a prime m (kept generic; the project instantiates m ∈ {41, 43, 61, 163} later) this file builds the degree-m isogeny orbit of the j-invariant: the m + 1 functions

• f_∞(τ) = j (m·τ) — from the Hermite-normal-form matrix [[m,0],[0,1]];
• f_b(τ) = j ((τ + b)/m) for b = 0, …, m-1 — from the matrices [[1,b],[0,m]].

indexed by Option (ZMod m) (none ↦ f_∞, some b ↦ f_b). The point maps are realized through Mathlib's GL (Fin 2) ℝ-action on ℍ (UpperHalfPlane.MoebiusAction), the choice recommended by the plan's trap list ("pick one action early and stick to it").

The (B2) deliverables:

• f : the m + 1 orbit functions, and mdifferentiable_f : each is holomorphic on ℍ;
• f_some_congr : well-definedness mod m (the some-index really lives on ZMod m);
• T-permutation f_T_smul: f i (T • τ) = f (σ_T i) τ with σ_T the rotation none ↦ none, some b ↦ some (b + 1);
• S-permutation f_S_smul: f i (S • τ) = f (σ_S i) τ with σ_S the involution none ↔ some 0, some b ↦ some (-b⁻¹) (b ≠ 0; needs m prime for the field inverse);
• the master statement f_SL_perm : the multiset {f i τ} is permuted by every S/T generator (hence SL(2,ℤ)-invariant), packaged as the pair of permutation lemmas.

q-expansions in the base variable w = exp(2πiτ/m) (decision point 2)

Rather than Puiseux series in q^{1/m}, we follow the clean formulation flagged in the plan brief: introduce the honest holomorphic function w = wParam m τ = exp(2πiτ/m) (a genuine power series variable, no root-taking) and the constant ζ = zetaM m = exp(2πi/m). The nome factorizes on each coset point:

• q_Acol_smul : q ((τ+b)/m) = ζ^b · w;
• q_AInf_smul : q (m·τ) = w^{m²},

so composing JFunction's integer expansion hasSum_j_mul_q gives, for every τ,

• hasSum_f_some : HasSum (fun n ↦ c n · (ζ^b·w)^n) (f (some b) τ · ζ^b·w);
• hasSum_f_none : HasSum (fun n ↦ c n · (w^{m²})^n) (f none τ · w^{m²}),

with c n = jqInt.coeff n ∈ ℤ the integer j-coefficients. The b-dependence is exactly ζ^{bn}, which is what powers the root-of-unity averaging of ModularPolynomialQ.lean's (B3).

The coset matrices and their action on ℍ

noncomputable def Chudnovsky.AInf (m : ℕ) [NeZero m] : GL (Fin 2) ℝ

The Hermite-normal-form matrix [[m,0],[0,1]] of determinant m, as an element of GL (Fin 2) ℝ; its Möbius action is τ ↦ m·τ.

Equations

• Chudnovsky.AInf m = Matrix.GeneralLinearGroup.mkOfDetNeZero !![↑m, 0; 0, 1] ⋯

noncomputable def Chudnovsky.Acol (m : ℕ) [NeZero m] (b : ℤ) : GL (Fin 2) ℝ

The Hermite-normal-form matrix [[1,b],[0,m]] of determinant m, as an element of GL (Fin 2) ℝ; its Möbius action is τ ↦ (τ + b)/m.

Equations

• Chudnovsky.Acol m b = Matrix.GeneralLinearGroup.mkOfDetNeZero !![1, ↑b; 0, ↑m] ⋯

@[simp]

theorem Chudnovsky.val_AInf {m : ℕ} [NeZero m] : ↑(AInf m) = !![↑m, 0; 0, 1]

@[simp]

theorem Chudnovsky.val_Acol {m : ℕ} [NeZero m] (b : ℤ) : ↑(Acol m b) = !![1, ↑b; 0, ↑m]

theorem Chudnovsky.det_AInf_pos {m : ℕ} [NeZero m] : 0 < ↑(Matrix.GeneralLinearGroup.det (AInf m))

theorem Chudnovsky.det_Acol_pos {m : ℕ} [NeZero m] (b : ℤ) : 0 < ↑(Matrix.GeneralLinearGroup.det (Acol m b))

theorem Chudnovsky.coe_AInf_smul {m : ℕ} [NeZero m] (τ : UpperHalfPlane) : ↑(AInf m • τ) = ↑m * ↑τ

The ∞-coset point: AInf m • τ = m·τ.

theorem Chudnovsky.coe_Acol_smul {m : ℕ} [NeZero m] (b : ℤ) (τ : UpperHalfPlane) : ↑(Acol m b • τ) = (↑τ + ↑b) / ↑m

The b-coset point: Acol m b • τ = (τ + b)/m.

The orbit functions and holomorphy

noncomputable def Chudnovsky.f (m : ℕ) [NeZero m] : Option (ZMod m) → UpperHalfPlane → ℂ

The m + 1 coset-orbit functions: f none τ = j (m·τ) and f (some b) τ = j ((τ+b)/m). Indexed by Option (ZMod m).

Equations

• Chudnovsky.f m none x✝ = Chudnovsky.j (Chudnovsky.AInf m • x✝)
• Chudnovsky.f m (some b) x✝ = Chudnovsky.j (Chudnovsky.Acol m ↑b.val • x✝)

@[simp]

theorem Chudnovsky.f_none {m : ℕ} [NeZero m] (τ : UpperHalfPlane) : f m none τ = j (AInf m • τ)

@[simp]

theorem Chudnovsky.f_some {m : ℕ} [NeZero m] (b : ZMod m) (τ : UpperHalfPlane) : f m (some b) τ = j (Acol m ↑b.val • τ)

theorem Chudnovsky.mdifferentiable_f {m : ℕ} [NeZero m] (i : Option (ZMod m)) : MDiff (f m i)

Each orbit function is holomorphic on ℍ.

j under integer translation and well-definedness of the b-cosets mod m

theorem Chudnovsky.j_vadd_int (n : ℤ) (τ : UpperHalfPlane) : j (↑n +ᵥ τ) = j τ

j is invariant under translation by any integer: j (n +ᵥ τ) = j τ.

theorem Chudnovsky.j_Acol_smul_congr {m : ℕ} [NeZero m] {a a' : ℤ} (h : ↑m ∣ a' - a) (τ : UpperHalfPlane) : j (Acol m a' • τ) = j (Acol m a • τ)

The b-coset function depends only on b mod m: if m ∣ a' - a then j ((τ+a')/m) = j ((τ+a)/m) (adding m to the offset shifts the point by an integer, which j absorbs).

The T-permutation

T • τ = τ + 1 cyclically permutes the b-cosets (b ↦ b + 1) and fixes f_∞.

def Chudnovsky.σT (m : ℕ) : Equiv.Perm (Option (ZMod m))

The permutation of the orbit induced by T: rotation some b ↦ some (b+1), none fixed.

Equations

• Chudnovsky.σT m = Equiv.optionCongr (Equiv.addRight 1)

@[simp]

theorem Chudnovsky.σT_none {m : ℕ} : (σT m) none = none

@[simp]

theorem Chudnovsky.σT_some {m : ℕ} (b : ZMod m) : (σT m) (some b) = some (b + 1)

theorem Chudnovsky.f_T_smul {m : ℕ} [NeZero m] (i : Option (ZMod m)) (τ : UpperHalfPlane) : f m i (1 +ᵥ τ) = f m ((σT m) i) τ

T-permutation: f i (T • τ) = f (σT i) τ, i.e. f i (τ + 1) = f (σT i) τ.

The S-permutation

S • τ = -1/τ. The key transfer lemma: if the GL-matrix A factors as ↑γ * B with γ ∈ SL(2,ℤ), then j (A • τ) = j (B • τ) (the SL(2,ℤ)-factor is absorbed by j_smul). All S-orbit identities are instances of a single matrix identity coset i · S = γ' · coset (σS i).

theorem Chudnovsky.j_matrix_transfer (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (A B : GL (Fin 2) ℝ) (τ : UpperHalfPlane) (h : A = Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ) * B) : j (A • τ) = j (B • τ)

Absorb an SL(2,ℤ) left factor of a GL-matrix into j-invariance.

def Chudnovsky.sSfun (m : ℕ) [Fact (Nat.Prime m)] : Option (ZMod m) → Option (ZMod m)

The permutation of the orbit induced by S: the involution swapping none ↔ some 0 and sending some b ↦ some (-b⁻¹) for b ≠ 0 (needs m prime for the field inverse).

Equations

• Chudnovsky.sSfun m none = some 0
• Chudnovsky.sSfun m (some b) = if b = 0 then none else some (-b⁻¹)

theorem Chudnovsky.sSfun_involutive {m : ℕ} [Fact (Nat.Prime m)] : Function.Involutive (sSfun m)

def Chudnovsky.σS (m : ℕ) [Fact (Nat.Prime m)] : Equiv.Perm (Option (ZMod m))

The S-permutation as an Equiv.Perm.

Equations

• Chudnovsky.σS m = Function.Involutive.toPerm (Chudnovsky.sSfun m) ⋯

@[simp]

theorem Chudnovsky.σS_apply {m : ℕ} [Fact (Nat.Prime m)] (i : Option (ZMod m)) : (σS m) i = sSfun m i

theorem Chudnovsky.f_S_smul {m : ℕ} [Fact (Nat.Prime m)] (i : Option (ZMod m)) (τ : UpperHalfPlane) : f m i (ModularGroup.S • τ) = f m ((σS m) i) τ

S-permutation: f i (S • τ) = f (σS i) τ, i.e. f i (-1/τ) = f (σS i) τ. This is what makes the elementary symmetric functions of the orbit SL(2,ℤ)-invariant.

q-expansions in the base variable w = exp(2πiτ/m)

The clean formulation of decision point 2: everything is a genuine power series in the honest holomorphic function w = wParam m τ = exp(2πiτ/m) (no root-taking), with the m-th root of unity ζ = zetaM m = exp(2πi/m). The nome factorizes on each coset point, and composing JFunction's integer expansion hasSum_j_mul_q yields the coefficientwise HasSum statements consumed by ModularPolynomialQ.lean's (B3).

noncomputable def Chudnovsky.wParam (m : ℕ) (τ : UpperHalfPlane) : ℂ

The base variable w = exp(2πiτ/m): an honest holomorphic function of τ (no q^{1/m}), with w^m = q τ.

Equations

• Chudnovsky.wParam m τ = Complex.exp (2 * ↑Real.pi * Complex.I * ↑τ / ↑m)

noncomputable def Chudnovsky.zetaM (m : ℕ) : ℂ

The m-th root of unity ζ = exp(2πi/m).

Equations

• Chudnovsky.zetaM m = Complex.exp (2 * ↑Real.pi * Complex.I / ↑m)

theorem Chudnovsky.wParam_ne_zero {m : ℕ} (τ : UpperHalfPlane) : wParam m τ ≠ 0

theorem Chudnovsky.zetaM_ne_zero {m : ℕ} : zetaM m ≠ 0

theorem Chudnovsky.wParam_pow_m {m : ℕ} [NeZero m] (τ : UpperHalfPlane) : wParam m τ ^ m = q τ

w^m = q τ: raising the base variable to the m-th power recovers the ordinary nome.

theorem Chudnovsky.zetaM_pow_m {m : ℕ} [NeZero m] : zetaM m ^ m = 1

ζ^m = 1.

theorem Chudnovsky.q_Acol_smul {m : ℕ} [NeZero m] (b : ℤ) (τ : UpperHalfPlane) : q (Acol m b • τ) = zetaM m ^ b * wParam m τ

The nome on the b-coset point factorizes as ζ^b · w: q ((τ+b)/m) = ζ^b · w.

theorem Chudnovsky.q_AInf_smul {m : ℕ} [NeZero m] (τ : UpperHalfPlane) : q (AInf m • τ) = wParam m τ ^ m ^ 2

The nome on the ∞-coset point is w^{m²}: q (m·τ) = w^{m²}.

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

q-expansion of the b-coset function in (ζ^b·w): the HasSum obtained from JFunction's integer j-expansion. The b-dependence is exactly ζ^{b·n} inside (ζ^b w)^n, which powers the root-of-unity averaging of (B3).

theorem Chudnovsky.hasSum_f_none {m : ℕ} [NeZero m] (τ : UpperHalfPlane) : HasSum (fun (n : ℕ) => ↑((PowerSeries.coeff n) jqInt) * (wParam m τ ^ m ^ 2) ^ n) (f m none τ * wParam m τ ^ m ^ 2)

q-expansion of the ∞-coset function in w^{m²}.

Master statement: SL(2,ℤ)-invariance of the orbit's symmetric functions

Since S and T generate SL(2,ℤ), the fact that both permute the multiset {f i τ} (the S/T-permutation lemmas above) makes every symmetric function of the orbit SL(2,ℤ)-invariant. We record the two consequences ModularPolynomialQ.lean's (B3)/(B4) consume directly: any product (e.g. ∏ (X - f i), the elementary symmetric generating polynomial) and any sum (e.g. ∑ (f i)^k, the power sums) of the orbit values is unchanged by each generator.

theorem Chudnovsky.prod_orbit_T_smul {m : ℕ} [NeZero m] {M : Type u_1} [CommMonoid M] (g : ℂ → M) (τ : UpperHalfPlane) : ∏ i : Option (ZMod m), g (f m i (1 +ᵥ τ)) = ∏ i : Option (ZMod m), g (f m i τ)

Any product over the orbit is T-invariant.

theorem Chudnovsky.sum_orbit_T_smul {m : ℕ} [NeZero m] {M : Type u_1} [AddCommMonoid M] (g : ℂ → M) (τ : UpperHalfPlane) : ∑ i : Option (ZMod m), g (f m i (1 +ᵥ τ)) = ∑ i : Option (ZMod m), g (f m i τ)

Any sum over the orbit is T-invariant (e.g. the power sums ∑ (f i)^k).

theorem Chudnovsky.prod_orbit_S_smul {m : ℕ} [Fact (Nat.Prime m)] {M : Type u_1} [CommMonoid M] (g : ℂ → M) (τ : UpperHalfPlane) : ∏ i : Option (ZMod m), g (f m i (ModularGroup.S • τ)) = ∏ i : Option (ZMod m), g (f m i τ)

Any product over the orbit is S-invariant.

theorem Chudnovsky.sum_orbit_S_smul {m : ℕ} [Fact (Nat.Prime m)] {M : Type u_1} [AddCommMonoid M] (g : ℂ → M) (τ : UpperHalfPlane) : ∑ i : Option (ZMod m), g (f m i (ModularGroup.S • τ)) = ∑ i : Option (ZMod m), g (f m i τ)

Any sum over the orbit is S-invariant (e.g. the power sums ∑ (f i)^k).