Recurrence 4 lookup certificate: three scalar residual identities #
This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.scalarResidual4Coefficient1 :
remainder5Coefficient3 ^ 2 * remainder4Coefficient1 = remainder5Coefficient0 * remainder5Coefficient3 * remainder4Coefficient4 + remainder5Coefficient1 * (remainder5Coefficient3 * remainder4Coefficient3 - remainder5Coefficient2 * remainder4Coefficient4) + remainder4Coefficient4 ^ 2 * exceptional4 * remainder6Coefficient1
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.scalarResidual4Coefficient2 :
remainder5Coefficient3 ^ 2 * remainder4Coefficient2 = remainder5Coefficient1 * remainder5Coefficient3 * remainder4Coefficient4 + remainder5Coefficient2 * (remainder5Coefficient3 * remainder4Coefficient3 - remainder5Coefficient2 * remainder4Coefficient4) + remainder4Coefficient4 ^ 2 * exceptional4 * remainder6Coefficient2