Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence0InnerPart1

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.recurrence0Inner6 :
selectionCofactorCoefficient6 = divisionCofactor0Coefficient0 * quotient0Coefficient6 + divisionCofactor0Coefficient1 * quotient0Coefficient5 + divisionCofactor0Coefficient2 * quotient0Coefficient4 + divisionCofactor0Coefficient3 * quotient0Coefficient3 + divisionCofactor0Coefficient4 * quotient0Coefficient2 + divisionCofactor0Coefficient5 * quotient0Coefficient1 + divisionCofactor0Coefficient6 * quotient0Coefficient0 + exceptional0 * remainder2Coefficient6
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner7 :
selectionCofactorCoefficient7 = divisionCofactor0Coefficient0 * quotient0Coefficient7 + divisionCofactor0Coefficient1 * quotient0Coefficient6 + divisionCofactor0Coefficient2 * quotient0Coefficient5 + divisionCofactor0Coefficient3 * quotient0Coefficient4 + divisionCofactor0Coefficient4 * quotient0Coefficient3 + divisionCofactor0Coefficient5 * quotient0Coefficient2 + divisionCofactor0Coefficient6 * quotient0Coefficient1 + divisionCofactor0Coefficient7 * quotient0Coefficient0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner8 :
selectionCofactorCoefficient8 = divisionCofactor0Coefficient0 * quotient0Coefficient8 + divisionCofactor0Coefficient1 * quotient0Coefficient7 + divisionCofactor0Coefficient2 * quotient0Coefficient6 + divisionCofactor0Coefficient3 * quotient0Coefficient5 + divisionCofactor0Coefficient4 * quotient0Coefficient4 + divisionCofactor0Coefficient5 * quotient0Coefficient3 + divisionCofactor0Coefficient6 * quotient0Coefficient2 + divisionCofactor0Coefficient7 * quotient0Coefficient1
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner9 :
selectionCofactorCoefficient9 = divisionCofactor0Coefficient0 * quotient0Coefficient9 + divisionCofactor0Coefficient1 * quotient0Coefficient8 + divisionCofactor0Coefficient2 * quotient0Coefficient7 + divisionCofactor0Coefficient3 * quotient0Coefficient6 + divisionCofactor0Coefficient4 * quotient0Coefficient5 + divisionCofactor0Coefficient5 * quotient0Coefficient4 + divisionCofactor0Coefficient6 * quotient0Coefficient3 + divisionCofactor0Coefficient7 * quotient0Coefficient2
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner10 :
selectionCofactorCoefficient10 = divisionCofactor0Coefficient0 * quotient0Coefficient10 + divisionCofactor0Coefficient1 * quotient0Coefficient9 + divisionCofactor0Coefficient2 * quotient0Coefficient8 + divisionCofactor0Coefficient3 * quotient0Coefficient7 + divisionCofactor0Coefficient4 * quotient0Coefficient6 + divisionCofactor0Coefficient5 * quotient0Coefficient5 + divisionCofactor0Coefficient6 * quotient0Coefficient4 + divisionCofactor0Coefficient7 * quotient0Coefficient3
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner11 :
selectionCofactorCoefficient11 = divisionCofactor0Coefficient0 * quotient0Coefficient11 + divisionCofactor0Coefficient1 * quotient0Coefficient10 + divisionCofactor0Coefficient2 * quotient0Coefficient9 + divisionCofactor0Coefficient3 * quotient0Coefficient8 + divisionCofactor0Coefficient4 * quotient0Coefficient7 + divisionCofactor0Coefficient5 * quotient0Coefficient6 + divisionCofactor0Coefficient6 * quotient0Coefficient5 + divisionCofactor0Coefficient7 * quotient0Coefficient4