Resultant obstruction for order-seven backtracking

This file is the stable consumer boundary between the generated resultant certificates and the geometric backtracking argument. Three nonzero bounded resultants first rule out a common root of the selection cofactor and any of the three quotient cofactors. The factor certificates and the rational nonvanishing of the dual-kernel cubic then lift this to the two geometric polynomials.

Keeping this bridge separate from OrderSevenBacktrackingObstruction prevents the lightweight geometric theorem from importing the memory-heavy factor certificate chain.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.cofactor_eval_obstruction_of_bounded_resultants (d : ℚ) (hres0 : (selectionCofactor d).resultant (divisionCofactor0 d) 33 7 ≠ 0) (hres1 : (selectionCofactor d).resultant (divisionCofactor1 d) 33 7 ≠ 0) (hres2 : (selectionCofactor d).resultant (divisionCofactor2 d) 33 7 ≠ 0) (z : ℚ) : Polynomial.eval z (selectionCofactor d) ≠ 0 ∨ Polynomial.eval z (divisionCofactor0 d * divisionCofactor1 d * divisionCofactor2 d) ≠ 0

Nonzero bounded resultants against all three quotient cofactors rule out their simultaneous vanishing with the selection cofactor at every rational abscissa.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.cofactor_eval_obstruction_of_resultant_recurrences (hrec3 : Internal.ResultantCertificate.recurrence3) (d : ℚ) (hd0 : d ≠ 0) (hd1 : d ≠ 1) (hcubic : d ^ 3 - 8 * d ^ 2 + 5 * d + 1 ≠ 0) (z : ℚ) : Polynomial.eval z (selectionCofactor d) ≠ 0 ∨ Polynomial.eval z (divisionCofactor0 d * divisionCofactor1 d * divisionCofactor2 d) ≠ 0

The six checked recurrences and the remaining recurrence hypothesis discharge all three bounded-resultant hypotheses in the stable cofactor obstruction.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.polynomial_eval_obstruction_of_bounded_resultants (d : ℚ) [(orderSevenFamily d).IsElliptic] (hres0 : (selectionCofactor d).resultant (divisionCofactor0 d) 33 7 ≠ 0) (hres1 : (selectionCofactor d).resultant (divisionCofactor1 d) 33 7 ≠ 0) (hres2 : (selectionCofactor d).resultant (divisionCofactor2 d) 33 7 ≠ 0) (z : ℚ) : orderSevenSelectionPolynomial d z ≠ 0 ∨ Polynomial.eval z ((orderSevenQuotient d).preΨ' 7) ≠ 0

Nonzero bounded resultants lift through the certified factorizations to show that the backtracking selection polynomial and quotient seventh division polynomial cannot both vanish at a rational abscissa.

theorem MazurTorsion.Kubert.orderSevenResidualHauptmodul_ne_fricke_of_bounded_resultants {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) (hres0 : (OrderSevenBacktrackingCertificate.selectionCofactor d).resultant (OrderSevenBacktrackingCertificate.divisionCofactor0 d) 33 7 ≠ 0) (hres1 : (OrderSevenBacktrackingCertificate.selectionCofactor d).resultant (OrderSevenBacktrackingCertificate.divisionCofactor1 d) 33 7 ≠ 0) (hres2 : (OrderSevenBacktrackingCertificate.selectionCofactor d).resultant (OrderSevenBacktrackingCertificate.divisionCofactor2 d) 33 7 ≠ 0) : orderSevenResidualHauptmodul d x y ≠ orderSevenFrickeParameter d

Three nonzero bounded resultants certify that the residual Hauptmodul of an order-49 point satisfying the kernel condition is not the Fricke parameter.

theorem MazurTorsion.Kubert.orderSevenG7F_residual_eq_zero_of_order_fortyNine_of_bounded_resultants {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) (hres0 : (OrderSevenBacktrackingCertificate.selectionCofactor d).resultant (OrderSevenBacktrackingCertificate.divisionCofactor0 d) 33 7 ≠ 0) (hres1 : (OrderSevenBacktrackingCertificate.selectionCofactor d).resultant (OrderSevenBacktrackingCertificate.divisionCofactor1 d) 33 7 ≠ 0) (hres2 : (OrderSevenBacktrackingCertificate.selectionCofactor d).resultant (OrderSevenBacktrackingCertificate.divisionCofactor2 d) 33 7 ≠ 0) : orderSevenG7F (orderSevenFrickeParameter d) (orderSevenResidualHauptmodul d x y) = 0

Three nonzero bounded resultants discharge the nonbacktracking hypothesis in the order-seven isogeny-tower equation for an order-49 point.