Denominator-free Tate normalization at an order-seven point

The pointwise Tate-normalization formula is naturally a tower of rational expressions. This file exposes compact cleared coordinates for the final Tate parameter and for the level-seven Hauptmodul. Polynomial-certificate consumers can therefore avoid expanding the normalization or carrying a spurious nonvanishing assumption for the fully cleared denominator.

def MazurTorsion.Kubert.pointTateLambdaNumerator (W : WeierstrassCurve ℚ) (x y : ℚ) : ℚ

The numerator of the tangent slope used in pointwise Tate normalization.

Equations

• MazurTorsion.Kubert.pointTateLambdaNumerator W x y = W.a₄ + 2 * x * W.a₂ - y * W.a₁ + 3 * x ^ 2

def MazurTorsion.Kubert.pointTateAlphaCleared (W : WeierstrassCurve ℚ) (x y : ℚ) : ℚ

The numerator of pointTateAlpha after clearing pointTateBeta ^ 2.

Equations

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

def MazurTorsion.Kubert.pointTateGammaCleared (W : WeierstrassCurve ℚ) (x y : ℚ) : ℚ

The last linear factor in pointTateParameter, after clearing pointTateBeta ^ 3.

Equations

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

def MazurTorsion.Kubert.pointTateParameterClearedNumerator (W : WeierstrassCurve ℚ) (x y : ℚ) : ℚ

The numerator of the pointwise Tate parameter in fully cleared form.

Equations

• MazurTorsion.Kubert.pointTateParameterClearedNumerator W x y = -MazurTorsion.Kubert.pointTateAlphaCleared W x y ^ 3

def MazurTorsion.Kubert.pointTateParameterClearedDenominator (W : WeierstrassCurve ℚ) (x y : ℚ) : ℚ

The denominator of the pointwise Tate parameter in fully cleared form.

Equations

• MazurTorsion.Kubert.pointTateParameterClearedDenominator W x y = MazurTorsion.Kubert.pointTateGammaCleared W x y * MazurTorsion.Kubert.pointTateBeta W x y ^ 4

theorem MazurTorsion.Kubert.pointTateParameter_eq_cleared (W : WeierstrassCurve ℚ) {x y : ℚ} (hbeta : pointTateBeta W x y ≠ 0) : pointTateParameter W x y = pointTateParameterClearedNumerator W x y / pointTateParameterClearedDenominator W x y

The pointwise Tate parameter as a quotient of polynomial expressions.

No nonvanishing hypothesis on the cleared denominator is needed: Lean's division is total, and both sides are zero when the last normalization factor vanishes.

theorem MazurTorsion.Kubert.pointTateBeta_ne_zero_of_hauptmodul_ne_zero (W : WeierstrassCurve ℚ) {x y : ℚ} (hB : orderSevenHauptmodulAt W x y ≠ 0) : pointTateBeta W x y ≠ 0

A nonzero pointwise level-seven Hauptmodul forces the vertical tangent denominator used by Tate normalization to be nonzero.

def MazurTorsion.Kubert.orderSevenParameterCubic (A B : ℚ) : ℚ

Homogenization of the cubic denominator in the level-seven Hauptmodul.

Equations

• MazurTorsion.Kubert.orderSevenParameterCubic A B = A ^ 3 - 8 * A ^ 2 * B + 5 * A * B ^ 2 + B ^ 3

def MazurTorsion.Kubert.orderSevenParameterHauptmodulNumerator (A B : ℚ) : ℚ

Homogenization of the numerator in the level-seven Hauptmodul.

Equations

• MazurTorsion.Kubert.orderSevenParameterHauptmodulNumerator A B = 49 * A * (A - B) * B

theorem MazurTorsion.Kubert.orderSevenHauptmodulAt_eq_cleared (W : WeierstrassCurve ℚ) {x y : ℚ} (hbeta : pointTateBeta W x y ≠ 0) : orderSevenHauptmodulAt W x y = orderSevenParameterHauptmodulNumerator (pointTateParameterClearedNumerator W x y) (pointTateParameterClearedDenominator W x y) / orderSevenParameterCubic (pointTateParameterClearedNumerator W x y) (pointTateParameterClearedDenominator W x y)

The pointwise level-seven Hauptmodul as a quotient of its fully polynomial numerator and denominator.