Order-seven specialization of the doubling derivative certificates

This file supplies the seven coefficients and the two small polynomial identities needed to invoke OrderSevenDoublingDerivative.vertical_at_point. The large abscissa identity remains in its independent interpolation module.

def MazurTorsion.Kubert.OrderSevenDoublingSpecialization.a₆ (d : ℚ) : ℚ

Equations

• MazurTorsion.Kubert.OrderSevenDoublingSpecialization.a₆ d = -2 * d * (d - 1) * (d + 1)

def MazurTorsion.Kubert.OrderSevenDoublingSpecialization.a₅ (d : ℚ) : ℚ

Equations

• MazurTorsion.Kubert.OrderSevenDoublingSpecialization.a₅ d = d * (d - 1) * (d ^ 5 + 2 * d ^ 4 - 3 * d ^ 3 + 5 * d ^ 2 - 7 * d + 1)

def MazurTorsion.Kubert.OrderSevenDoublingSpecialization.a₄ (d : ℚ) : ℚ

Equations

• MazurTorsion.Kubert.OrderSevenDoublingSpecialization.a₄ d = -d ^ 3 * (d - 1) ^ 2 * (6 * d ^ 4 - 9 * d ^ 3 + 12 * d ^ 2 - 13 * d - 1)

def MazurTorsion.Kubert.OrderSevenDoublingSpecialization.a₃ (d : ℚ) : ℚ

Equations

• MazurTorsion.Kubert.OrderSevenDoublingSpecialization.a₃ d = d ^ 4 * (d - 1) ^ 3 * (d ^ 5 + d ^ 4 + 4 * d ^ 3 - 8 * d ^ 2 - 7 * d - 1)

def MazurTorsion.Kubert.OrderSevenDoublingSpecialization.a₂ (d : ℚ) : ℚ

Equations

• MazurTorsion.Kubert.OrderSevenDoublingSpecialization.a₂ d = -d ^ 6 * (d - 1) ^ 4 * (d + 1) * (3 * d ^ 2 - 5 * d - 3)

def MazurTorsion.Kubert.OrderSevenDoublingSpecialization.a₁ (d : ℚ) : ℚ

Equations

• MazurTorsion.Kubert.OrderSevenDoublingSpecialization.a₁ d = d ^ 8 * (d - 1) ^ 5 * (d ^ 2 - 3 * d - 3)

def MazurTorsion.Kubert.OrderSevenDoublingSpecialization.a₀ (d : ℚ) : ℚ

Equations

• MazurTorsion.Kubert.OrderSevenDoublingSpecialization.a₀ d = d ^ 10 * (d - 1) ^ 6

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingSpecialization.differentialPolynomial (d : ℚ) : Polynomial ℚ

The polynomial whose evaluation is the cleared Vélu differential numerator.

Equations

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

@[simp]

theorem MazurTorsion.Kubert.OrderSevenDoublingSpecialization.differentialPolynomial_eval (d x : ℚ) : Polynomial.eval x (differentialPolynomial d) = orderSevenVeluDifferentialNumerator d x

theorem MazurTorsion.Kubert.OrderSevenDoublingSpecialization.baseVeluDifferential_eq (d : ℚ) : OrderSevenDoublingDerivative.baseVeluDifferential (a₆ d) (a₅ d) (a₄ d) (a₃ d) (a₂ d) (a₁ d) (a₀ d) (orderSevenB d) (orderSevenC d) = differentialPolynomial d

The generic F'K - 2FK' polynomial specializes to the explicit order-seven differential numerator.

theorem MazurTorsion.Kubert.OrderSevenDoublingSpecialization.kernel_polynomial_identity (d : ℚ) : OrderSevenDoublingDerivative.composedKernel (orderSevenB d) (orderSevenC d) (orderSevenFamily d) = OrderSevenDoublingDerivative.baseKernel (orderSevenB d) (orderSevenC d) * OrderSevenDoublingDerivative.baseVeluDifferential (a₆ d) (a₅ d) (a₄ d) (a₃ d) (a₂ d) (a₁ d) (a₀ d) (orderSevenB d) (orderSevenC d)

The cubic kernel evaluated at the source doubling forms factors as K * N.

theorem MazurTorsion.Kubert.OrderSevenDoublingSpecialization.landing_polynomial_identity (d : ℚ) : OrderSevenDoublingDerivative.targetCompletedCubic (orderSevenQuotient d) (a₆ d) (a₅ d) (a₄ d) (a₃ d) (a₂ d) (a₁ d) (a₀ d) (orderSevenB d) (orderSevenC d) = OrderSevenDoublingDerivative.sourceCompletedCubic (orderSevenFamily d) * OrderSevenDoublingDerivative.baseVeluDifferential (a₆ d) (a₅ d) (a₄ d) (a₃ d) (a₂ d) (a₁ d) (a₀ d) (orderSevenB d) (orderSevenC d) ^ 2

The completed-square cubic of the quotient image is H * N².