The geometric order-seven backtracking obstruction

This file isolates the lightweight geometric part of the backtracking argument from the large factor and resultant certificates. It turns a non-simultaneous-vanishing statement for the two relevant polynomials into the missing nonbacktracking hypothesis in the order-seven isogeny tower.

theorem MazurTorsion.Kubert.orderSevenQuotient_preΨ_seven_eval_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) : Polynomial.eval (orderSevenVeluX d x) ((orderSevenQuotient d).preΨ' 7) = 0

The image on the quotient curve of an order-49 point satisfying the kernel condition is a root of the quotient seventh division polynomial.

theorem MazurTorsion.Kubert.orderSevenResidualHauptmodul_ne_fricke_of_obstruction {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) (hobstruction : orderSevenSelectionPolynomial d (orderSevenVeluX d x) ≠ 0 ∨ Polynomial.eval (orderSevenVeluX d x) ((orderSevenQuotient d).preΨ' 7) ≠ 0) : orderSevenResidualHauptmodul d x y ≠ orderSevenFrickeParameter d

If the backtracking selection polynomial and the quotient seventh division polynomial cannot both vanish, the residual Hauptmodul is not the Fricke parameter.

theorem MazurTorsion.Kubert.orderSevenG7F_residual_eq_zero_of_order_fortyNine_of_obstruction {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) (hobstruction : orderSevenSelectionPolynomial d (orderSevenVeluX d x) ≠ 0 ∨ Polynomial.eval (orderSevenVeluX d x) ((orderSevenQuotient d).preΨ' 7) ≠ 0) : orderSevenG7F (orderSevenFrickeParameter d) (orderSevenResidualHauptmodul d x y) = 0

A polynomial nonvanishing obstruction supplies the missing nonbacktracking hypothesis in the existing order-seven isogeny-tower theorem.