Masser–Wüstholz — geometric grid-coset estimate with bounded equations

Proved

PhilipponMultiplicity.masser_wustholz_geometric_coset_bound

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

algebraic-groupsphilippon-multiplicityzero-estimates

Accepted proof-sketch; one local geometric input remains Open. The Lean reduction proves finite-choice and Noetherian globalization, the global component-dimension bound, passage to an algebraic subgroup by Zariski closure, and preservation of the coset count and original equation-degree bound. Its sole Open child is the reflocal prime estimate over finitely generated subgroups.

Let $G$ be a connected positive-dimensional commutative algebraic group embedded in one projective space, with the translation bound $a$ and closure-equation bound $b$ of Masser–Wüstholz. Write

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

Let $m,D\geq1$ , let $\gamma_1,\ldots,\gamma_m\in G$ , and let $R\geq1$ . Suppose a homogeneous polynomial of degree at most $D$ vanishes on the nonnegative sampling grid of radius $nR$ , but does not vanish identically on $G$ .

Then there are an integer $1\leq r\leq n$ , an algebraic subgroup $H$ of dimension at most $n-r$ , and a relatively closed algebraic subset $V$ of $G$ such that

\#\bigl((\Gamma(R)+H)/H\bigr)\leq X^r, \qquad H\subseteq V,\qquad \dim V\leq n-r.

The set $V$ is cut out in $G$ by finitely many actual homogeneous equations, each of degree at most $a^nD$ .

The formal statement is unchanged. The remaining child retains all bounded differences stabilizing the selected local prime and leaves the prime-selection, localized component-dimension, and component-degree estimates explicit. The global subgroup and containing variety are constructed in the accepted reduction. Source: Masser–Wüstholz, Chapter 1, §§2–3, printed pp.413–417: https://gdz.sub.uni-goettingen.de/id/PPN356556735_0072 .

Preamble

import Definitions.Def_PhilipponMultiplicity_GeometricSupport
set_option autoImplicit false
open scoped BigOperators

Formal statement

namespace PhilipponMultiplicity

theorem masser_wustholz_geometric_coset_bound
    (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) →
    ∃ r : ℕ, 1 ≤ r ∧ r ≤ G.dimension ∧
      ∃ H : AlgebraicSubgroup G, varietyDimension G H.carrier ≤ G.dimension - r ∧
        ((((fun g => translate g H.carrier) '' samplingGrid γ R).ncard : ℝ) ≤
          ((D : ℝ) / c) ^ r) ∧
        ∃ V : GroupSubvariety G, H.carrier ⊆ V.carrier ∧
          varietyDimension G V.carrier ≤ G.dimension - r ∧
          DefinedByEquations G V.carrier ((a : ℝ) ^ G.dimension * (D : ℝ)) := by sorry

end PhilipponMultiplicity

Source

Derived geometric input from Masser–Wüstholz, Fields of large transcendence degree generated by values of elliptic functions, Inventiones Mathematicae 72 (1983), Chapter 1 §§2–3, printed pp.413–417; Theorem I p.412. https://gdz.sub.uni-goettingen.de/id/PPN356556735_0072 . Philippon 1986 p.361: https://numdam.org/articles/10.24033/bsmf.2060/

View graph