The marked repeated-root branch of the exceptional star cubic

For a marked root r of T^3 + A T + B, vanishing of the derivative gives A = -3r^2 and B = 2r^3 in the residue field. This file develops the next pointwise branch on the same selected short equation. A nonzero repeated marked root forces the twelfth multiple of the marked point into canonical nonsingular reduction. The arithmetic consumers therefore force the marked root to vanish, which increases the displayed coefficient and abscissa depths without changing the model or the chosen uniformizer.

Only affine group-law and valuation consequences for the marked point are asserted. No Kodaira symbol, regular model, component incidence, or global component-group bound is constructed.

theorem MazurTorsion.EllipticCurve.markedExceptionalCubic_coefficients_of_derivative_eq_zero {O : Type u} {F : Type v} [CommRing O] [IsLocalRing O] [Field F] [Algebra O F] {W₀ : WeierstrassCurve O} {W : WeierstrassCurve.Affine F} {P : W.Point} (D : MarkedExceptionalCubicData W₀ W P) (hrepeated : D.derivativeResidue = 0) : (IsLocalRing.residue O) D.A = -3 * (IsLocalRing.residue O) D.X ^ 2 ∧ (IsLocalRing.residue O) D.B = 2 * (IsLocalRing.residue O) D.X ^ 3

At a repeated marked exceptional-cubic root, the two coefficient residues are determined by that root.

theorem MazurTorsion.EllipticCurve.markedExceptionalCubic_deeper_depths_of_derivative_eq_zero_of_root_eq_zero {O : Type u} {F : Type v} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O] [Field F] [Algebra O F] {W₀ : WeierstrassCurve O} {W : WeierstrassCurve.Affine F} {P : W.Point} (D : MarkedExceptionalCubicData W₀ W P) (hrepeated : D.derivativeResidue = 0) (hroot : (IsLocalRing.residue O) D.X = 0) : (IsLocalRing.residue O) D.A = 0 ∧ (IsLocalRing.residue O) D.B = 0 ∧ D.x ∈ IsLocalRing.maximalIdeal O ^ 2 ∧ W₀.a₄ ∈ IsLocalRing.maximalIdeal O ^ 3 ∧ W₀.a₆ ∈ IsLocalRing.maximalIdeal O ^ 4

If the repeated marked root is zero, its abscissa and both displayed coefficients gain one power of the same bundled uniformizer.

theorem MazurTorsion.EllipticCurve.twelve_nsmul_mem_nonsingularReductionSubgroup_of_repeatedExceptionalRoot_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)} {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) (hrepeated : D.derivativeResidue = 0) (hroot_ne : (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) D.X ≠ 0) : 12 • P ∈ WeierstrassCurve.Affine.nonsingularReductionSubgroup hW ⋯

A nonzero repeated marked root forces the twelfth multiple of the marked point into canonical nonsingular reduction. If the tangent slope is nonintegral or a unit, the double is already in canonical reduction. Otherwise the double remains at the cusp with marked root -2r, which is simple because its derivative is 3²r².