Minimal-model scaling inputs for the tame Tate algorithm

Mathlib's minimal-model API states minimality as maximality of the multiplicative discriminant valuation among integral admissible changes. This file extracts the forms used at the start of a Tate-algorithm argument:

• integral j gives v(c₄)³ ≤ v(Δ); and
• integral changes whose scale factor has valuation one preserve minimality; and
• no translations followed by a scale of valuation below one can keep all five transformed coefficients integral on a minimal equation.

These are valuation and minimality inputs only. They do not construct a Néron model, determine a Kodaira symbol, identify the canonical nonsingular-reduction subgroup with the Néron identity component, or bound the order of a marked component class.

theorem MazurTorsion.EllipticCurve.valuation_c₄_pow_three_le_valuation_Δ_of_valuation_j_le_one {R : Type u_1} {K : Type u_2} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} [W.IsElliptic] (hj : (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.j ≤ 1) : (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.c₄ ^ 3 ≤ (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.Δ

Integral j is the valuation inequality v(c₄)³ ≤ v(Δ). This is the potentially-good valuation input to the tame Kodaira classification.

theorem MazurTorsion.EllipticCurve.not_valuation_Δ_lt_of_isMinimal_of_isIntegral_variableChange {R : Type u_1} {K : Type u_2} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} [WeierstrassCurve.IsMinimal R W] (C : WeierstrassCurve.VariableChange K) [hC : WeierstrassCurve.IsIntegral R (C • W)] : ¬(IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.Δ < (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) (C • W).Δ

Minimality forbids an integral admissible change whose discriminant has strictly larger multiplicative valuation. This unfolds Mathlib's MaximalFor definition and removes the bounded subtype used internally by valuation_Δ_aux.

theorem MazurTorsion.EllipticCurve.isMinimal_variableChange_of_isIntegral_of_valuation_u_eq_one {R : Type u_1} {K : Type u_2} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} [WeierstrassCurve.IsMinimal R W] (C : WeierstrassCurve.VariableChange K) (hC : WeierstrassCurve.IsIntegral R (C • W)) (hu : (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) ↑C.u = 1) : WeierstrassCurve.IsMinimal R (C • W)

An integral admissible change whose scale factor has valuation one preserves minimality. In particular, integral translations used to move a singular point to the origin stay within the chosen minimal class.

theorem MazurTorsion.EllipticCurve.not_isIntegral_variableChange_of_isMinimal_of_valuation_u_lt_one {R : Type u_1} {K : Type u_2} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} [W.IsElliptic] [WeierstrassCurve.IsMinimal R W] (C : WeierstrassCurve.VariableChange K) (hu : (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) ↑C.u < 1) : ¬WeierstrassCurve.IsIntegral R (C • W)

On a minimal elliptic equation, an admissible change whose scale factor has valuation below one cannot be integral, regardless of its translation parameters. The discriminant multiplier depends only on the scale factor, so such a change would strictly improve the multiplicative discriminant valuation.

theorem MazurTorsion.EllipticCurve.not_isIntegral_scale_of_isMinimal {R : Type u_1} {K : Type u_2} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} [W.IsElliptic] [WeierstrassCurve.IsMinimal R W] (u : Kˣ) (hu : (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) ↑u < 1) : ¬WeierstrassCurve.IsIntegral R ({ u := u, r := 0, s := 0, t := 0 } • W)

A pure change of scale by u with v(u) < 1 cannot remain integral on a minimal elliptic equation. Its discriminant is multiplied by u⁻¹², which would strictly improve the multiplicative discriminant valuation.

def MazurTorsion.EllipticCurve.TranslatedWeightedCoefficientsIntegralAfterScale {R : Type u_1} {K : Type u_2} [CommRing R] [Field K] [Algebra R K] (W : WeierstrassCurve K) (u : Kˣ) (r s t : K) : Prop

All five coefficients have integral lifts after translating by r, s, and t, then applying the weighted scale by u⁻¹. These are exactly the five coefficient formulas for the admissible change ⟨u, r, s, t⟩.

Equations

• One or more equations did not get rendered due to their size.

theorem MazurTorsion.EllipticCurve.tateAlgorithm_minimalityTranslatedCoefficientObstruction {R : Type u_1} {K : Type u_2} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} [W.IsElliptic] [WeierstrassCurve.IsMinimal R W] (u : Kˣ) (r s t : K) (hu : (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) ↑u < 1) : ¬TranslatedWeightedCoefficientsIntegralAfterScale W u r s t

Tate translation-and-scaling input. On a minimal equation, arbitrary translations cannot make all five transformed coefficients integral after a scale factor of valuation below one. This is the simultaneous divisibility obstruction used before the blowup and Kodaira case split.

def MazurTorsion.EllipticCurve.WeightedCoefficientsIntegralAfterScale {R : Type u_1} {K : Type u_2} [CommRing R] [Field K] [Algebra R K] (W : WeierstrassCurve K) (u : Kˣ) : Prop

All five coefficients have integral lifts after the weighted pure scale by u⁻¹.

Equations

• One or more equations did not get rendered due to their size.

theorem MazurTorsion.EllipticCurve.tateAlgorithm_minimalityCoefficientObstruction {R : Type u_1} {K : Type u_2} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} [W.IsElliptic] [WeierstrassCurve.IsMinimal R W] (u : Kˣ) (hu : (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) ↑u < 1) : ¬WeightedCoefficientsIntegralAfterScale W u

Named Tate-algorithm consumer. On a minimal equation, at least one weighted coefficient fails to remain integral after scaling down by an element of positive additive valuation. This is the precise coefficient obstruction used to prevent another global scaling step in Tate's algorithm. Further translations, blowups, and component bookkeeping are still required to deduce a Kodaira symbol or a component-order bound.