The order-seven Tate parametrization

On Tate normal form the marked origin has order seven exactly when

b² - bc - c³ = 0,

and then d = b/c parametrizes X₁(7):

b = d³ - d², c = d² - d, with d ∉ {0,1}.

The discriminant of the parametrized family is d⁷(d-1)⁷(d³-8d²+5d+1), and the X₀(7) hauptmodul value

t₇ = 49d(d-1)/(d³-8d²+5d+1)

satisfies the cleared j-identity used by the composite-level hauptmodul certificates.

theorem MazurTorsion.Kubert.orderSeven_tate_relation (b c : ℚ) (hb : b ≠ 0) (h00 : (tateNormalCurve b c).toAffine.Nonsingular 0 0) (hP0 : WeierstrassCurve.Affine.Point.some 0 0 h00 ≠ 0) (h7 : 7 • WeierstrassCurve.Affine.Point.some 0 0 h00 = 0) : c ≠ 0 ∧ b ^ 2 - b * c - c ^ 3 = 0

On Tate normal form, an origin killed by seven and not by lower multiples satisfies b² - bc - c³ = 0 with c ≠ 0.

theorem MazurTorsion.Kubert.orderSeven_parametrization (b c : ℚ) (hb : b ≠ 0) (hc : c ≠ 0) (hrel : b ^ 2 - b * c - c ^ 3 = 0) : ∃ (d : ℚ), d ≠ 0 ∧ d ≠ 1 ∧ b = d ^ 3 - d ^ 2 ∧ c = d ^ 2 - d

The order-seven relation is rationally parametrized by d = b/c.

theorem MazurTorsion.Kubert.orderSeven_Δ (d : ℚ) : (tateNormalCurve (d ^ 3 - d ^ 2) (d ^ 2 - d)).Δ = d ^ 7 * (d - 1) ^ 7 * (d ^ 3 - 8 * d ^ 2 + 5 * d + 1)

The discriminant of the parametrized order-seven family.

theorem MazurTorsion.Kubert.orderSeven_c₄ (d : ℚ) : (tateNormalCurve (d ^ 3 - d ^ 2) (d ^ 2 - d)).c₄ = (d ^ 2 - d + 1) * (d ^ 6 - 11 * d ^ 5 + 30 * d ^ 4 - 15 * d ^ 3 - 10 * d ^ 2 + 5 * d + 1)

The invariant c₄ of the parametrized order-seven family.

theorem MazurTorsion.Kubert.orderSeven_hauptmodul_identity (d : ℚ) (hd0 : d ≠ 0) (hd1 : d ≠ 1) (hK : d ^ 3 - 8 * d ^ 2 + 5 * d + 1 ≠ 0) : ((49 * d * (d - 1) / (d ^ 3 - 8 * d ^ 2 + 5 * d + 1)) ^ 2 + 13 * (49 * d * (d - 1) / (d ^ 3 - 8 * d ^ 2 + 5 * d + 1)) + 49) * ((49 * d * (d - 1) / (d ^ 3 - 8 * d ^ 2 + 5 * d + 1)) ^ 2 + 245 * (49 * d * (d - 1) / (d ^ 3 - 8 * d ^ 2 + 5 * d + 1)) + 2401) ^ 3 * (tateNormalCurve (d ^ 3 - d ^ 2) (d ^ 2 - d)).Δ = (tateNormalCurve (d ^ 3 - d ^ 2) (d ^ 2 - d)).c₄ ^ 3 * (49 * d * (d - 1) / (d ^ 3 - 8 * d ^ 2 + 5 * d + 1)) ^ 7

The cleared j-identity for the order-seven hauptmodul value on the parametrized family: with t₇ = 49d(d-1)/(d³-8d²+5d+1),

(t₇²+13t₇+49)(t₇²+245t₇+2401)³ · Δ = c₄³ · t₇⁷.