Discriminant bounds in the last branches of Tate's algorithm

In the triple-root branch of Tate's algorithm, the successive normal forms at Steps 8, 9, and 10 force the discriminant to be divisible by the eighth, ninth, and tenth powers of the uniformiser, respectively. These are the lower bounds on the discriminant valuation used when the reduction symbols IV*, III*, and II* are assigned an algorithmic Ogg exponent.

The bounds are polynomial identities and hold over an arbitrary commutative ring. In particular, they do not need a discrete valuation ring, a perfect residue field, or minimality. The normal-form constructions under those hypotheses are in TateAlgorithm.TripleRoot.

Reference

J. H. Silverman, Advanced Topics in the Arithmetic of Elliptic Curves, IV.9, Steps 8–10 of Tate's algorithm.

theorem WeierstrassCurve.pow_eight_dvd_Δ_of_stepEight {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (ϖ : R) (h₁ : ϖ ∣ W.a₁) (h₂ : ϖ ^ 2 ∣ W.a₂) (h₃ : ϖ ^ 2 ∣ W.a₃) (h₄ : ϖ ^ 3 ∣ W.a₄) (h₆ : ϖ ^ 4 ∣ W.a₆) : ϖ ^ 8 ∣ W.Δ

In the Step 8 normal form of Tate's algorithm, the discriminant is divisible by ϖ⁸. The hypotheses on the coefficients are exactly those produced by the triple-root translation.

theorem WeierstrassCurve.pow_nine_dvd_Δ_of_stepNine {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (ϖ : R) (h₁ : ϖ ∣ W.a₁) (h₂ : ϖ ^ 2 ∣ W.a₂) (h₃ : ϖ ^ 3 ∣ W.a₃) (h₄ : ϖ ^ 3 ∣ W.a₄) (h₆ : ϖ ^ 5 ∣ W.a₆) : ϖ ^ 9 ∣ W.Δ

In the Step 9 normal form of Tate's algorithm, the discriminant is divisible by ϖ⁹. The stronger divisibility of a₃ and a₆ raises that of b₆ from ϖ⁴ to ϖ⁵.

theorem WeierstrassCurve.pow_ten_dvd_Δ_of_stepTen {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (ϖ : R) (h₁ : ϖ ∣ W.a₁) (h₂ : ϖ ^ 2 ∣ W.a₂) (h₃ : ϖ ^ 3 ∣ W.a₃) (h₄ : ϖ ^ 4 ∣ W.a₄) (h₆ : ϖ ^ 5 ∣ W.a₆) : ϖ ^ 10 ∣ W.Δ

In the Step 10 normal form of Tate's algorithm, the discriminant is divisible by ϖ¹⁰. The extra divisibility of a₄ raises the bounds on both b₄ and b₈.