Recurrence 4 scalar-zero tail convolution

This internal shard checks the bounded convolution window used at the top eighty coefficients of the fourth pseudo-division scalar identity.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.scalarResidual4Coefficient0_tail (n : ℕ) (hlo : 443 ≤ n) (hhi : n ≤ 522) : Polynomial.coeff recurrence4Scalar0Left n = Polynomial.coeff (recurrence4Scalar0Main + recurrence4Scalar0Exceptional) n