Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence0InnerPart0

Initial resultant recurrence certificates for order-seven branch zero #

This internal proof shard checks a balanced subset of the independent coefficient identities used by the initial pseudo-remainder recurrence.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner0 :
selectionCofactorCoefficient0 = divisionCofactor0Coefficient0 * quotient0Coefficient0 + exceptional0 * remainder2Coefficient0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner1 :
selectionCofactorCoefficient1 = divisionCofactor0Coefficient0 * quotient0Coefficient1 + divisionCofactor0Coefficient1 * quotient0Coefficient0 + exceptional0 * remainder2Coefficient1
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner2 :
selectionCofactorCoefficient2 = divisionCofactor0Coefficient0 * quotient0Coefficient2 + divisionCofactor0Coefficient1 * quotient0Coefficient1 + divisionCofactor0Coefficient2 * quotient0Coefficient0 + exceptional0 * remainder2Coefficient2
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner3 :
selectionCofactorCoefficient3 = divisionCofactor0Coefficient0 * quotient0Coefficient3 + divisionCofactor0Coefficient1 * quotient0Coefficient2 + divisionCofactor0Coefficient2 * quotient0Coefficient1 + divisionCofactor0Coefficient3 * quotient0Coefficient0 + exceptional0 * remainder2Coefficient3
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner4 :
selectionCofactorCoefficient4 = divisionCofactor0Coefficient0 * quotient0Coefficient4 + divisionCofactor0Coefficient1 * quotient0Coefficient3 + divisionCofactor0Coefficient2 * quotient0Coefficient2 + divisionCofactor0Coefficient3 * quotient0Coefficient1 + divisionCofactor0Coefficient4 * quotient0Coefficient0 + exceptional0 * remainder2Coefficient4
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner5 :
selectionCofactorCoefficient5 = divisionCofactor0Coefficient0 * quotient0Coefficient5 + divisionCofactor0Coefficient1 * quotient0Coefficient4 + divisionCofactor0Coefficient2 * quotient0Coefficient3 + divisionCofactor0Coefficient3 * quotient0Coefficient2 + divisionCofactor0Coefficient4 * quotient0Coefficient1 + divisionCofactor0Coefficient5 * quotient0Coefficient0 + exceptional0 * remainder2Coefficient5