Factor certificates for order-seven backtracking

The selection identity has degree at most 36 in the abscissa and is checked at 37 rational values. The quotient seventh division-polynomial identity has degree at most 24 and is checked at 25 rational values. Their pointwise consequences expose only the canonical cofactors needed by the backtracking obstruction.

Both evaluation families are serial import chains so an ordinary build does not check several memory-heavy interpolation shards concurrently.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.orderSevenSelectionPolynomial_eval_factorization (d x : ℚ) : orderSevenSelectionPolynomial d x = 64 ^ 3 * orderSevenDualKernelPolynomial d x * Polynomial.eval x (selectionCofactor d)

Pointwise factorization of the backtracking selection polynomial into the dual-kernel cubic and its degree-33 cofactor.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.orderSevenQuotient_preΨ_seven_eval_factorization (d x : ℚ) : Polynomial.eval x ((orderSevenQuotient d).preΨ' 7) = orderSevenDualKernelPolynomial d x * Polynomial.eval x (divisionCofactor0 d * divisionCofactor1 d * divisionCofactor2 d)

Pointwise factorization of the quotient seventh division polynomial into the dual-kernel cubic and the three canonical degree-seven cofactors.