Upper bound theorem for geometric simplicial spheres (Stanley 1975)

upper_bound_simplicial_spheres

Submitter: Kim Morrison.

Notes: Among finite (d − 1)-dimensional simplicial spheres with n vertices, the cyclic polytope C(n, d) maximises every face number f_k. The Lean encoding `FiniteSimplicialSphere d` uses mathlib's `Geometry.SimplicialComplex ℝ (EuclideanSpace ℝ (Fin d))` — finite geometric complexes linearly embedded in ℝᵈ whose underlying space `K.space` is homeomorphic to the unit sphere in ℝᵈ. Stanley 1975 proves the bound for all finite *abstract* simplicial spheres; not every abstract finite simplicial sphere embeds linearly in ℝᵈ, so our geometric class is a subset and Stanley 1975 implies this Lean statement. The h-vector is the standard binomial transform of the f-vector with the convention f_{−1} = 1; the cyclic-polytope h-vector and face counts use the closed-form `choose (n − d − 1 + min(j, d − j)) (min(j, d − j))` and the inverse h-to-f transform. §142 of Knill's *Some Fundamental Theorems in Mathematics*.

Source: R.P. Stanley, 'The upper bound conjecture and Cohen–Macaulay rings', Studies in Appl. Math. 54 (1975) 135–142. Conjecture: T.S. Motzkin (1957); polytope case: P. McMullen, 'The maximum numbers of faces of a convex polytope', Mathematika 17 (1970) 179–184. §142 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Stanley's proof passes through the **Stanley–Reisner ring** (face ring) of a simplicial sphere. (1) Associate to a simplicial complex Δ the squarefree-monomial quotient `R[Δ] = k[x_v : v ∈ Δ⁰] / I_Δ`, where I_Δ is the ideal generated by squarefree monomials supported on non-faces of Δ. (2) Reisner's criterion: Δ is Cohen–Macaulay iff certain reduced simplicial homologies of vertex-link subcomplexes vanish; simplicial spheres satisfy this. (3) For a (d − 1)-sphere with n vertices, k[Δ] is a Cohen–Macaulay module of Krull dimension d over a polynomial ring k[θ_1, …, θ_d]; passing to the artinian quotient `A_Δ = k[Δ] / (θ_1, …, θ_d)` makes the h-vector exactly `dim_k (A_Δ)_j`. (4) Macaulay's theorem bounds the Hilbert function of any standard graded Artinian algebra generated by `n − d` degree-one elements; for C(n, d) the h-vector saturates this bound, and together with the f-from-h identity (and Dehn–Sommerville symmetry for spheres) this gives the upper bound on f_k. Mathlib has `AbstractSimplicialComplex`, `Geometry.SimplicialComplex`, faces/facets/vertices/space, but no Stanley–Reisner ring, no Cohen–Macaulay property, no Reisner criterion, no cyclic polytopes, no h-vectors, and no upper bound theorem.

theorem declaration uses `sorry`upper_bound_theorem_simplicial_spheres {d n k : ℕ} (X : LeanEval.Combinatorics.UpperBoundSimplicialSpheresProblem.FiniteSimplicialSphere d)
    (_hn : LeanEval.Combinatorics.UpperBoundSimplicialSpheresProblem.faceCount X 0 = n) (_hk : k < d) :
    LeanEval.Combinatorics.UpperBoundSimplicialSpheresProblem.faceCount X k ≤ LeanEval.Combinatorics.UpperBoundSimplicialSpheresProblem.cyclicPolytopeFaceCount n d k := byd:ℕn:ℕk:ℕX:FiniteSimplicialSphere d_hn:faceCount X 0 = n_hk:k < d⊢ faceCount X k ≤ cyclicPolytopeFaceCount n d k
  sorryAll goals completed! 🐙

Solved by

Not yet solved.