The marked triple in the next tame Tate branch

Let an integral short Weierstrass equation have standard cuspidal special fibre, with a₄ ∈ 𝔪² and a₆ ∈ 𝔪² \ 𝔪³. This file proves the pointwise consequence needed by the tame torsion argument: the triple of every local 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_a₄_sq_a₆_sq_not_cube {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)} (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))) (ha₄sq : W₀.a₄ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 2) (_ha₆sq : W₀.a₆ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 2) (ha₆notcube : W₀.a₆ ∉ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 3) (P : W.Point) : 3 • P ∈ WeierstrassCurve.Affine.nonsingularReductionSubgroup hW ⋯

In the exact depth-two a₆ branch, the triple of every local point belongs to canonical nonsingular reduction.

theorem MazurTorsion.EllipticCurve.twelve_nsmul_mem_nonsingularReductionSubgroup_of_a₄_sq_a₆_sq_not_cube {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)} (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))) (ha₄sq : W₀.a₄ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 2) (ha₆sq : W₀.a₆ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 2) (ha₆notcube : W₀.a₆ ∉ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 3) (P : W.Point) : 12 • P ∈ WeierstrassCurve.Affine.nonsingularReductionSubgroup hW ⋯

The exact depth-two a₆ branch supplies the exponent twelve used by the arithmetic specializations: it is four times the checked triple.