Upper bound theorem for geometric simplicial spheres (Stanley 1975)

upper_bound_simplicial_spheres — a formalization challenge from the lean-eval benchmark.

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.

Formal statement

/-- **Upper bound theorem for simplicial spheres** (Stanley 1975).
Every `k`-face count of a finite simplicial `(d − 1)`-sphere with `n`
vertices is bounded above by the corresponding face count of the
cyclic polytope `C(n, d)`. -/
theorem upper_bound_theorem_simplicial_spheres
    {d n k : ℕ} (X : FiniteSimplicialSphere d)
    (_hn : faceCount X 0 = n) (_hk : k < d) :
    faceCount X k ≤ cyclicPolytopeFaceCount n d k := by
  sorry

Informal solution sketch

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.

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).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: upper_bound_theorem_simplicial_spheres
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.