Step 5 data for the order-seven branch-zero resultant PRS

This serial data shard records one normalized primitive remainder and exceptional content factor. Its linear pseudo-division quotient is derived from leading coefficients and checked by the Lean recurrence.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient0Chunk0 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient0Chunk1 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient0Chunk2 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient0Chunk3 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient0Chunk4 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient0Chunk5 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient0Chunk6 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient0Chunk7 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient0Chunk8 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient0Chunk9 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient0Chunk10 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient0Chunk11 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient0Block0 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient0 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient1Chunk0 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient1Chunk1 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient1Chunk2 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient1Chunk3 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient1Chunk4 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient1Chunk5 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient1Chunk6 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient1Chunk7 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient1Chunk8 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient1Chunk9 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient1Chunk10 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient1Block0 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7Coefficient1 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.remainder7 : Bivariate

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.quotient5 : Bivariate

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.exceptionalUnit5 : Coefficient

Internal datum.

Equations

• MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.exceptionalUnit5 = Polynomial.C (1 / (199944508519179168 * 10 ^ 36 + 873514110594451712887216908764160100))

noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.exceptional5 : Coefficient

Internal datum.

Equations

• One or more equations did not get rendered due to their size.

def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5 : Prop

Internal datum.

Equations

• One or more equations did not get rendered due to their size.