Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence0InnerPart3

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.recurrence0Inner18 :
selectionCofactorCoefficient18 = divisionCofactor0Coefficient0 * quotient0Coefficient18 + divisionCofactor0Coefficient1 * quotient0Coefficient17 + divisionCofactor0Coefficient2 * quotient0Coefficient16 + divisionCofactor0Coefficient3 * quotient0Coefficient15 + divisionCofactor0Coefficient4 * quotient0Coefficient14 + divisionCofactor0Coefficient5 * quotient0Coefficient13 + divisionCofactor0Coefficient6 * quotient0Coefficient12 + divisionCofactor0Coefficient7 * quotient0Coefficient11
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner19 :
selectionCofactorCoefficient19 = divisionCofactor0Coefficient0 * quotient0Coefficient19 + divisionCofactor0Coefficient1 * quotient0Coefficient18 + divisionCofactor0Coefficient2 * quotient0Coefficient17 + divisionCofactor0Coefficient3 * quotient0Coefficient16 + divisionCofactor0Coefficient4 * quotient0Coefficient15 + divisionCofactor0Coefficient5 * quotient0Coefficient14 + divisionCofactor0Coefficient6 * quotient0Coefficient13 + divisionCofactor0Coefficient7 * quotient0Coefficient12
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner20 :
selectionCofactorCoefficient20 = divisionCofactor0Coefficient0 * quotient0Coefficient20 + divisionCofactor0Coefficient1 * quotient0Coefficient19 + divisionCofactor0Coefficient2 * quotient0Coefficient18 + divisionCofactor0Coefficient3 * quotient0Coefficient17 + divisionCofactor0Coefficient4 * quotient0Coefficient16 + divisionCofactor0Coefficient5 * quotient0Coefficient15 + divisionCofactor0Coefficient6 * quotient0Coefficient14 + divisionCofactor0Coefficient7 * quotient0Coefficient13
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner21 :
selectionCofactorCoefficient21 = divisionCofactor0Coefficient0 * quotient0Coefficient21 + divisionCofactor0Coefficient1 * quotient0Coefficient20 + divisionCofactor0Coefficient2 * quotient0Coefficient19 + divisionCofactor0Coefficient3 * quotient0Coefficient18 + divisionCofactor0Coefficient4 * quotient0Coefficient17 + divisionCofactor0Coefficient5 * quotient0Coefficient16 + divisionCofactor0Coefficient6 * quotient0Coefficient15 + divisionCofactor0Coefficient7 * quotient0Coefficient14
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner22 :
selectionCofactorCoefficient22 = divisionCofactor0Coefficient0 * quotient0Coefficient22 + divisionCofactor0Coefficient1 * quotient0Coefficient21 + divisionCofactor0Coefficient2 * quotient0Coefficient20 + divisionCofactor0Coefficient3 * quotient0Coefficient19 + divisionCofactor0Coefficient4 * quotient0Coefficient18 + divisionCofactor0Coefficient5 * quotient0Coefficient17 + divisionCofactor0Coefficient6 * quotient0Coefficient16 + divisionCofactor0Coefficient7 * quotient0Coefficient15
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner23 :
selectionCofactorCoefficient23 = divisionCofactor0Coefficient0 * quotient0Coefficient23 + divisionCofactor0Coefficient1 * quotient0Coefficient22 + divisionCofactor0Coefficient2 * quotient0Coefficient21 + divisionCofactor0Coefficient3 * quotient0Coefficient20 + divisionCofactor0Coefficient4 * quotient0Coefficient19 + divisionCofactor0Coefficient5 * quotient0Coefficient18 + divisionCofactor0Coefficient6 * quotient0Coefficient17 + divisionCofactor0Coefficient7 * quotient0Coefficient16