Coefficient-divisibility identities for short Tate equations

This file records internal substitution identities for a short Weierstrass polynomial F(X, Y) = Y^2 - X^3 - a₄ X - a₆. A bundled witness records chosen powers of an element dividing a₄ and a₆.

The first three identities remove two factors from the total transform when a₄ = ϖ A₁ and a₆ = ϖ² B₂. The remaining identities are the four weighted substitutions used later in the tame Tate case split. They remain private until such a case has a checked consumer. These are only polynomial identities: no universal property, regularity statement, or strict-transform claim is made here. The public result is the coordinate-divisibility consequence currently needed as the next route handoff.

theorem MazurTorsion.EllipticCurve.y_mem_maximalIdeal_sq_of_short_equation_of_coefficient_divisibility {R : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (W : WeierstrassCurve R) [W.IsShortNF] {x y : R} (heq : W.toAffine.Equation x y) (hx : x ∈ IsLocalRing.maximalIdeal R) (hy : y ∈ IsLocalRing.maximalIdeal R) (ha₄ : W.a₄ ∈ IsLocalRing.maximalIdeal R ^ 2) (ha₆ : W.a₆ ∈ IsLocalRing.maximalIdeal R ^ 3) : y ∈ IsLocalRing.maximalIdeal R ^ 2

Coordinate-divisibility handoff. On a short equation over a DVR, suppose an integral point specializes to the cusp. If a₄ ∈ 𝔪² and a₆ ∈ 𝔪³, then its Y-coordinate lies in 𝔪².

After writing X = ϖ X₁ and Y = ϖ Y₁, the two-factor identity reduces modulo ϖ to Y₁² = 0. The residue field is a domain, hence Y₁ also vanishes modulo ϖ.