Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupLeadingSquare

Recurrence 2 lookup certificate: LeadingSquare degree bound #

This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_natDegree_le :
Polynomial.natDegree recurrence2LeadingSquare ≤ 268
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_high (n : ℕ) (h : 268 < n) :
Polynomial.coeff recurrence2LeadingSquare n = 0