Masser–Wüstholz — unpointed prime selection before recentering

Proved

PhilipponMultiplicity.masser_wustholz_unpointed_prime_orbit

by tomasz · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-groupsphilippon-multiplicityzero-estimates

Accepted proof-sketch; one retained-ideal selection input remains Open. The Lean reduction proves that the selected prime’s sampled translates are whole minimal-prime components of an equidimensional retained ideal. It bounds the number of these components by the actual ordinary degree, using positive integral prime degrees and positive finite generic local lengths in the degree associativity formula. The sole Open child is refstationary retained-ideal selection.

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

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

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$ , a homogeneous prime $\mathfrak p\supset I(G)$ , and a finite family of homogeneous equations $\mathcal F\subset\mathfrak p$ of degree at most $a^{n-1}D$ , such that $V=G\cap Z(\mathfrak p)$ meets $\Gamma$ and

\#\{g+V:g\in\Delta(R)\}\leq X^r.

Every minimal prime $\mathfrak q$ of $I(G)+(\mathcal F)$ whose group zero set meets $\Gamma$ satisfies

\dim(G\cap Z(\mathfrak q))\leq n-r.

The formal statement is unchanged. The remaining child constructs the retained homogeneous ideal with its equidimensionality, numerical degree bound, preservation of components meeting the finitely generated subgroup, and stationary prime. Source: Masser–Wüstholz, Chapter 1 §2, printed p.414, especially (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_unpointed_prime_orbit
    (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 ∧
      ∃ p : Ideal G.CoordinateRing, p.IsPrime ∧ IsMultihomogeneousIdeal G.ambient p ∧
        G.vanishingIdeal Set.univ ≤ p ∧
        (∃ x ∈ Γ, x ∈ idealZeroLocusOnGroup G p) ∧
        ((((fun g => translate g (idealZeroLocusOnGroup G p)) '' samplingGrid γ R).ncard : ℝ) ≤
          ((D : ℝ) / c) ^ r) ∧
        ∃ Q : Finset G.CoordinateRing,
          (∀ F ∈ Q, ∃ d : G.FactorIndex → ℕ,
            G.ambient.IsHomogeneous F d ∧
              ∀ i, (d i : ℝ) ≤ (a : ℝ) ^ (G.dimension - 1) * (D : ℝ)) ∧
          (∀ F ∈ Q, F ∈ p) ∧
          ∀ q ∈ (G.vanishingIdeal Set.univ ⊔ Ideal.span (Q : Set G.CoordinateRing)).minimalPrimes,
            (∃ x ∈ Γ, x ∈ idealZeroLocusOnGroup G q) →
            varietyDimension G (idealZeroLocusOnGroup G q) ≤ G.dimension - r := by sorry

end PhilipponMultiplicity

Source

Derived unpointed prime selection 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 (1.3) p.414 and the retained-prime observation before (1.5) p.415. The globalization is in §3, pp.416–417. https://gdz.sub.uni-goettingen.de/id/PPN356556735_0072

View graph