Exact depth four on the marked exceptional branch

On the marked exceptional-cubic branch, suppose the same integral point and short equation have x,y ∈ 𝔪², a₄ ∈ 𝔪³, and a₆ ∉ 𝔪⁵. The equation forces a₆ ∈ 𝔪⁴, and this file proves that the triple of that marked point has canonical nonsingular reduction.

The proof is entirely on the selected Weierstrass equation. It follows the tangent and secant formulas, separates slopes with a pole from integral-unit slopes, and handles equal-abscissa and vertical cases in the group law explicitly. It does not name a Kodaira symbol or construct a regular model, strict transform, component group, or component-cardinality bound.

theorem MazurTorsion.EllipticCurve.three_nsmul_mem_nonsingularReductionSubgroup_of_marked_a₆_not_fifth {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₆notfive : W₀.a₆ ∉ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 5) : 3 • P ∈ WeierstrassCurve.Affine.nonsingularReductionSubgroup hW ⋯

If the marked point has x,y ∈ 𝔪², a₄ ∈ 𝔪³, and a₆ ∉ 𝔪⁵, then its triple has canonical nonsingular reduction. The equation itself forces a₆ ∈ 𝔪⁴; it is not a premise.

theorem MazurTorsion.EllipticCurve.twelve_nsmul_mem_nonsingularReductionSubgroup_of_marked_a₆_not_fifth {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₆notfive : W₀.a₆ ∉ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 5) : 12 • P ∈ WeierstrassCurve.Affine.nonsingularReductionSubgroup hW ⋯

The marked branch outside 𝔪⁵ supplies the exponent twelve used by the arithmetic specializations: it is four times the checked triple.