Mazur 13 port: exists_scaled_pade_graph

Proved

MazurProof.N13MumfordFullKummerIdentityFiber.exists_scaled_pade_graph

by xuanji · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

huang-flt-portmazur-full-torsionmazur-n13-portorder13

A rational graph scalar rescales the Padé cubic into the actual graph polynomial used by Cantor's identity. The same construction works for both the linear and quadratic quotient branches.

This lemma is one step of a machine-checked proof that the genus-two curve

Y^2 = X^6+4X^5+6X^4+2X^3+X^2+2X+1

(a model of $X_1(13)$ ) has no rational affine points other than the cusps $X\in\{0,-1\}$ , which gives the case $N=13$ of Mazur's torsion theorem. The proof is Xiang Huang's Lean development, ported to this Mathlib and split into one node per large lemma; definitions live in the layered entries MazurN13_L0, MazurN13_L1, ….

Preamble

import Mathlib
import Definitions.Def_MazurN13_L1

open MazurProof MazurProof.N13MumfordFullKummerIdentityFiber
open Polynomial
open SexticMumford
open scoped nonZeroDivisors
universe u
variable {K : Type u} [Field K]

Formal statement

theorem MazurProof.N13MumfordFullKummerIdentityFiber.exists_scaled_pade_graph (D : LowRep) (q : ℚˣ) (a l : ℚ[X]) (c b : ℚ) (hrelation : Polynomial.C (q : ℚ) * l ^ 2 - a ^ 2 * D.toSemi.u = Polynomial.C c * N13Mumford.f ℚ) (hb : b ≠ 0) (hbSq : b ^ 2 = c / (q : ℚ)) (hgraph : D.toSemi.u ∣ l - Polynomial.C b * D.toSemi.v) (hc : c ≠ 0) : ∃ L₀ : ℚ[X], ∃ κ : ℚˣ, N13Mumford.f ℚ - L₀ ^ 2 = a ^ 2 * (Polynomial.C (κ : ℚ) * D.toSemi.u) ∧ D.toSemi.u ∣ L₀ - D.toSemi.v := by sorry

Source

Xiang Huang, FLT fork, https://github.com/xiangyazi24/FLT/blob/51bbb4f/FLT/Assumptions/MazurProof/N13MumfordFullKummerIdentityFiber.lean#L1364

View graph