Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence0InnerPart4

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.recurrence0Inner24 :
selectionCofactorCoefficient24 = divisionCofactor0Coefficient0 * quotient0Coefficient24 + divisionCofactor0Coefficient1 * quotient0Coefficient23 + divisionCofactor0Coefficient2 * quotient0Coefficient22 + divisionCofactor0Coefficient3 * quotient0Coefficient21 + divisionCofactor0Coefficient4 * quotient0Coefficient20 + divisionCofactor0Coefficient5 * quotient0Coefficient19 + divisionCofactor0Coefficient6 * quotient0Coefficient18 + divisionCofactor0Coefficient7 * quotient0Coefficient17
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner25 :
selectionCofactorCoefficient25 = divisionCofactor0Coefficient0 * quotient0Coefficient25 + divisionCofactor0Coefficient1 * quotient0Coefficient24 + divisionCofactor0Coefficient2 * quotient0Coefficient23 + divisionCofactor0Coefficient3 * quotient0Coefficient22 + divisionCofactor0Coefficient4 * quotient0Coefficient21 + divisionCofactor0Coefficient5 * quotient0Coefficient20 + divisionCofactor0Coefficient6 * quotient0Coefficient19 + divisionCofactor0Coefficient7 * quotient0Coefficient18
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner26 :
selectionCofactorCoefficient26 = divisionCofactor0Coefficient0 * quotient0Coefficient26 + divisionCofactor0Coefficient1 * quotient0Coefficient25 + divisionCofactor0Coefficient2 * quotient0Coefficient24 + divisionCofactor0Coefficient3 * quotient0Coefficient23 + divisionCofactor0Coefficient4 * quotient0Coefficient22 + divisionCofactor0Coefficient5 * quotient0Coefficient21 + divisionCofactor0Coefficient6 * quotient0Coefficient20 + divisionCofactor0Coefficient7 * quotient0Coefficient19
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner27 :
selectionCofactorCoefficient27 = divisionCofactor0Coefficient1 * quotient0Coefficient26 + divisionCofactor0Coefficient2 * quotient0Coefficient25 + divisionCofactor0Coefficient3 * quotient0Coefficient24 + divisionCofactor0Coefficient4 * quotient0Coefficient23 + divisionCofactor0Coefficient5 * quotient0Coefficient22 + divisionCofactor0Coefficient6 * quotient0Coefficient21 + divisionCofactor0Coefficient7 * quotient0Coefficient20
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner28 :
selectionCofactorCoefficient28 = divisionCofactor0Coefficient2 * quotient0Coefficient26 + divisionCofactor0Coefficient3 * quotient0Coefficient25 + divisionCofactor0Coefficient4 * quotient0Coefficient24 + divisionCofactor0Coefficient5 * quotient0Coefficient23 + divisionCofactor0Coefficient6 * quotient0Coefficient22 + divisionCofactor0Coefficient7 * quotient0Coefficient21
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner29 :
selectionCofactorCoefficient29 = divisionCofactor0Coefficient3 * quotient0Coefficient26 + divisionCofactor0Coefficient4 * quotient0Coefficient25 + divisionCofactor0Coefficient5 * quotient0Coefficient24 + divisionCofactor0Coefficient6 * quotient0Coefficient23 + divisionCofactor0Coefficient7 * quotient0Coefficient22