Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence0InnerPart2

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.recurrence0Inner12 :
selectionCofactorCoefficient12 = divisionCofactor0Coefficient0 * quotient0Coefficient12 + divisionCofactor0Coefficient1 * quotient0Coefficient11 + divisionCofactor0Coefficient2 * quotient0Coefficient10 + divisionCofactor0Coefficient3 * quotient0Coefficient9 + divisionCofactor0Coefficient4 * quotient0Coefficient8 + divisionCofactor0Coefficient5 * quotient0Coefficient7 + divisionCofactor0Coefficient6 * quotient0Coefficient6 + divisionCofactor0Coefficient7 * quotient0Coefficient5
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner13 :
selectionCofactorCoefficient13 = divisionCofactor0Coefficient0 * quotient0Coefficient13 + divisionCofactor0Coefficient1 * quotient0Coefficient12 + divisionCofactor0Coefficient2 * quotient0Coefficient11 + divisionCofactor0Coefficient3 * quotient0Coefficient10 + divisionCofactor0Coefficient4 * quotient0Coefficient9 + divisionCofactor0Coefficient5 * quotient0Coefficient8 + divisionCofactor0Coefficient6 * quotient0Coefficient7 + divisionCofactor0Coefficient7 * quotient0Coefficient6
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner14 :
selectionCofactorCoefficient14 = divisionCofactor0Coefficient0 * quotient0Coefficient14 + divisionCofactor0Coefficient1 * quotient0Coefficient13 + divisionCofactor0Coefficient2 * quotient0Coefficient12 + divisionCofactor0Coefficient3 * quotient0Coefficient11 + divisionCofactor0Coefficient4 * quotient0Coefficient10 + divisionCofactor0Coefficient5 * quotient0Coefficient9 + divisionCofactor0Coefficient6 * quotient0Coefficient8 + divisionCofactor0Coefficient7 * quotient0Coefficient7
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner15 :
selectionCofactorCoefficient15 = divisionCofactor0Coefficient0 * quotient0Coefficient15 + divisionCofactor0Coefficient1 * quotient0Coefficient14 + divisionCofactor0Coefficient2 * quotient0Coefficient13 + divisionCofactor0Coefficient3 * quotient0Coefficient12 + divisionCofactor0Coefficient4 * quotient0Coefficient11 + divisionCofactor0Coefficient5 * quotient0Coefficient10 + divisionCofactor0Coefficient6 * quotient0Coefficient9 + divisionCofactor0Coefficient7 * quotient0Coefficient8
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner16 :
selectionCofactorCoefficient16 = divisionCofactor0Coefficient0 * quotient0Coefficient16 + divisionCofactor0Coefficient1 * quotient0Coefficient15 + divisionCofactor0Coefficient2 * quotient0Coefficient14 + divisionCofactor0Coefficient3 * quotient0Coefficient13 + divisionCofactor0Coefficient4 * quotient0Coefficient12 + divisionCofactor0Coefficient5 * quotient0Coefficient11 + divisionCofactor0Coefficient6 * quotient0Coefficient10 + divisionCofactor0Coefficient7 * quotient0Coefficient9
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner17 :
selectionCofactorCoefficient17 = divisionCofactor0Coefficient0 * quotient0Coefficient17 + divisionCofactor0Coefficient1 * quotient0Coefficient16 + divisionCofactor0Coefficient2 * quotient0Coefficient15 + divisionCofactor0Coefficient3 * quotient0Coefficient14 + divisionCofactor0Coefficient4 * quotient0Coefficient13 + divisionCofactor0Coefficient5 * quotient0Coefficient12 + divisionCofactor0Coefficient6 * quotient0Coefficient11 + divisionCofactor0Coefficient7 * quotient0Coefficient10