Rational nonvanishing factors for the order-seven resultant

The primitive resultant certificate for the order-seven backtracking calculation has two factors not accounted for by the discriminant of the Kubert family. This file records them over ℤ and proves that neither has a rational root. Since both polynomials are monic with constant coefficient one, the rational-root theorem reduces the proof to evaluation at ±1.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.resultantFactorSix : Polynomial ℤ

The degree-six primitive factor in the order-seven resultant.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.resultantFactorTwelve : Polynomial ℤ

The degree-twelve primitive factor in the order-seven resultant.

Equations

• One or more equations did not get rendered due to their size.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.resultantFactorSix_eval_ne_zero (d : ℚ) : Polynomial.eval₂ (Int.castRingHom ℚ) d resultantFactorSix ≠ 0

The primitive degree-six resultant factor has no rational root.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.resultantFactorTwelve_eval_ne_zero (d : ℚ) : Polynomial.eval₂ (Int.castRingHom ℚ) d resultantFactorTwelve ≠ 0

The primitive degree-twelve resultant factor has no rational root.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.resultantFactorData : Polynomial ℚ

The generic first backtracking resultant, factored over the parameter ring. The Bézout certificate has this polynomial as its scalar target.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.resultantFactorData_eval_ne_zero (d : ℚ) (hd0 : d ≠ 0) (hd1 : d ≠ 1) (hcubic : d ^ 3 - 8 * d ^ 2 + 5 * d + 1 ≠ 0) : Polynomial.eval d resultantFactorData ≠ 0

The factored generic resultant is nonzero away from the three singular Kubert parameters.