The marked double in the next tame Tate branch

Let an integral short Weierstrass equation over the valuation ring of an adic completion have standard cuspidal special fibre. After the first coefficient split, suppose the quotient of a₄ by a uniformizer has nonzero residue. This file proves the precise pointwise consequence needed downstream: the double of every local point has canonical nonsingular reduction.

For a point specializing to the cusp, the tangent numerator has valuation exactly one. If the ordinate has valuation at least two, the tangent slope has a pole and the double belongs to the formal kernel. Otherwise the slope is an integral unit, and the double reduces to (lambda^2, -lambda^3) on Y² = X³, away from its singular origin. No Kodaira symbol, strict-transform assertion, regular model, or component-cardinality statement is made.

theorem MazurTorsion.EllipticCurve.two_nsmul_mem_nonsingularReductionSubgroup_of_firstBlowup_residue_b₄_ne_zero {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] (B : FirstBlowupEquationCharts W₀) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hspecial : W₀.map (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) = cuspidalShortCurve (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))) (hb₄ : (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) B.coefficients.b₄ ≠ 0) (P : W.Point) : 2 • P ∈ WeierstrassCurve.Affine.nonsingularReductionSubgroup hW ⋯

In the a₄/ϖ-nonzero branch of a normalized tame equation, the double of every local point belongs to the canonical nonsingular-reduction subgroup.

theorem MazurTorsion.EllipticCurve.twelve_nsmul_mem_nonsingularReductionSubgroup_of_firstBlowup_residue_b₄_ne_zero {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] (B : FirstBlowupEquationCharts W₀) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hspecial : W₀.map (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) = cuspidalShortCurve (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))) (hb₄ : (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) B.coefficients.b₄ ≠ 0) (P : W.Point) : 12 • P ∈ WeierstrassCurve.Affine.nonsingularReductionSubgroup hW ⋯

The same branch supplies the uniform exponent twelve used by the arithmetic specialization consumers: it is six times the checked double.