Recurrence 1 certificate: SourceData

This file is a checked bounded-band arithmetic shard for the first pseudo-division recurrence in the order-seven branch-zero resultant certificate.

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1Source0Block3 = Polynomial.X ^ 27 * -1

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1Source2Block2 = Polynomial.X ^ 18 * (161 + -77 * Polynomial.X ^ 1)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1Source4Block1 = Polynomial.X ^ 9 * (-1799 + 1274 * Polynomial.X ^ 1 + -294 * Polynomial.X ^ 2)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1Source7Block0 = Polynomial.X ^ 0 * 1

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

Equations

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