Theorem 2.1 — general multiplicity estimate
ProvedPhilipponMultiplicity.theorem_2_1Proved with no Open theorem dependencies, verified 29 September 2026. Checked locally with Lean 4.33.1 and the proposal’s pinned Mathlib. An independent blind readback is attached.
For fixed embedded group factors, choose positive integral constants depending only on the individual embeddings. For a polynomial with contact at least nT+1 on the n-fold sampling sumset, obtain a connected algebraic subgroup with the stated incomplete-definition degree bound, containment in a translated zero locus, and binomial/coset/Hilbert inequality. Preserve both complex and ℓ-adic settings.
/- Open statement draft. The proof and source-comparison obligations remain open. -/ import Definitions.Def_PhilipponMultiplicity_Degree import Definitions.Def_PhilipponMultiplicity_Analytic set_option autoImplicit false open scoped BigOperators
namespace PhilipponMultiplicity
theorem theorem_2_1
(K : Type*) [NontriviallyNormedField K] (hK : IsPhilipponBaseField K) :
∃ c : EmbeddedCommutativeGroup K → ℕ,
(∀ E, 1 ≤ c E) ∧
∀ (G : EmbeddedGroupProduct K) (A : AnalyticSubgroup G)
(sample : Finset G.Point), 0 ∈ sample →
∀ (T : ℕ) (D : G.FactorIndex → ℕ) (P : G.CoordinateRing),
P ≠ 0 → IsMultihomogeneousOfDegree G P D →
(∀ g ∈ sumset sample G.dimension,
((G.dimension * T + 1 : ℕ) : WithTop ℕ) ≤ vanishingOrder A P g) →
∃ H : AlgebraicSubgroup G,
H.IsConnected ∧
HasIncompleteDefinition G H.carrier (fun i => c (G.factor i) * D i) ∧
(∃ g : G.Point, H.carrier ⊆ translate g (zeroLocusOnGroup G P)) ∧
((Nat.choose (T + analyticCodimension A H.carrier) (analyticCodimension A H.carrier) : ℝ) *
(cosetCount sample H.carrier : ℝ) * hilbertDegreeForm G H.carrier D ≤
hilbertDegreeForm G Set.univ (fun i => c (G.factor i) * D i)) := by sorry
end PhilipponMultiplicityRead-back
What the Lean code literally says, in plain math · gpt-6
Let be any nontrivially normed field for which there is an isometric field isomorphism either , or for some prime natural number , where is the field denoted by . There exists a function assigning a natural number to every embedded commutative group over , with for every such , such that the following holds simultaneously for every embedded product , every analytic datum on , every finite containing , every , every , and every nonzero multihomogeneous of degree exactly . If for every , then there is a connected algebraic subgroup of having an incomplete definition of degrees at most , such that for some , and . The translation clause means that each can be written with . The function is chosen before , and a factor receives the same assigned value wherever that identical embedded group occurs. An embedded product consists of a positive number of factors ; each factor is a locally closed subset of , with , carrying an abelian additive group structure. Its addition and negation are required to have local projective polynomial representations: at every source point and for each target block, some open neighborhood in the source projective Zariski topology and some tuple of homogeneous polynomials of a common block multidegree represent that block of the map at every source point in the neighborhood, and the evaluated tuple is nonzero there. The points of are the Cartesian product of the factor carriers, and is its coordinate polynomial ring. In each projective block a nonzero representative is chosen; denotes evaluation at these chosen representatives. A polynomial is multihomogeneous of degree when every monomial in its support has total exponent in block ; the zero polynomial has every such degree. The ambient Zariski topology is generated by the sets where a multihomogeneous polynomial is nonzero, and has the induced topology. For any , is the ideal generated by all multihomogeneous polynomials vanishing at every point of ; write for the whole group and . An algebraic subgroup means an additive subgroup closed in this topology; connectedness refers to this topology. Translation means . The data consist of a natural number , a real radius , the open ball with its asserted openness and membership , and a map such that and whenever . No injectivity is required. There are coordinate lifts , defined for every and , each analytic at ; for each coordinate admits a formal multilinear power series on the entire radius- ball and each block of is nonzero and represents for every . For every , on some neighborhood of contained in , every block of is nonzero and represents . The set is the additive subgroup generated by , with no topological closure operation. Put and . The natural number is , using natural-number subtraction, and is . The order is the least for which the -fold Fréchet derivative of at is nonzero, or if all these derivatives vanish; the derivative of order zero is the value at . Derivatives use the total Fréchet derivative, which is zero where differentiability fails. All order comparisons take place in . For any ideal and block degree , let be the -dimension of the image of the vector space of multihomogeneous polynomials of degree in . Let be a polynomial agreeing with at every natural vector above some coordinatewise natural threshold, if such a polynomial exists; if none exists, set . The polynomial, when it exists, is unique. Set , with total degree of the zero polynomial defined as , and , where brackets select the total homogeneous part of that degree. This is a rational value, viewed as a real number in the group inequalities. Write and . The number assigned to a factor is the total degree of the corresponding polynomial for its vanishing ideal in its one-block homogeneous coordinate ring, and . None of these definitions supplies a separate existence hypothesis for ; the zero fallback makes both and equal to zero in that case. Evaluation permits zero coordinates of , with . Saying that has an incomplete definition of degrees at most means that there is an ideal closed under every block-homogeneous component projection, and a finite set whose members are each homogeneous of some degree coordinatewise, such that , , and every minimal prime of whose equations vanish at some point of is a minimal prime of . The finite equation set may be empty and may contain zero; components not meeting impose no condition, and additional minimal primes of are not excluded. For a finite set , is the set of sums of exactly members of , allowing repetitions, so . The number counts distinct subsets for , not elements of a multiset. The quantifiers include , zero entries of , factors with , and ; they exclude an empty factor list and, because , an empty sample. If , the vanishing hypothesis is imposed only at and has threshold . If or , the binomial factor is . A nonzero polynomial in is allowed to vanish on every point of unless a separate nonvanishing-on- clause is stated.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.