The terminal weighted-depth branch of the marked short equation

This file continues the pointwise calculation on the selected short marked model. From x ∈ 𝔪², a₄ ∈ 𝔪³, and a₆ ∈ 𝔪⁵, the equation first forces y ∈ 𝔪³. If a₄ has exact depth three, the marked double has canonical nonsingular reduction. Excluding that branch forces the weighted depths a₄ ∈ 𝔪⁴ and a₆ ∈ 𝔪⁶, to which the checked pure-scaling minimality obstruction applies.

Only the selected equation, its marked point, and minimality are used. No Kodaira symbol, regular model, component group, or component-cardinality claim is made.

theorem MazurTorsion.EllipticCurve.markedExceptionalCubic_y_mem_cube_of_coefficient_depths {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] [CharZero K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : WeierstrassCurve.Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} {P : W.Point} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [W₀.IsShortNF] (D : MarkedExceptionalCubicData W₀ W P) (hxsq : D.x ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 2) (ha₄cube : W₀.a₄ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 3) (ha₆five : W₀.a₆ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 5) : D.y ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 3

On the selected marked short equation, the weighted coefficient depths x ∈ 𝔪², a₄ ∈ 𝔪³, and a₆ ∈ 𝔪⁵ force the marked ordinate into 𝔪³.

theorem MazurTorsion.EllipticCurve.markedExceptionalCubic_a₆_mem_sixth_of_coefficient_depths {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] [CharZero K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : WeierstrassCurve.Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} {P : W.Point} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [W₀.IsShortNF] (D : MarkedExceptionalCubicData W₀ W P) (hxsq : D.x ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 2) (ha₄four : W₀.a₄ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 4) (ha₆five : W₀.a₆ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 5) : W₀.a₆ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 6

Once a₄ reaches weighted depth four on the same marked short equation, the equation upgrades a₆ ∈ 𝔪⁵ to a₆ ∈ 𝔪⁶.

theorem MazurTorsion.EllipticCurve.two_nsmul_mem_nonsingularReductionSubgroup_of_marked_a₄_not_fourth {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] [CharZero K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : WeierstrassCurve.Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} {P : W.Point} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] [W₀.IsShortNF] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hspecial : W₀.map (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) = cuspidalShortCurve (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))) (D : MarkedExceptionalCubicData W₀ W P) (hxsq : D.x ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 2) (ha₄cube : W₀.a₄ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 3) (ha₄notfour : W₀.a₄ ∉ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 4) (ha₆five : W₀.a₆ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 5) : 2 • P ∈ WeierstrassCurve.Affine.nonsingularReductionSubgroup hW ⋯

If a₄ has exact depth three after the marked equation has reached x ∈ 𝔪² and a₆ ∈ 𝔪⁵, the double of the marked point has canonical nonsingular reduction.

theorem MazurTorsion.EllipticCurve.twelve_nsmul_mem_nonsingularReductionSubgroup_of_marked_a₄_not_fourth {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] [CharZero K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : WeierstrassCurve.Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} {P : W.Point} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] [W₀.IsShortNF] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hspecial : W₀.map (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) = cuspidalShortCurve (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))) (D : MarkedExceptionalCubicData W₀ W P) (hxsq : D.x ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 2) (ha₄cube : W₀.a₄ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 3) (ha₄notfour : W₀.a₄ ∉ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 4) (ha₆five : W₀.a₆ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 5) : 12 • P ∈ WeierstrassCurve.Affine.nonsingularReductionSubgroup hW ⋯

The exact-depth-three a₄ branch supplies the exponent twelve required by the arithmetic specializations.

theorem MazurTorsion.EllipticCurve.not_isMinimal_of_short_model_weighted_coefficient_depths {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] [CharZero K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : WeierstrassCurve (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [W.IsElliptic] [W₀.IsShortNF] (ϖ : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (hϖ : Irreducible ϖ) (ha₄four : W₀.a₄ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 4) (ha₆six : W₀.a₆ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 6) : ¬WeierstrassCurve.IsMinimal (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) W

A short integral model with weighted depths a₄ ∈ 𝔪⁴ and a₆ ∈ 𝔪⁶ cannot have minimal generic fibre. Scaling by the displayed uniformizer would keep every coefficient integral while increasing the discriminant valuation.