The order-three orbit of the order-seven resultant

The generic pseudo-remainder certificate computes the bounded resultant against the first division cofactor. The order-three parameter symmetry transports coprimality twice around its orbit, producing the other two bounded resultants required by the stable obstruction consumer.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.bounded_resultants_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 ∧ (selectionCofactor d).resultant (divisionCofactor1 d) 33 7 ≠ 0 ∧ (selectionCofactor d).resultant (divisionCofactor2 d) 33 7 ≠ 0

The six checked recurrences and the remaining recurrence hypothesis make all three bounded resultants nonzero at every nonsingular order-seven Kubert parameter.