Polynomial data for the order-seven doubling certificate

This file contains the two degree-28 polynomials and their degree bounds. The pointwise ring certificates are split into serially imported blocks so a cold build does not place the entire normalization proof in one Lean process.

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingCertificate.sourceCompletedCubicPolynomial (d : ℚ) : Polynomial ℚ

Equations

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

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingCertificate.sourceDoubleXPolynomial (d : ℚ) : Polynomial ℚ

Equations

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

@[reducible, inline]

noncomputable abbrev MazurTorsion.Kubert.OrderSevenDoublingCertificate.kernelPolynomial (d : ℚ) : Polynomial ℚ

Compatibility alias for the shared source kernel polynomial.

Equations

• MazurTorsion.Kubert.OrderSevenDoublingCertificate.kernelPolynomial = MazurTorsion.Kubert.OrderSevenIsogenyPolynomialData.kernelPolynomial

@[reducible, inline]

noncomputable abbrev MazurTorsion.Kubert.OrderSevenDoublingCertificate.veluXPolynomial (d : ℚ) : Polynomial ℚ

Compatibility alias for the shared cleared Vélu abscissa polynomial.

Equations

• MazurTorsion.Kubert.OrderSevenDoublingCertificate.veluXPolynomial = MazurTorsion.Kubert.OrderSevenIsogenyPolynomialData.veluXPolynomial

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingCertificate.veluXHomogeneousPolynomial (d : ℚ) (u v : Polynomial ℚ) : Polynomial ℚ

Equations

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

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingCertificate.doubleXHomogeneousPolynomial (W : WeierstrassCurve ℚ) (u v : Polynomial ℚ) : Polynomial ℚ

Equations

• MazurTorsion.Kubert.OrderSevenDoublingCertificate.doubleXHomogeneousPolynomial W u v = u ^ 4 - Polynomial.C W.b₄ * u ^ 2 * v ^ 2 - Polynomial.C (2 * W.b₆) * u * v ^ 3 - Polynomial.C W.b₈ * v ^ 4

theorem MazurTorsion.Kubert.OrderSevenDoublingCertificate.Internal.left_degree (d : ℚ) : (veluXHomogeneousPolynomial d (sourceDoubleXPolynomial d) (sourceCompletedCubicPolynomial d)).natDegree ≤ 28

theorem MazurTorsion.Kubert.OrderSevenDoublingCertificate.Internal.right_degree (d : ℚ) : (doubleXHomogeneousPolynomial (orderSevenQuotient d) (veluXPolynomial d) (kernelPolynomial d ^ 2)).natDegree ≤ 28

def MazurTorsion.Kubert.OrderSevenDoublingCertificate.Internal.EvalCertificate (d n : ℚ) : Prop

Equations

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