Fixed-doubling compatibility for the explicit order-seven isogeny

This file proves the amount of multiplicative compatibility needed by the order-49 tower. It uses denominator-free tangent-doubling coordinates and homogeneous polynomial certificates, avoiding a case analysis for the full binary addition law.

def MazurTorsion.Kubert.orderSevenVeluXNumeratorHomogeneous {R : Type u_1} [CommRing R] (d u v : R) : R

Homogenization of the cleared order-seven Vélu abscissa numerator.

Equations

• One or more equations did not get rendered due to their size.

def MazurTorsion.Kubert.orderSevenVeluDifferentialNumeratorHomogeneous {R : Type u_1} [CommRing R] (d u v : R) : R

Homogenization of the cleared order-seven Vélu differential numerator.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MazurTorsion.Kubert.orderSevenVeluXNumeratorHomogeneous_at_one (d x : ℚ) : orderSevenVeluXNumeratorHomogeneous d x 1 = orderSevenVeluXNumerator d x

@[simp]

theorem MazurTorsion.Kubert.orderSevenVeluDifferentialNumeratorHomogeneous_at_one (d x : ℚ) : orderSevenVeluDifferentialNumeratorHomogeneous d x 1 = orderSevenVeluDifferentialNumerator d x

theorem MazurTorsion.Kubert.orderSevenPointMap_two_nsmul_of_order_fortyNine {d : ℚ} [(orderSevenFamily d).IsElliptic] {Q : (orderSevenFamily d).toAffine.Point} (hQ : addOrderOf Q = 49) : orderSevenPointMap d (2 • Q) = 2 • orderSevenPointMap d Q

On an exact-order-49 point, the explicit total order-seven Vélu map commutes with tangent doubling.

theorem MazurTorsion.Kubert.orderSevenPointMap_seven_nsmul_of_order_fortyNine {d : ℚ} [(orderSevenFamily d).IsElliptic] {Q : (orderSevenFamily d).toAffine.Point} (hQ : addOrderOf Q = 49) (hkernel : orderSevenPointMap d (7 • Q) = 0) : orderSevenPointMap d (7 • Q) = 7 • orderSevenPointMap d Q

If 7 • Q lies in the explicit zero fiber, doubling compatibility and translation invariance force the Vélu map to commute with that multiple.

theorem MazurTorsion.Kubert.addOrderOf_orderSevenPointMap_of_order_fortyNine_of_kernel {d : ℚ} [(orderSevenFamily d).IsElliptic] {Q : (orderSevenFamily d).toAffine.Point} (hQ : addOrderOf Q = 49) (hkernel : orderSevenPointMap d (7 • Q) = 0) : addOrderOf (orderSevenPointMap d Q) = 7

Under the single zero-fiber hypothesis at 7 • Q, the Vélu image of an exact-order-49 point has exact order seven.

theorem MazurTorsion.Kubert.exists_orderSevenHauptmodul_of_order_fortyNine_image_of_kernel {d : ℚ} [(orderSevenFamily d).IsElliptic] {Q : (orderSevenFamily d).toAffine.Point} (hQ : addOrderOf Q = 49) (hkernel : orderSevenPointMap d (7 • Q) = 0) : ∃ (B : ℚ), B ≠ 0 ∧ orderSevenJNumerator B * (orderSevenQuotient d).Δ = (orderSevenQuotient d).c₄ ^ 3 * B ^ 7

The order-49 image supplies a residual level-seven Hauptmodul from the zero-fiber hypothesis alone.

theorem MazurTorsion.Kubert.orderSevenResidualHauptmodul_spec_of_order_fortyNine_of_kernel {d x y : ℚ} [(orderSevenFamily d).IsElliptic] (hP : (orderSevenFamily d).toAffine.Nonsingular x y) (hQ : addOrderOf (WeierstrassCurve.Affine.Point.some x y hP) = 49) (hkernel : orderSevenPointMap d (7 • WeierstrassCurve.Affine.Point.some x y hP) = 0) : orderSevenResidualHauptmodul d x y ≠ 0 ∧ orderSevenJNumerator (orderSevenResidualHauptmodul d x y) * (orderSevenQuotient d).Δ = (orderSevenQuotient d).c₄ ^ 3 * orderSevenResidualHauptmodul d x y ^ 7

The explicit residual Hauptmodul satisfies its quotient identity from the zero-fiber hypothesis alone.

theorem MazurTorsion.Kubert.orderSevenG7F_residual_eq_zero_of_order_fortyNine_of_kernel {d x y : ℚ} [(orderSevenFamily d).IsElliptic] (hP : (orderSevenFamily d).toAffine.Nonsingular x y) (hQ : addOrderOf (WeierstrassCurve.Affine.Point.some x y hP) = 49) (hkernel : orderSevenPointMap d (7 • WeierstrassCurve.Affine.Point.some x y hP) = 0) (hoff : orderSevenFrickeParameter d ≠ orderSevenResidualHauptmodul d x y) : orderSevenG7F (orderSevenFrickeParameter d) (orderSevenResidualHauptmodul d x y) = 0

A nonbacktracking residual Hauptmodul lies on the level-49 correspondence from the zero-fiber hypothesis alone.