Masser's Theorem A1 at τ₁₆₃: rationality of s₂ (Phase C, statement 3)

This file discharges the last remaining sorry of the Chudnovsky development, s₂_τ₁₆₃_rational, by formalizing Masser's Appendix A1 argument (LNM 437, Thm. A1), specialized to the CM point τ₁₆₃ = (1 + i√163)/2. See PhaseC-PLAN.md §5.1. The final result is unconditional: masser_s₂_rational : ∃ r : ℚ, s₂ τ₁₆₃ = r (axiom-clean, zero sorry).

Masser's function is ψ(τ) = (3E₄/2E₆)(E₂ − 3/(π Im τ)) = (3/2)·s₂(τ). His theorem gives ψ(τ) ∈ ℚ(j(τ)), and here ℚ(j(τ₁₆₃)) = ℚ (statement 2, already proved).

Structure of Masser's proof (steps 1–5 of the plan)

1. The trace-zero fixing matrix Λ = !![1, −82; 2, −1] (det 163, Λ • τ₁₆₃ = τ₁₆₃, Möbius derivative Λ′(τ₁₆₃) = −1, Λ''(τ₁₆₃) = 4/(2τ − 1)).
2. Λ is a coset of the modular polynomial Φ₁₆₃, so F(z) := Φ₁₆₃(j(Λz), j(z)) vanishes identically on ℍ.
3. Second-order Taylor expansion of F at τ₁₆₃ gives Masser's identity (105): 2·j''/j′ + Λ'' = −j′·γ, with γ = (β₂₀ − β₁₁ + β₀₂)/β₀₁ ∈ ℚ (a ratio of Taylor coefficients of Φ₁₆₃ at (j₀, j₀), all rational since j₀ ∈ ℚ).
4. β₀₁ ≠ 0 (Masser's Lemma A1): the only degree-163 integer matrices fixing τ₁₆₃ are ±Λ, so no other coset value coincides with j₀.
5. The Ramanujan identities deriv_E2/E₄/E₆ turn (105) into Masser's (106): s₂(τ₁₆₃) = 3·j₀·γ + (7j₀ − 6912)/(j₀ − 1728), rational since j₀, γ ∈ ℚ, j₀ ≠ 1728.

What is proved here

Everything, unconditionally:

• all the arithmetic/nonvanishing inputs: j₀ := 1728·J(τ₁₆₃) ∈ ℚ, j₀ ≠ 0, j₀ ≠ 1728, E₄(τ₁₆₃) ≠ 0, E₆(τ₁₆₃) ≠ 0;
• the closed-form modular identity E₄³/E₆² = j₀/(j₀ − 1728);
• the geometric data of steps 1–2 (Λ fixes τ₁₆₃, (2τ − 1)² = −163, the coset factorization Λ = γ · Acol 163 (−82), and the identity j(Λ • z) = f₁₆₃(81) z on all of ℍ — one vanishing factor of Masser's F);
• the full reduction (step 5): given Masser's post-Ramanujan identity (the analytic gate hMasser), s₂(τ₁₆₃) is rational (masser_s₂_rational_of);
• the analytic gate itself (masser_gate, second half of this file): the chart calculus of F(z) = Φ₁₆₃(j(Λz), j z) ≡ 0 (first- and second-derivative extraction at τ₁₆₃, masser_bivariate_derivs), Masser's Lemma A1 (β₁₀ ≠ 0, via the p² − pk + 41k² = 163 fixed-matrix classification), and the Ramanujan substitution turning (105) into the gate identity with γ = (β₂₀ − 2β₁₁ + β₀₂)/β₀₁ ∈ ℚ.

The top-level deliverable is masser_s₂_rational : ∃ r : ℚ, s₂ τ₁₆₃ = r.

instance Chudnovsky.instNeZeroNatOfNat_leanPool : NeZero 163

Step 1 — the trace-zero fixing matrix Λ = !![1, −82; 2, −1]

det Λ = 163, Λ • τ₁₆₃ = τ₁₆₃, and the Möbius square-root data (2τ − 1)² = −163. These are the geometric inputs to Masser's second-order Taylor expansion (step 3).

theorem Chudnovsky.two_tau_sub_one_sq : (2 * ↑τ₁₆₃ - 1) ^ 2 = -163

(2τ₁₆₃ − 1)² = −163, from τ₁₆₃² = τ₁₆₃ − 41. (So 2τ₁₆₃ − 1 = i√163, the pure imaginary generator of the CM order; (2τ − 1)/2 = i·Im τ₁₆₃.)

theorem Chudnovsky.two_tau_sub_one_ne_zero : 2 * ↑τ₁₆₃ - 1 ≠ 0

2τ₁₆₃ − 1 ≠ 0 (its square is −163 ≠ 0).

noncomputable def Chudnovsky.LamGL : GL (Fin 2) ℝ

The trace-zero fixing matrix Λ = !![1, −82; 2, −1] as an element of GL (Fin 2) ℝ (determinant 163 > 0).

Equations

• Chudnovsky.LamGL = Matrix.GeneralLinearGroup.mkOfDetNeZero !![1, -82; 2, -1] Chudnovsky.LamGL._proof_3

@[simp]

theorem Chudnovsky.val_LamGL : ↑LamGL = !![1, -82; 2, -1]

theorem Chudnovsky.LamGL_det_pos : 0 < ↑(Matrix.GeneralLinearGroup.det LamGL)

theorem Chudnovsky.LamGL_smul_eq : LamGL • τ₁₆₃ = τ₁₆₃

Λ fixes τ₁₆₃ as a Möbius transformation: (τ − 82)/(2τ − 1) = τ.

def Chudnovsky.LamGamma : Matrix.SpecialLinearGroup (Fin 2) ℤ

The SL(2,ℤ) cofactor γ = !![1, 0; 2, 1] (determinant 1) of the coset decomposition Λ = γ · Acol 163 (−82).

Equations

• Chudnovsky.LamGamma = ⟨!![1, 0; 2, 1], Chudnovsky.LamGamma._proof_1⟩

theorem Chudnovsky.LamGL_factor : LamGL = Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) LamGamma) * Acol 163 (-82)

Coset decomposition Λ = γ · Acol 163 (−82) in GL (Fin 2) ℝ.

theorem Chudnovsky.j_LamGL_smul (z : UpperHalfPlane) : j (LamGL • z) = f 163 (some 81) z

Step 2 — coset identification. For every z : ℍ, j(Λ • z) equals the 81-coset orbit value f 163 (some 81) z (since −82 ≡ 81 mod 163). Hence one factor of the orbit product Φ₁₆₃(·, j z) vanishes at X = j(Λz), i.e. Masser's F(z) = 0.

Arithmetic and nonvanishing inputs at τ₁₆₃

theorem Chudnovsky.J_τ₁₆₃_ne_zero : J τ₁₆₃ ≠ 0

J(τ₁₆₃) ≠ 0: it has norm > 1 (Estimates one_lt_norm_J).

theorem Chudnovsky.j₀_ne_zero : 1728 * J τ₁₆₃ ≠ 0

j₀ := 1728·J(τ₁₆₃) ≠ 0.

theorem Chudnovsky.j₀_ne_1728 : 1728 * J τ₁₆₃ ≠ 1728

j₀ ≠ 1728: J(τ₁₆₃) ≠ 1 since ‖J(τ₁₆₃)‖ > 1.

theorem Chudnovsky.E₆_τ₁₆₃_ne_zero : ModularForm.E₆ τ₁₆₃ ≠ 0

E₆(τ₁₆₃) ≠ 0 (Estimates E₆_ne_zero_of_mem_Region).

theorem Chudnovsky.E₄_τ₁₆₃_ne_zero : ModularForm.E₄ τ₁₆₃ ≠ 0

E₄(τ₁₆₃) ≠ 0: else j₀ = E₄³/Δ = 0, contradicting j₀ ≠ 0.

theorem Chudnovsky.j₀_rational : ∃ (r : ℚ), 1728 * J τ₁₆₃ = ↑r

j₀ ∈ ℚ (statement 2). Derived locally from Kronecker.lean + Rationality.lean (rather than from the pin file LeanPool.Chudnovsky.SingularModuli, which imports THIS file to fill its s₂_τ₁₆₃_rational pin — importing it here would be a cycle).

The closed-form modular identity E₄³/E₆² = j₀/(j₀ − 1728)

theorem Chudnovsky.E₄_cube_τ₁₆₃ : ModularForm.E₄ τ₁₆₃ ^ 3 = 1728 * J τ₁₆₃ * ModularForm.discriminant τ₁₆₃

E₄³ = j₀·Δ at τ₁₆₃.

theorem Chudnovsky.E₆_sq_τ₁₆₃ : ModularForm.E₆ τ₁₆₃ ^ 2 = (1728 * J τ₁₆₃ - 1728) * ModularForm.discriminant τ₁₆₃

E₆² = (j₀ − 1728)·Δ at τ₁₆₃.

theorem Chudnovsky.E₄_cube_div_E₆_sq_τ₁₆₃ : ModularForm.E₄ τ₁₆₃ ^ 3 / ModularForm.E₆ τ₁₆₃ ^ 2 = 1728 * J τ₁₆₃ / (1728 * J τ₁₆₃ - 1728)

The closed-form identity E₄³/E₆² = j₀/(j₀ − 1728) at τ₁₆₃ (the algebraic heart of the s₂-formula's non-γ term).

The gated top-level theorem (step 5 reduction, fully assembled)

theorem Chudnovsky.masser_s₂_rational_of (hMasser : ∃ (γ : ℚ), E₂star τ₁₆₃ = 3 * (1728 * J τ₁₆₃) * (ModularForm.E₆ τ₁₆₃ / ModularForm.E₄ τ₁₆₃) * ↑γ + 4 * (ModularForm.E₆ τ₁₆₃ / ModularForm.E₄ τ₁₆₃) + 3 * ModularForm.E₄ τ₁₆₃ ^ 2 / ModularForm.E₆ τ₁₆₃) : ∃ (r : ℚ), s₂ τ₁₆₃ = ↑r

Masser's Theorem A1 at τ₁₆₃, assembled around the analytic gate.

hMasser is Masser's identity (106) before solving for s₂: the post-Ramanujan form of his second-order Taylor identity (105), asserting the existence of a rational γ (Masser's (β₂₀ − β₁₁ + β₀₂)/β₀₁ ∈ ℚ) with

E₂*(τ₁₆₃) = 3·j₀·(E₆/E₄)·γ + 4·(E₆/E₄) + 3·E₄²/E₆.

Given it, s₂(τ₁₆₃) = (E₄/E₆)·E₂* = 3·j₀·γ + 4 + 3·E₄³/E₆² = 3·j₀·γ + (7j₀−6912)/(j₀−1728) is rational.

Discharging the analytic gate

The remainder of this file proves the gate hypothesis hMasser of masser_s₂_rational_of and derives the unconditional masser_s₂_rational. Structure:

• Chart calculus (masserLam, cj, masserGD): the Möbius map λ(z) = (z−82)/(2z−1) of Λ and the j-function in the ℂ-chart, with explicit first derivatives on {0 < Im z} and the second derivative of j∘ofComplex at τ₁₆₃ via the Ramanujan identities.
• Master second-derivative lemma (masser_bivariate_derivs): for a finite sum F(z) = Σₙ pₙ(v z)·(u z)ⁿ vanishing on the upper half-plane, the first and second derivatives at an interior point, expanded in the five partial-derivative sums (the Taylor coefficients β₁₀, β₀₁, β₂₀, β₁₁, β₀₂ of Φ₁₆₃ at (j₀, j₀)).
• Vanishing input: F(z) = Φ₁₆₃(j(λz), j z) = 0 on ℍ from j_LamGL_smul (step 2).
• Masser's Lemma A1 (masser_lemmaA1): no coset other than some 81 takes the value j τ₁₆₃ at τ₁₆₃ (the p² − pk + 41k² = 163 classification), whence β₁₀ ≠ 0.
• Assembly: β₁₀ = β₀₁, division by g′(τ)² β₀₁ ≠ 0, and the Ramanujan substitution produce the gate identity with γ = (β₂₀ − 2β₁₁ + β₀₂)/β₀₁ ∈ ℚ.

The Möbius chart map λ(z) = (z − 82)/(2z − 1)

The j-function in the ℂ-chart and its first two derivatives

cj = j ∘ ofComplex, with cj′ = masserGD on {0 < Im z} (from the Ramanujan identities deriv_comp_ofComplex_E₄/E₆), and the explicit second derivative masserG2 at τ₁₆₃.

The master second-derivative lemma

For a finite family of polynomials pₙ ∈ ℂ[X] and functions u, v differentiable on the upper half-plane such that F(z) = Σₙ pₙ(v z)·(u z)ⁿ vanishes identically there, the first and second derivatives of F at an interior point t vanish; expanded by the chain rule they give the two linear relations among the five partial-derivative sums (the β's of Masser's proof) used below.

Support-sum expansions of the specialized modular polynomial

Φ₁₆₃ ∈ ℚ[Y][X] is pinned via exists_PhiQ_closed; we expand Φ₁₆₃(x, Y₀) and its X-derivative as sums over the (finite) support, the form consumed by the master lemma, and record the ℚ-rationality of all evaluations at (j₀, j₀), j₀ = j τ₁₆₃ ∈ ℚ.

The pinned modular polynomial Φ₁₆₃ and the rational β-data

Masser's F(z) = Φ₁₆₃(j(Λz), j z) vanishes identically

The two Taylor relations at τ₁₆₃

Masser's Lemma A1 at τ₁₆₃: β₁₀ ≠ 0

β₁₀ = ∏_{i ≠ some 81} (j₀ − fᵢ(τ₁₆₃)), and no other coset value equals j₀: a coincidence would produce an integer matrix fixing τ₁₆₃ of determinant 163; by the fixed-matrix classification for the primitive form (1, −1, 41) its norm form gives p² − pk + 41k² = 163, whose only solutions are ±(1, 2), i.e. the matrix is ±Λ — and ±Λ lies in the coset some 81.

The gate and the unconditional theorem

theorem Chudnovsky.masser_gate : ∃ (γ : ℚ), E₂star τ₁₆₃ = 3 * (1728 * J τ₁₆₃) * (ModularForm.E₆ τ₁₆₃ / ModularForm.E₄ τ₁₆₃) * ↑γ + 4 * (ModularForm.E₆ τ₁₆₃ / ModularForm.E₄ τ₁₆₃) + 3 * ModularForm.E₄ τ₁₆₃ ^ 2 / ModularForm.E₆ τ₁₆₃

The analytic gate of masser_s₂_rational_of, discharged: Masser's identity (106) before solving for s₂, with γ = (β₂₀ − 2β₁₁ + β₀₂)/β₀₁ ∈ ℚ.

theorem Chudnovsky.masser_s₂_rational : ∃ (r : ℚ), s₂ τ₁₆₃ = ↑r

Masser's Theorem A1 at τ₁₆₃, unconditional (Phase C, statement 3): s₂(τ₁₆₃) ∈ ℚ. This discharges the last analytic input of the Chudnovsky formula.