Masser–Wüstholz — stationary component of a retained equidimensional ideal

Proved

PhilipponMultiplicity.masser_wustholz_stationary_retained_ideal

by tomasz · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-groupsphilippon-multiplicityzero-estimates

Accepted proof-sketch; the terminal retained-cut induction remains Open. The Lean reduction proves stationary-prime selection using charts covering the finitely generated subgroup, dense-open extension of homogeneous vanishing, the retained-prime property, and bounded homogeneous prime avoidance. The sole Open child is refterminal retained hypersurface cut.

Let $G\subset\mathbb P^N_K$ be a connected commutative algebraic group of dimension $n>0$ over a Philippon base field. Under the original Masser–Wüstholz translation bound $a\geq1$ and closure-equation bound $b\geq1$ , set $c=a^{-n}b^{-(N-n)}$ and $X=D/c$ . Let $D,m\geq1$ , $R\geq1$ , and $\gamma_1,\ldots,\gamma_m\in G$ , and write

\Delta(S)=\{\textstyle\sum_i u_i\gamma_i:u_i\in\mathbb Z,\ 0\leq u_i\leq S\}.

Suppose a homogeneous polynomial of degree at most $D$ vanishes on $\Delta(nR)$ but not on all of $G$ . For every finitely generated subgroup $\Gamma$ containing the sampling generators, there exist $1\leq r\leq n$ , homogeneous equations $\mathcal F$ of degree at most $a^{n-1}D$ , a homogeneous ideal $J$ , and a minimal prime $\mathfrak p$ of $J$ , with the following properties.

Put $I=I(G)+(\mathcal F)$ . Then $I\subseteq J$ . Every minimal prime $\mathfrak q$ of $J$ has Hilbert dimension $\dim J=n-r$ and its group zero set meets $\Gamma$ . The ordinary scheme degree satisfies $\deg J\leq X^r$ . Every minimal prime of $I$ whose group zero set meets $\Gamma$ is also a minimal prime of $J$ . Finally,

g+(G\cap Z(\mathfrak p))\subseteq G\cap Z(J)\qquad(g\in\Delta(R)).

The formal statement is unchanged. The remaining child constructs a retained homogeneous ideal of the required dimension and degree, with bounded equations vanishing on the appropriate shrinking grid, at a stage where every permitted next equation belongs to some minimal prime. Stationary-prime selection is proved by contradiction from this terminality. Source: Masser–Wüstholz, Chapter 1 §2, printed p.414, equation (1.3): https://gdz.sub.uni-goettingen.de/id/PPN356556735_0072 .

Preamble

import Definitions.Def_PhilipponMultiplicity_GeometricSupport
import Definitions.Def_PhilipponMultiplicity_SectionFive
set_option autoImplicit false
open scoped BigOperators

Formal statement

namespace PhilipponMultiplicity

theorem masser_wustholz_stationary_retained_ideal
    (K : Type*) [NontriviallyNormedField K] (hK : IsPhilipponBaseField K)
    (E : EmbeddedCommutativeGroup K)
    (hn : 0 < (singleGroupProduct E).dimension)
    (hconnected : @_root_.IsConnected _ (singleGroupProduct E).zariskiTopology Set.univ)
    (a b : ℕ) (ha : 1 ≤ a) (hb : 1 ≤ b)
    (htranslation : MWTranslationBound (singleGroupProduct E) a)
    (hclosure : ∃ equations : Finset (singleGroupProduct E).CoordinateRing,
      (∀ P ∈ equations, (singleGroupProduct E).ambient.IsHomogeneousAtMost P (fun _ => b)) ∧
      groupProjectiveClosure (singleGroupProduct E) =
        {x | ∀ P ∈ equations, (singleGroupProduct E).ambient.eval P x = 0})
    (m D : ℕ) (hm : 1 ≤ m) (hD : 1 ≤ D)
    (γ : Fin m → (singleGroupProduct E).Point) (R : ℝ) (hR : 1 ≤ R)
    (P : (singleGroupProduct E).CoordinateRing)
    (hP : (singleGroupProduct E).ambient.IsHomogeneousAtMost P (fun _ => D)) :
    let G := singleGroupProduct E
    let c : ℝ := 1 / ((a : ℝ) ^ G.dimension * (b : ℝ) ^ (E.ambientDimension - G.dimension))
    (∀ x ∈ samplingGrid γ ((G.dimension : ℝ) * R),
      G.ambient.eval P (G.embedding x) = 0) →
    (∃ x : G.Point, G.ambient.eval P (G.embedding x) ≠ 0) →
    ∀ Γ : Submodule ℤ G.Point, Γ.FG → (∀ i, γ i ∈ Γ) →
    ∃ r : ℕ, 1 ≤ r ∧ r ≤ G.dimension ∧
      ∃ F : Finset G.CoordinateRing,
        (∀ Q ∈ F, ∃ d : G.FactorIndex → ℕ,
          G.ambient.IsHomogeneous Q d ∧
            ∀ i, (d i : ℝ) ≤ (a : ℝ) ^ (G.dimension - 1) * (D : ℝ)) ∧
        ∃ J : Ideal G.CoordinateRing, IsMultihomogeneousIdeal G.ambient J ∧
          (G.vanishingIdeal Set.univ ⊔ Ideal.span (F : Set G.CoordinateRing) ≤ J) ∧
          (∀ q ∈ J.minimalPrimes,
            SectionThree.idealDimension G.ambient q = SectionThree.idealDimension G.ambient J) ∧
          SectionThree.idealDimension G.ambient J = G.dimension - r ∧
          ((SectionThree.idealDegreeValue G.ambient J (fun _ => 1) : ℚ) : ℝ) ≤
            ((D : ℝ) / c) ^ r ∧
          (∀ q ∈ J.minimalPrimes, ∃ x ∈ Γ, x ∈ idealZeroLocusOnGroup G q) ∧
          (∀ q ∈ (G.vanishingIdeal Set.univ ⊔ Ideal.span (F : Set G.CoordinateRing)).minimalPrimes,
            (∃ x ∈ Γ, x ∈ idealZeroLocusOnGroup G q) → q ∈ J.minimalPrimes) ∧
          ∃ p ∈ J.minimalPrimes, ∀ g ∈ samplingGrid γ R,
            translate g (idealZeroLocusOnGroup G p) ⊆ idealZeroLocusOnGroup G J := by sorry

end PhilipponMultiplicity

Source

Derived retained-ideal selection input from D. W. Masser and G. Wüstholz, Fields of large transcendence degree generated by values of elliptic functions, Inventiones Mathematicae 72 (1983), Chapter 1 §2, printed pp.413–415, especially the induction (I_r), unmixedness, and equation (1.3) on p.414. https://gdz.sub.uni-goettingen.de/id/PPN356556735_0072

View graph