Projective closure — degree bound from bounded equations

Proved

PhilipponMultiplicity.connected_projective_closure_degree_bound

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

algebraic-geometryphilippon-multiplicityzero-estimates

Proved, with no Open dependencies; direct Lean proof accepted 1 October 2026.

Let $K$ be a Philippon base field and let $G\subset\mathbb P^N_K$ be a connected commutative algebraic group with its specified projective embedding. Write $n=\dim G$ for the actual Hilbert dimension in the mission's definitions. Suppose that $b\geq1$ and that the projective closure $\overline G$ is the common zero set of a finite family of homogeneous polynomials, each of degree at most $b$ . Then the ordinary projective degree satisfies

\deg(\overline G)\leq b^{N-n}.

The formal degree is the actual normalized Hilbert degree of the homogeneous vanishing ideal of the embedded group, evaluated at $1$ ; it is not an assigned numerical invariant. The equations are assumed only to define the closure set-theoretically.

The proof applies the already Proved Proposition 3.3 to the zero ideal and the finite homogeneous equations. It proves that the group vanishing ideal is a relevant minimal prime of their ideal using connectedness and the projective Nullstellensatz. Nonnegativity isolates its contribution in the reduced component sum. An explicit monomial count gives the ambient Hilbert polynomial and degree form b^N; one-factor homogeneity and cancellation give the bound b^(N-n). The equations need only define the closure set-theoretically. The formal statement is unchanged.

This closes the initial projective degree input to the Masser–Wüstholz terminal retained-cut induction. Source: Chapter 1 §2, printed pp.413–414, h=N-n and B_(h+r)=b^h D_(h+1)...D_(h+r): 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

/-- The initial projective Bezout bound; no sampling or retained-cut
conclusion is included in this geometric input. -/
theorem connected_projective_closure_degree_bound
    (K : Type*) [NontriviallyNormedField K] (hK : IsPhilipponBaseField K)
    (E : EmbeddedCommutativeGroup K)
    (hconnected : @_root_.IsConnected _ (singleGroupProduct E).zariskiTopology Set.univ)
    (b : ℕ) (hb : 1 ≤ b)
    (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}) :
    ((SectionThree.idealDegreeValue (singleGroupProduct E).ambient
      ((singleGroupProduct E).vanishingIdeal Set.univ) (fun _ => 1) : ℚ) : ℝ) ≤
        (b : ℝ) ^ (E.ambientDimension - (singleGroupProduct E).dimension) := by sorry

end PhilipponMultiplicity

Source

Classical projective Bezout bound underlying the factor b^h 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, h=N-n and B_(h+r)=b^h D_(h+1)...D_(h+r). Also related to Philippon (1986), Proposition 3.3 (reduced intersection inequality). https://gdz.sub.uni-goettingen.de/id/PPN356556735_0072

View graph