Masser–Wüstholz — pointed prime with bounded translation orbit

Proved

PhilipponMultiplicity.masser_wustholz_pointed_prime_orbit

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

algebraic-groupsphilippon-multiplicityzero-estimates

Accepted proof-sketch; one unpointed prime-selection input remains Open. The Lean reduction translates the selected prime through a subgroup point to the identity, pulls back its equations with the exact degree bound, preserves the sampled orbit cardinal, and transfers the component-dimension bound for every component meeting the subgroup. The sole Open child is refunpointed prime selection before recentering.

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$ . Suppose $a,b\geq1$ are integers satisfying the Masser–Wüstholz hypotheses: translations on each finitely generated subgroup have homogeneous polynomial charts of degree at most $a$ covering that subgroup, and the projective closure of $G$ has defining equations of degree at most $b$ . Set

c=a^{-n}b^{-(N-n)},\qquad X=D/c.

Fix $m,D\geq1$ , points $\gamma_1,\ldots,\gamma_m\in G$ , and a real radius $R\geq1$ . Write

\Delta(S)=\left\{\sum_i u_i\gamma_i:u\in\mathbb Z^m,\ 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 $\gamma_i$ , there exist an integer $1\leq r\leq n$ , a homogeneous prime ideal $\mathfrak p\supset I(G)$ , and finitely many homogeneous equations $\mathcal Q\subset\mathfrak p$ , each of degree at most $a^nD$ , such that the group zero set $W=G\cap Z(\mathfrak p)$ satisfies

0\in W,\qquad \#\{g+W:g\in\Delta(R)\}\leq X^r.

Moreover, every minimal prime $\mathfrak q$ of $I(G)+(\mathcal Q)$ whose group zero set meets $\Gamma$ satisfies

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

The formal statement is unchanged. The remaining child selects a homogeneous prime whose group zero set meets the finitely generated subgroup, with the sampled orbit bound and original equations of degree at most a^(n-1)D satisfying the local dimension estimate. The child does not require the prime to pass through the identity. Source: Masser–Wüstholz, Chapter 1, §2, printed pp.414–415: 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_pointed_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 ∧
        (0 : G.Point) ∈ 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 * (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 pointed 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 (1.5) p.415. The globalization is in §3, pp.416–417. https://gdz.sub.uni-goettingen.de/id/PPN356556735_0072

View graph