Masser–Wüstholz — local prime estimate over finitely generated subgroups

Proved

PhilipponMultiplicity.masser_wustholz_local_prime_estimate

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

algebraic-groupsphilippon-multiplicityzero-estimates

Accepted proof-sketch; one pointed-prime selection input remains Open. The Lean reduction constructs bounded integer relations from equal sampled translates, proves that their image generates a subgroup contained in the selected pointed zero set, and establishes an exact equality of sampled coset and translation-orbit counts. The sole Open child is the refpointed prime with bounded translation orbit.

Let $K$ be a Philippon base field, and let $G\subset\mathbb P^N_K$ be a connected commutative algebraic group of positive dimension $n$ . Let $a,b\geq1$ be integers. Assume that translations on each finitely generated subgroup have homogeneous polynomial presentations of degree at most $a$ on a chart containing that subgroup, and that the projective closure of $G$ is defined by finitely many homogeneous equations of degree at most $b$ . Put

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

Fix $m,D\geq1$ , points $\gamma_1,\ldots,\gamma_m\in G$ , and $R\geq1$ . Write $\Psi(u)=\sum_i u_i\gamma_i$ and

\Delta(S)=\{\Psi(u):u\in\mathbb Z^m,\ 0\leq u_i\leq S\text{ for all }i\}.

Suppose a homogeneous polynomial of degree at most $D$ vanishes on $\Delta(nR)$ but not identically on $G$ .

For every finitely generated subgroup $\Gamma\leq G(K)$ containing the $\gamma_i$ , there exist an integer $1\leq r\leq n$ , a finite set $\Sigma\subset\mathbb Z^m$ with $|\sigma_i|\leq R$ for all $\sigma\in\Sigma$ , and finitely many homogeneous polynomials $\mathcal Q$ , each of degree at most $a^nD$ , with the following properties. If $A$ is the subgroup generated by $\Psi(\Sigma)$ , then

\#\bigl((\Delta(R)+A)/A\bigr)\leq X^r, \qquad Q|_A=0\quad(Q\in\mathcal Q).

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

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

The formal statement is unchanged. The remaining child supplies a homogeneous prime through the identity, its sampled orbit bound, and bounded equations with the local component-dimension estimate. No bounded-relation or subgroup-coset conclusion is assumed in that child. 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_local_prime_estimate
    (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 ∧
      ∃ relations : Finset (Fin m → ℤ), (∀ v ∈ relations, ∀ i, |(v i : ℝ)| ≤ R) ∧
        let A := (Submodule.span ℤ
          (integerCombination γ '' (relations : Set (Fin m → ℤ)))).toAddSubgroup
        ((((fun g => translate g (A : Set G.Point)) '' 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 : ℝ)) ∧
          (∀ x ∈ A, ∀ F ∈ Q, G.ambient.eval F (G.embedding x) = 0) ∧
          ∀ 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 local prime estimate 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