Recurrence 5 lookup certificate: two scalar residual identities #
This is a checked coefficient-lookup shard for the fifth pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.scalarResidual5Coefficient1 :
remainder6Coefficient2 ^ 2 * remainder5Coefficient1 = remainder6Coefficient0 * remainder6Coefficient2 * remainder5Coefficient3 + remainder6Coefficient1 * (remainder6Coefficient2 * remainder5Coefficient2 - remainder6Coefficient1 * remainder5Coefficient3) + remainder5Coefficient3 ^ 2 * exceptional5 * remainder7Coefficient1