Polynomial derivative infrastructure for order-seven doubling

This file isolates the formal-derivative argument used to recover the completed-ordinate certificate from three smaller polynomial identities: the abscissa identity, the kernel identity, and the completed-square landing identity. The degree-seven numerator and cubic denominator are kept generic; the order-seven specialization supplies only their seven coefficients.

def MazurTorsion.Kubert.OrderSevenDoublingDerivative.veluXHomogeneous (a₆ a₅ a₄ a₃ a₂ a₁ a₀ u v : ℚ) : ℚ

A monic degree-seven binary form, written with its seven lower coefficients.

Equations

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

def MazurTorsion.Kubert.OrderSevenDoublingDerivative.veluXHomogeneousDirectional (a₆ a₅ a₄ a₃ a₂ a₁ a₀ u v du dv : ℚ) : ℚ

Directional derivative of veluXHomogeneous.

Equations

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

def MazurTorsion.Kubert.OrderSevenDoublingDerivative.kernelHomogeneous (b c u v : ℚ) : ℚ

Homogenization of the cubic denominator X (X - b) (X - c).

Equations

• MazurTorsion.Kubert.OrderSevenDoublingDerivative.kernelHomogeneous b c u v = u * (u - b * v) * (u - c * v)

def MazurTorsion.Kubert.OrderSevenDoublingDerivative.kernelHomogeneousDirectional (b c u v du dv : ℚ) : ℚ

Directional derivative of kernelHomogeneous.

Equations

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

def MazurTorsion.Kubert.OrderSevenDoublingDerivative.veluDifferentialHomogeneous (a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c u v : ℚ) : ℚ

Homogenization to degree nine of F'K - 2FK', for the degree-seven form F and cubic kernel K.

Equations

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

theorem MazurTorsion.Kubert.OrderSevenDoublingDerivative.veluXHomogeneous_directional (a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c u v du dv : ℚ) : veluXHomogeneousDirectional a₆ a₅ a₄ a₃ a₂ a₁ a₀ u v du dv * v * kernelHomogeneous b c u v - veluXHomogeneous a₆ a₅ a₄ a₃ a₂ a₁ a₀ u v * (dv * kernelHomogeneous b c u v + 2 * v * kernelHomogeneousDirectional b c u v du dv) = veluDifferentialHomogeneous a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c u v * (du * v - u * dv)

Directional numerator identity for a rational function F / K², where F is monic of degree seven and K = X (X-b) (X-c).

Polynomial versions and their chain rules

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingDerivative.completedCubicPolynomial (W : WeierstrassCurve ℚ) (u v : Polynomial ℚ) : Polynomial ℚ

Equations

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

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingDerivative.doubleXPolynomial (W : WeierstrassCurve ℚ) (u v : Polynomial ℚ) : Polynomial ℚ

Equations

• MazurTorsion.Kubert.OrderSevenDoublingDerivative.doubleXPolynomial 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

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingDerivative.doubleCompletedYPolynomial (W : WeierstrassCurve ℚ) (u v : Polynomial ℚ) : Polynomial ℚ

Equations

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

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingDerivative.veluXPolynomial (a₆ a₅ a₄ a₃ a₂ a₁ a₀ : ℚ) (u v : Polynomial ℚ) : Polynomial ℚ

Equations

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

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingDerivative.kernelPolynomial (b c : ℚ) (u v : Polynomial ℚ) : Polynomial ℚ

Equations

• MazurTorsion.Kubert.OrderSevenDoublingDerivative.kernelPolynomial b c u v = u * (u - Polynomial.C b * v) * (u - Polynomial.C c * v)

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingDerivative.veluDifferentialPolynomial (a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c : ℚ) (u v : Polynomial ℚ) : Polynomial ℚ

Equations

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

theorem MazurTorsion.Kubert.OrderSevenDoublingDerivative.eval_completedCubicPolynomial (W : WeierstrassCurve ℚ) (u v : Polynomial ℚ) (x : ℚ) : Polynomial.eval x (completedCubicPolynomial W u v) = Doubling.completedCubicHomogeneous W (Polynomial.eval x u) (Polynomial.eval x v)

theorem MazurTorsion.Kubert.OrderSevenDoublingDerivative.eval_derivative_completedCubicPolynomial (W : WeierstrassCurve ℚ) (u v : Polynomial ℚ) (x : ℚ) : Polynomial.eval x (Polynomial.derivative (completedCubicPolynomial W u v)) = Doubling.completedCubicHomogeneousDirectional W (Polynomial.eval x u) (Polynomial.eval x v) (Polynomial.eval x (Polynomial.derivative u)) (Polynomial.eval x (Polynomial.derivative v))

theorem MazurTorsion.Kubert.OrderSevenDoublingDerivative.eval_doubleXPolynomial (W : WeierstrassCurve ℚ) (u v : Polynomial ℚ) (x : ℚ) : Polynomial.eval x (doubleXPolynomial W u v) = Doubling.xNumeratorHomogeneous W (Polynomial.eval x u) (Polynomial.eval x v)

theorem MazurTorsion.Kubert.OrderSevenDoublingDerivative.eval_derivative_doubleXPolynomial (W : WeierstrassCurve ℚ) (u v : Polynomial ℚ) (x : ℚ) : Polynomial.eval x (Polynomial.derivative (doubleXPolynomial W u v)) = Doubling.xNumeratorHomogeneousDirectional W (Polynomial.eval x u) (Polynomial.eval x v) (Polynomial.eval x (Polynomial.derivative u)) (Polynomial.eval x (Polynomial.derivative v))

theorem MazurTorsion.Kubert.OrderSevenDoublingDerivative.eval_doubleCompletedYPolynomial (W : WeierstrassCurve ℚ) (u v : Polynomial ℚ) (x : ℚ) : Polynomial.eval x (doubleCompletedYPolynomial W u v) = Doubling.completedYNumeratorHomogeneous W (Polynomial.eval x u) (Polynomial.eval x v)

theorem MazurTorsion.Kubert.OrderSevenDoublingDerivative.eval_veluXPolynomial (a₆ a₅ a₄ a₃ a₂ a₁ a₀ : ℚ) (u v : Polynomial ℚ) (x : ℚ) : Polynomial.eval x (veluXPolynomial a₆ a₅ a₄ a₃ a₂ a₁ a₀ u v) = veluXHomogeneous a₆ a₅ a₄ a₃ a₂ a₁ a₀ (Polynomial.eval x u) (Polynomial.eval x v)

theorem MazurTorsion.Kubert.OrderSevenDoublingDerivative.eval_derivative_veluXPolynomial (a₆ a₅ a₄ a₃ a₂ a₁ a₀ : ℚ) (u v : Polynomial ℚ) (x : ℚ) : Polynomial.eval x (Polynomial.derivative (veluXPolynomial a₆ a₅ a₄ a₃ a₂ a₁ a₀ u v)) = veluXHomogeneousDirectional a₆ a₅ a₄ a₃ a₂ a₁ a₀ (Polynomial.eval x u) (Polynomial.eval x v) (Polynomial.eval x (Polynomial.derivative u)) (Polynomial.eval x (Polynomial.derivative v))

theorem MazurTorsion.Kubert.OrderSevenDoublingDerivative.eval_kernelPolynomial (b c : ℚ) (u v : Polynomial ℚ) (x : ℚ) : Polynomial.eval x (kernelPolynomial b c u v) = kernelHomogeneous b c (Polynomial.eval x u) (Polynomial.eval x v)

theorem MazurTorsion.Kubert.OrderSevenDoublingDerivative.eval_derivative_kernelPolynomial (b c : ℚ) (u v : Polynomial ℚ) (x : ℚ) : Polynomial.eval x (Polynomial.derivative (kernelPolynomial b c u v)) = kernelHomogeneousDirectional b c (Polynomial.eval x u) (Polynomial.eval x v) (Polynomial.eval x (Polynomial.derivative u)) (Polynomial.eval x (Polynomial.derivative v))

theorem MazurTorsion.Kubert.OrderSevenDoublingDerivative.eval_veluDifferentialPolynomial (a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c : ℚ) (u v : Polynomial ℚ) (x : ℚ) : Polynomial.eval x (veluDifferentialPolynomial a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c u v) = veluDifferentialHomogeneous a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c (Polynomial.eval x u) (Polynomial.eval x v)

The common-denominator derivative argument

End-to-end reusable vertical certificate

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingDerivative.sourceCompletedCubic (W : WeierstrassCurve ℚ) : Polynomial ℚ

Equations

• MazurTorsion.Kubert.OrderSevenDoublingDerivative.sourceCompletedCubic W = MazurTorsion.Kubert.OrderSevenDoublingDerivative.completedCubicPolynomial W Polynomial.X 1

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingDerivative.sourceDoubleX (W : WeierstrassCurve ℚ) : Polynomial ℚ

Equations

• MazurTorsion.Kubert.OrderSevenDoublingDerivative.sourceDoubleX W = MazurTorsion.Kubert.OrderSevenDoublingDerivative.doubleXPolynomial W Polynomial.X 1

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingDerivative.sourceDoubleCompletedY (W : WeierstrassCurve ℚ) : Polynomial ℚ

Equations

• MazurTorsion.Kubert.OrderSevenDoublingDerivative.sourceDoubleCompletedY W = MazurTorsion.Kubert.OrderSevenDoublingDerivative.doubleCompletedYPolynomial W Polynomial.X 1

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingDerivative.baseVeluX (a₆ a₅ a₄ a₃ a₂ a₁ a₀ : ℚ) : Polynomial ℚ

Equations

• MazurTorsion.Kubert.OrderSevenDoublingDerivative.baseVeluX a₆ a₅ a₄ a₃ a₂ a₁ a₀ = MazurTorsion.Kubert.OrderSevenDoublingDerivative.veluXPolynomial a₆ a₅ a₄ a₃ a₂ a₁ a₀ Polynomial.X 1

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingDerivative.baseKernel (b c : ℚ) : Polynomial ℚ

Equations

• MazurTorsion.Kubert.OrderSevenDoublingDerivative.baseKernel b c = MazurTorsion.Kubert.OrderSevenDoublingDerivative.kernelPolynomial b c Polynomial.X 1

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingDerivative.baseVeluDifferential (a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c : ℚ) : Polynomial ℚ

Equations

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

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingDerivative.composedVeluX (a₆ a₅ a₄ a₃ a₂ a₁ a₀ : ℚ) (W : WeierstrassCurve ℚ) : Polynomial ℚ

Equations

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

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingDerivative.composedKernel (b c : ℚ) (W : WeierstrassCurve ℚ) : Polynomial ℚ

Equations

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

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingDerivative.composedVeluDifferential (a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c : ℚ) (W : WeierstrassCurve ℚ) : Polynomial ℚ

Equations

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

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingDerivative.targetDoubleX (W' : WeierstrassCurve ℚ) (a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c : ℚ) : Polynomial ℚ

Equations

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

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingDerivative.targetCompletedCubic (W' : WeierstrassCurve ℚ) (a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c : ℚ) : Polynomial ℚ

Equations

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

noncomputable def MazurTorsion.Kubert.OrderSevenDoublingDerivative.targetDoubleCompletedY (W' : WeierstrassCurve ℚ) (a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c : ℚ) : Polynomial ℚ

Equations

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

theorem MazurTorsion.Kubert.OrderSevenDoublingDerivative.vertical_at_point (a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c : ℚ) (W W' : WeierstrassCurve ℚ) (x : ℚ) (hX : composedVeluX a₆ a₅ a₄ a₃ a₂ a₁ a₀ W = targetDoubleX W' a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c) (hkernel : composedKernel b c W = baseKernel b c * baseVeluDifferential a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c) (hlanding : targetCompletedCubic W' a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c = sourceCompletedCubic W * baseVeluDifferential a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c ^ 2) (hK : Polynomial.eval x (baseKernel b c) ≠ 0) (hN : Polynomial.eval x (baseVeluDifferential a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c) ≠ 0) : Polynomial.eval x (composedVeluDifferential a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c W) * Polynomial.eval x (sourceDoubleCompletedY W) = Polynomial.eval x (targetDoubleCompletedY W' a₆ a₅ a₄ a₃ a₂ a₁ a₀ b c)

The vertical homogeneous certificate obtained by differentiating the abscissa, kernel, and landing polynomial certificates.