Why a complete face-vector characterization matters

A convex polytope has finitely many faces in each dimension, and their numbers form its f-vector. Determining which integer vectors occur is a basic realization problem in discrete geometry: necessary identities such as Euler's relation do not by themselves decide whether a proposed vector comes from a polytope. For simplicial polytopes, whose facets are simplices, the g-theorem gives a complete answer. In the matrix formulation recorded in Chapter 10 of Branko Grünbaum's Convex Polytopes, realizable extended f-vectors are exactly the products of M-sequences with an explicit binomial matrix.

This is a known theorem, not an open conjecture. The mission asks for a machine-checked proof of the reviewed Lean statement while preserving the theorem's full biconditional. It is not merely a collection of upper or lower bounds on individual coordinates: one side asserts geometric realizability of the whole vector, and the other gives a simultaneous arithmetic characterization.

Geometric and arithmetic setting

A d-polytope is represented as a nonempty finite convex hull in the real coordinate space Fin d → ℝ whose affine span is the whole space. A nonempty exposed face has dimension equal to the real dimension of the direction space of its affine span. The function faceCount P j counts the nonempty exposed j-dimensional faces of P.

A simplicial d-polytope is a d-polytope for which every facet is the convex hull of d affinely independent points. The extended f-vector is indexed by Fin (d+1): its coordinate f 0 is fixed to one for the empty face, while f j.succ is the integer embedding of faceCount P j for each j : Fin d.

An M-sequence in the formalization is a natural-valued function g used only from index zero through m. It begins with g 0 = 1. Each positive entry through m is either zero, with empty boundary, or is represented by a strictly increasing binomial expansion whose upper boundary is at most the preceding entry. This is the finite Macaulay condition used on printed pages 198a–198b.

The integer-valued matrix gTheoremMatrix d j k is Björner's matrix $M_d$. Its entries are

$$(M_d)_{j,k}={d+1-j\choose d+1-k}-{j\choose d+1-k},$$

with rows $0\le j\le\lfloor d/2\rfloor$ and columns $0\le k\le d$. Subtraction is performed in the integers, not truncated natural-number arithmetic.

Formalization target

For every natural dimension d and every integer vector f : Fin (d+1) → ℤ, the main item states the equivalence

$$f\text{ is the extended f-vector of a simplicial }d\text{-polytope} \quad\Longleftrightarrow\quad \exists g\text{ an M-sequence},\ f=gM_d.$$

The left side includes both f 0 = 1 and a single simplicial polytope realizing every remaining coordinate. The right side uses one M-sequence and checks the matrix equation at every column. Its sum ranges over exactly Finset.range (d / 2 + 1), so the row indices are zero through the floor of half the dimension. Values of g outside that finite range are irrelevant on both sides of the arithmetic condition.

Significance

The theorem converts a geometric existence question into an exact finite arithmetic criterion. It characterizes the entire vector at once, retaining the correlations between face numbers that coordinatewise extremal theorems cannot express. The biconditional also has two substantive directions: every simplicial polytope produces an M-sequence, and every permitted M-sequence is realized by a simplicial polytope.

Formalizing this statement supplies reusable interfaces for full-dimensional polytopes, exposed-face counts, simpliciality, finite M-sequences, and the g-theorem matrix. The theorem body remains open in the proposal. The established mathematical result is being posed as a Lean proof task rather than claimed as already machine-checked.

Difficulty

Neither direction follows from Euler or Dehn–Sommerville linear identities alone. Those equations describe an affine subspace but do not impose the nonlinear integrality and growth conditions encoded by an M-sequence. Conversely, verifying the Macaulay inequalities for a candidate sequence does not directly construct a polytope realizing all coordinates. Proving separate inequalities for each face number would also be insufficient, because the target requires one polytope and one sequence to witness simultaneous equality of the complete vectors.

Formalization scope

All ambient geometry is finite-dimensional and real. Faces use Mathlib's exposed-face convention, and faceCount excludes the empty face before assigning a natural dimension; the leading coordinate f 0 = 1 restores the empty face in the extended vector. The polytope witness is full-dimensional in Fin d → ℝ. The matrix and the target vector are integer-valued, while the M-sequence itself is natural-valued.

The mission retains all dimensions, including the low-dimensional boundary cases. Natural subtractions inside binomial indices use Lean's truncated subtraction exactly as in the reviewed source adapter, while subtraction between the two binomial coefficients occurs in ℤ. The M-sequence witness is constrained only over the finite range used by the matrix product; no unintended condition is imposed on its unused tail.

The definitions of IsDPolytope and faceCount are reused from exact private platform declarations. The simplicial predicate is reused byte-for-byte from the preceding staged package, and the M-sequence and matrix declarations preserve their reviewed local definitions with only platform-compatible module imports. Contributions should prove the iff without weakening it to one direction, replacing realizability with coordinatewise inequalities, restricting the dimension, changing the index ranges, or allowing different witnesses for different coordinates.

Selected references

• Branko Grünbaum, Convex Polytopes, 2nd ed., Graduate Texts in Mathematics 221, Springer, 2003, §10.6, printed pp. 198a–198b / PDF pp. 235–236. DOI: 10.1007/978-1-4613-0019-9.