Masser–Wüstholz — terminal retained hypersurface cut

Proved

PhilipponMultiplicity.masser_wustholz_terminal_retained_cut

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

algebraic-groupsphilippon-multiplicityzero-estimates

Accepted proof-sketch; the initial projective closure degree bound remains Open. The Lean reduction proves the terminal-cut induction by retaining canonical primary components meeting the subgroup. It proves the regular hypersurface step, actual dimension drop and scheme-degree bound, survival of the original components, the shrinking-grid induction, and termination. The sole Open child is refprojective closure degree bound.

Let $G\subset\mathbb P^N_K$ be a connected commutative algebraic group of dimension $n>0$ over a Philippon base field. Assume the original Masser–Wüstholz translation-chart bound $a\geq1$ and projective-closure equation bound $b\geq1$ , and put $c=a^{-n}b^{-(N-n)}$ and $X=D/c$ . For $m,D\geq1$ , $R\geq1$ , and $\gamma_1,\ldots,\gamma_m\in G$ , 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 $G$ . For every finitely generated subgroup $\Gamma$ containing the sampling generators, there exist $1\leq r\leq n$ , a finite family $\mathcal F$ of homogeneous equations of degrees at most $a^{r-1}D$ , and a homogeneous ideal $J$ , satisfying the following properties.

Every equation in $\mathcal F$ vanishes on $\Delta((n-r+1)R)$ . With $I=I(G)+(\mathcal F)$ , we have $I\subseteq J$ . All minimal primes of $J$ have Hilbert dimension $\dim J=n-r$ , and their group zero sets meet $\Gamma$ . The ordinary scheme degree satisfies $\deg J\leq X^r$ . Every minimal prime of $I$ whose group zero set meets $\Gamma$ is a minimal prime of $J$ .

The cut is terminal in the following precise sense: for every homogeneous polynomial $Q$ of degree exactly $a^rD$ ,

Q|_{\Delta((n-r)R)}=0 \quad\Longrightarrow\quad Q\in\mathfrak p\text{ for some }\mathfrak p\in\operatorname{Min}(J).

Thus no such equation avoids all the retained minimal primes.

The formal statement is unchanged. The remaining child says that a connected embedded group whose projective closure is defined set-theoretically by equations of degrees at most b has degree at most b^(N-n). The retained-cut construction and terminality are proved in the accepted parent sketch. Source: Masser–Wüstholz, Chapter 1 §2, printed pp.413–414: 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_terminal_retained_cut
    (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 ^ (r - 1) * D) ∧
        (∀ Q ∈ F, ∀ x ∈ samplingGrid γ (((G.dimension - r + 1 : ℕ) : ℝ) * R),
          G.ambient.eval Q (G.embedding x) = 0) ∧
        ∃ 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) ∧
          ∀ Q : G.CoordinateRing, G.ambient.IsHomogeneous Q (fun _ => a ^ r * D) →
            (∀ x ∈ samplingGrid γ (((G.dimension - r : ℕ) : ℝ) * R),
              G.ambient.eval Q (G.embedding x) = 0) →
            ∃ p ∈ J.minimalPrimes, Q ∈ p := by sorry

end PhilipponMultiplicity

Source

Derived terminal-cut formulation of the retained-ideal induction in 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–414, particularly the choice of r with (I_r) true and (I_{r+1}) false preceding (1.3). https://gdz.sub.uni-goettingen.de/id/PPN356556735_0072

View graph