Generic resultant certificate for order-seven backtracking

This file checks the degree and leading-coefficient side conditions for the primitive pseudo-remainder sequence and telescopes its seven recurrences to the factored generic resultant. The recurrence proofs are separate exact-arithmetic certificate shards.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.generic_resultant_eq_resultantFactorData (hrec3 : Internal.ResultantCertificate.recurrence3) : selectionCofactorData.resultant divisionCofactorData0 33 7 = resultantFactorData

The six checked pseudo-remainder recurrences and the remaining recurrence hypothesis imply the exact factorization of the first bounded resultant over ℚ[D].

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.selection_divisionCofactor0_resultant_eq_resultantFactorData_eval (hrec3 : Internal.ResultantCertificate.recurrence3) (d : ℚ) : (selectionCofactor d).resultant (divisionCofactor0 d) 33 7 = Polynomial.eval d resultantFactorData

Specializing the checked generic identity gives the first bounded resultant without requiring the selection cofactor to preserve its degree.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.selection_divisionCofactor0_resultant_ne_zero (hrec3 : Internal.ResultantCertificate.recurrence3) (d : ℚ) (hd0 : d ≠ 0) (hd1 : d ≠ 1) (hcubic : d ^ 3 - 8 * d ^ 2 + 5 * d + 1 ≠ 0) : (selectionCofactor d).resultant (divisionCofactor0 d) 33 7 ≠ 0

The first bounded resultant is nonzero at every nonsingular Kubert parameter once the remaining primitive pseudo-remainder recurrence is known.