Convex Polytopes

Motivation

A polytope can be given by a list of vertices, a list of inequalities, or much less explicit access. The last case arises when geometric information is available through queries to a physical or computational object but a full description is unavailable. Grünbaum's account of a result by Gritzmann, Klee, and Westwater asks how much of a polytope can be recovered when each query shoots a ray from a known interior point and reports where it meets the boundary. The target is the complete face lattice, including incidence among faces of every dimension, and the cost is the number of oracle calls. The result appears in Convex Polytopes, §3.6, printed pp. 52b–52c (PDF pp. 74–75 of the supplied source).

Setting

Fix a positive integer $d$. A $d$-polytope $P$ is a nonempty finite convex hull in real coordinate space $\mathbb R^d$ whose affine span is the whole space. The origin is known to lie in the interior of $P$. A ray query supplies a nonzero direction $v$; the oracle returns the intersection of the positive ray $\{tv:t>0\}$ with the boundary of $P$. The theorem requires this boundary-point property for every nonzero direction. It does not give the reconstruction program the vertices, inequalities, face counts, or coordinates of $P$.

A face is represented by an exposed subset of $P$, ordered by inclusion. The resulting face lattice includes the empty and whole faces. For $0\leq k<d$, $f_k(P)$ counts nonempty faces of affine dimension $k$; hence $f_0(P)$ is the vertex count and $f_{d-1}(P)$ is the facet count. The empty face has dimension $-1$ in the book's convention and is excluded from these natural-indexed counts. These conventions follow Grünbaum §§2.4 and 3.1 (printed pp. 17 and 31; PDF pp. 35 and 51).

Formalization target

The single source obligation is the unnumbered Gritzmann–Klee–Westwater theorem of Grünbaum §3.6. For each $d>0$, one finite exact-real ray-query program works for every eligible $P$ and every correct ray oracle for $P$. It halts with an encoding of the entire face lattice after at most

$$f_0(P)+(d-1)f_{d-1}(P)^2+(5d-4)f_{d-1}(P)$$

queries. The square on the facet count, both coefficients, and the continuation of “queries” across the page break are part of the printed statement. The program is selected before the unknown polytope and its oracle. The finite running time and output may depend on the instance. No common output, fixed runtime bound, or bit-complexity bound is asserted.

The Lean declaration is Grunbaum2003.ray_oracle_face_lattice_reconstruction. It asserts existence of the program, universal correctness, finite termination in a halt instruction, the displayed query inequality, and a concrete encoding of the whole face lattice. Its body is sorry: this package is a compiled statement and does not claim a machine-checked proof.

Significance

The conclusion recovers all face incidences from boundary samples on rays from one interior point. It is stronger than recovering only a vertex or facet list because the output explicitly determines the ordering of all faces. The bound measures the information requested from the oracle; the source does not constrain the number of internal arithmetic steps. A formal proof would connect the geometric reconstruction argument to a precise query machine and establish that its output matrix has exactly the claimed faces and inclusions.

Difficulty

Ray answers are geometric points, while the desired output is a global combinatorial structure. Sampling one direction per visible feature gives no direct certificate that all faces and incidences have been found. In particular, a proposed reconstruction must use only the permitted oracle answers and still know when its finite description is complete. The theorem also needs a uniform program for every polytope in a fixed dimension, with the instance dependent query count above. The present statement makes these quantifier and resource requirements explicit.

Formalization scope

The machine has a finite instruction list for rational constants, exact real arithmetic, sign branches, tape movement, oracle queries, and halt. Its tape begins at zero. A query reads a nonzero direction from the tape and writes back the oracle's boundary answer; only this instruction increments the query counter. A zero direction, invalid label, or division by zero fails instead of creating a successful execution. Thus an unrestricted oracle value at zero cannot certify the theorem. Arithmetic and sign tests are exact real operations, matching the source's query model rather than imposing a bit model.

The output is a self-delimiting Boolean inclusion matrix indexed by a finite type. A bijection connects its indices to all exposed faces of $P$, and each matrix entry is one precisely when the associated faces are ordered by inclusion. This rules out an output consisting merely of face counts, vertices, or facets. IsDPolytope, faceCount, PolytopeFace, the ray-oracle predicate, machine syntax and execution, and the output predicate are the expression dependencies of the goal. The exposed-face subtype and full-dimensional polytope predicate are shared unchanged with this book's other staged missions. Contributions needed for a proof may include geometric face finiteness and reconstruction lemmas, but those are not added as unreviewed mission items here.

Selected references

• Branko Grünbaum, Convex Polytopes, 2nd ed., Springer, 2003, §§2.4, 3.1, 3.6, especially the unnumbered Gritzmann–Klee–Westwater theorem on printed pp. 52b–52c (supplied source.pdf, PDF pp. 74–75).
• P. Gritzmann, V. Klee, and D. Westwater, original result cited by Grünbaum as Theorem 5.5 (1995), p. 715. This package follows Grünbaum's stated theorem; the original article was not independently inspected for this packaging step.

Motivation

A polytope may be described by its vertices or by its facets. These descriptions can differ sharply in size even when every vertex has only binary coordinates. Grünbaum's account of 0/1-polytopes in §4.9 records a result of Bárány and Pór: the maximal number of facets grows superexponentially with dimension. The result is an existence statement about the geometry of binary coordinate sets. The source describes random polytopes as witnesses, without specifying a probability distribution as part of the theorem.

Setting

Fix a dimension $d$. A $d$-polytope here is a nonempty convex hull of finitely many points in $\mathbb R^d$ with full affine span. A 0/1-polytope is the convex hull of a subset of $\{0,1\}^d$. Both properties are required of the witness. A facet is a nonempty exposed face of affine dimension $d-1$. The count $f_{d-1}(P)$ uses the book's convention that the empty face has dimension $-1$ and is excluded from natural-indexed face counts. This representation follows Grünbaum §§2.4 and 3.1 for faces and full-dimensional polytopes, and §4.9 for the binary coordinate family.

Formalization target

The single source obligation is the unnumbered Bárány–Pór assertion quoted by Grünbaum in §4.9, printed p. 69a (PDF p. 94). In mathematical notation, the statement is

$$\exists c>1\;\exists D\geq 2\;\forall d\geq D\;\exists P\subseteq\mathbb R^d:\quad P\text{ is a full-dimensional 0/1-polytope}\quad\text{and}\quad c^{d\log d}<f_{d-1}(P).$$

The constant $c$ and threshold $D$ are chosen before $d$; the witness $P$ may depend on $d$. The logarithm in Lean is natural logarithm. Changing a fixed logarithm base rescales the existential constant. The result is asymptotic: it does not assert the inequality in every small dimension. The threshold $D\geq2$ also keeps the natural-number expression $d-1$ in the facet dimension away from underflow.

The goal item Grunbaum2003.barany_por_binary_facet_growth carries this entire obligation. Its body is sorry, so the package presents a compiled statement, not a machine-checked proof. There are no separate source lemmas in this mission and no milestones to assert beyond the goal.

Significance

The theorem shows that binary vertex coordinates do not impose a merely exponential ceiling on the number of facets. It gives a family of full-dimensional binary polytopes whose facet counts eventually exceed an expression of the form $c^{d\log d}$ for one fixed $c>1$. A formal proof would establish that family in the chosen polytope and face-count representation. The present statement makes the quantifier order, full-dimensionality, binary-coordinate restriction, and strict facet inequality explicit for such a proof.

Difficulty

The existence of many binary vertices alone does not certify many facets: one must establish distinct supporting faces of codimension one. The source attributes the strong lower bound to a random construction. A proof must connect that construction to the geometric facet count while keeping one constant valid for every sufficiently large dimension. The mission statement leaves the construction method to the proof, as the quoted book assertion supplies no probability-space parameters or probability bound.

Formalization scope

Lean represents a point of $\mathbb R^d$ by Fin d → ℝ and a polytope by a set of such points. IsDPolytope requires a finite nonempty convex-hull presentation and full affine span. IsZeroOnePolytope requires a convex-hull presentation whose generators have every coordinate equal to zero or one. faceCount P k uses the finite cardinality of nonempty exposed faces of affine dimension $k$; for the full-dimensional witness, faceCount P (d - 1) is the facet count. No face-finiteness, simplicity, or probabilistic assumption is added to the theorem.

The package uses these three expression-essential definitions and the Mathlib real-power and logarithm notation. IsDPolytope and faceCount match the definitions already staged for other missions in this textbook series. A proof may reuse geometric lemmas or supply a new formal version of the Bárány–Pór construction, provided it proves the stated inequality for the original full-dimensional binary family.

Selected references

• Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003, §§2.4, 3.1, 4.9, printed pp. 17, 31, 69a (supplied source.pdf, PDF pp. 35, 51, 94).
• Imre Bárány and Attila Pór, “On 0–1 Polytopes with Many Facets,” Advances in Mathematics 161 (2001), 209–228, Theorem 1.1, p. 210. https://www.renyi.hu/~barany/cikkek/86.pdf

Motivation

The face structure of a cube is unusually regular: its vertices, edges, and higher dimensional faces are indexed by choices of fixed and free coordinates. A natural realization question asks how much of this structure can survive in a polytope of lower dimension. In §4.9 of Convex Polytopes, Grünbaum reports the Joswig–Ziegler construction of neighborly cubical polytopes. The source result says that a cubical $d$-polytope can retain a prescribed low dimensional skeleton of an $n$-cube even when $n>d$. It concerns the entire pattern of faces and containments within that skeleton, rather than a count of vertices or edges alone. The theorem appears on printed page 69b (PDF page 95) of the supplied 2003 edition.

Setting

Fix natural numbers $n>d\geq2$. A $d$-polytope here is a nonempty finite convex hull $P\subseteq\mathbb R^d$ with full affine span. A face is an exposed subset of $P$; the empty face and $P$ itself are included in the face poset. Its order is set inclusion. For a nonempty face, dimension is the dimension of its affine span. The standard $n$-cube is $[0,1]^n$ in $\mathbb R^n$, described coordinatewise by $0\leq x_i\leq1$.

A cubical $d$-polytope is such a full dimensional polytope whose every facet, meaning every nonempty exposed face of dimension $d-1$, has a full face poset order isomorphic to the face poset of a standard $(d-1)$-cube. This is combinatorial cubicality: a facet need not be congruent or affinely equal to a metric cube. It also does not say that the vertices of $P$ have binary coordinates.

The $k$-skeleton face poset consists of the empty face together with all exposed faces of affine dimension at most $k$, with their inherited inclusion order. The source speaks of a skeleton “of” an $n$-cube: the intended correspondence preserves and reflects face containment across the two ambient dimensions. An order isomorphism of the two skeleton face posets is the Lean expression of that combinatorial equivalence.

Formalization target

The single target is the unnumbered Joswig–Ziegler existence theorem as reported by Grünbaum. For every $n>d\geq2$, with $k=\lfloor d/2\rfloor-1$, it asks for a cubical $d$-polytope $P$ such that

$$\operatorname{Skel}_k(P)\cong\operatorname{Skel}_k([0,1]^n).$$

The witness $P$ may depend on both $n$ and $d$. The strict inequality $n>d$ and lower bound $d\geq2$ are source conditions. They have not been expanded or narrowed for this package. For $d=2$ and $d=3$, the cutoff is zero, so the skeleton includes the empty face and vertices. At larger dimensions the claim includes all faces through the stated cutoff and their order relations.

In Lean the theorem is Grunbaum2003.neighborly_cubical_realization. Its conclusion supplies a set in Fin d → ℝ, proves the cubical-polytope predicate of that set, and supplies a nonempty type of order isomorphisms between the two skeleton face posets. The declaration is a compiled statement with a sorry body. No machine-checked proof of the existence theorem is claimed here.

Significance

This theorem separates dimension of realization from the low dimensional combinatorics being realized. In particular, an $n$-cube skeleton can occur inside a lower dimensional cubical polytope, subject to the precise cutoff above. The conclusion is a structural face-poset match, not a numerical face-vector equality. A complete formal proof would establish an existence statement about genuine full dimensional convex polytopes and an order equivalence of their truncated face systems.

The reusable formal objects in this package are the full dimensional polytope predicate, the face subtype, the skeleton subtype, the standard cube, and the cubical-polytope predicate. They express the geometry and combinatorics independently of the particular neighborly realization theorem. The goal is kept as one mission because the source states one dimension-parametric existence result; the definitions are only its expression dependencies.

Difficulty

A lower dimensional realization cannot retain every face of a higher dimensional cube. The theorem therefore specifies exactly which dimensions of faces can be preserved. Merely matching the number of vertices would leave edges, higher faces, and incidence unconstrained. Likewise, requiring all facets to look like cubes says nothing by itself about whether a large cube's skeleton appears. A proof must produce a genuine cubical witness and the ordered skeleton correspondence simultaneously, for every allowed pair of dimensions.

Formalization scope

The Lean coordinate spaces are real functions on Fin d and Fin n. Natural division d / 2 is floor division, and the assumption $d\geq2$ makes natural subtraction by one agree with the source's integer cutoff. The full dimensional condition rules out an empty or lower dimensional witness. IsExposed supplies faces, including the improper empty and whole faces; the skeleton predicate treats the empty face explicitly because its conventional dimension is $-1$, outside natural-number dimensions. The nonempty face dimension is the finrank of the affine direction.

The face-poset order is inherited from set inclusion. Cubicality is checked on each qualifying facet by an order isomorphism with the full face poset of the reference cube. The target's order isomorphism similarly covers the whole selected skeleton rather than only vertices. Contributions toward a proof may introduce construction and comparison lemmas, but none is asserted as an additional theorem item in this reviewed package.

Selected references

• Branko Grünbaum, Convex Polytopes, 2nd ed., Springer, 2003, §4.9, unnumbered Joswig–Ziegler existence theorem, printed p. 69b / PDF p. 95 of the supplied source.pdf.
• Michael Joswig and Günter M. Ziegler, “Neighborly cubical polytopes,” 2000, arXiv:math/9812033. This is corroboration for the construction; the mission retains Grünbaum's stated parameter range.

Motivation

A convex set can be studied through its images in lower-dimensional spaces. Each image retains part of the geometry while discarding information along the directions that are collapsed. Finite convex hulls behave well under affine maps: the image of a convex hull of finitely many points is again the convex hull of finitely many points. The converse is subtler. It asks whether sufficiently comprehensive lower-dimensional image data forces the original bounded convex set itself to have a finite description by points.

This mission formalizes the projection-recognition criterion attributed to Klee in Branko Grünbaum's Convex Polytopes, second edition, §5.1, Theorem 5.1.8, printed page 74 (PDF page 100 of the supplied source). The criterion concerns every projection into one suitable intermediate dimension, not a chosen coordinate view. It therefore characterizes a global property of the original set by an entire family of dimension-reducing images.

Setting

Fix a natural number $d\geq 3$. Real coordinate space $\mathbb R^d$ is represented in Lean by functions from Fin d to the real numbers. A subset $K\subseteq\mathbb R^d$ is convex when it contains every line segment joining two of its points, and it is bounded when all of its points lie within some finite metric ball. Neither condition requires $K$ to be nonempty, closed, or full-dimensional.

For a set $V$, its convex hull $\operatorname{conv}(V)$ is the smallest convex set containing $V$. In the convention used by Grünbaum in §3.1, printed page 31 (PDF page 51), a polytope is equivalently the convex hull of a finite set. The generating set need not be a minimal vertex set, and the formal statement permits the finite set to be empty or contained in a proper affine subspace.

An affine map preserves affine combinations. A surjective affine map

$$f:\mathbb R^d\longrightarrow\mathbb R^j$$

has image dimension exactly $j$. When $j<d$, it is singular. Grünbaum defines a projection at the opening of §5.1, printed page 71 (PDF page 97), as an image under a singular affine map. Using a surjective affine map to coordinate $j$-space represents a projection to a $j$-dimensional affine space followed by an affine choice of coordinates. Whether a set is a finite convex hull is unchanged by that coordinate identification.

Formalization target

For every bounded convex set $K\subseteq\mathbb R^d$, the target is the equivalence

$$K\text{ is a polytope} \quad\Longleftrightarrow\quad \exists j\in\mathbb N,\;2\leq j<d,\; \forall f:\mathbb R^d\twoheadrightarrow\mathbb R^j\text{ affine},\; f(K)\text{ is a polytope}.$$

The dimension $j$ may depend on $K$, but it is selected before the universal quantifier over affine maps. Every surjective affine map with that target dimension is tested. For each map, the finite set whose convex hull is $f(K)$ may be different; no common projected generator set and no uniform bound on its size is asserted. This is one theorem with both directions, so there are no separate milestone statements in the package.

Significance

The forward implication records the stability of finite convex hulls under affine images. The recognition implication is the substantive part: under boundedness and convexity, polytopality of every projection in one eligible intermediate dimension forces $K$ itself to be a polytope. The conclusion concerns $K$ rather than merely its closure and does not add a hidden closedness assumption.

The theorem is established mathematics in the cited textbook. The present artifact is a compiled formal statement, not a completed machine-checked proof: its theorem body is by sorry. Completing it would connect Mathlib's finite convex-hull and affine-map infrastructure to the classical projection-recognition argument while preserving the source's quantifier order and lower-dimensional boundary cases.

Difficulty

Each projected set may have its own unrelated finite generating set. Those separate witnesses do not directly assemble into a finite generating set in the original ambient space, because every projection has discarded a kernel direction. Checking one convenient projection is inadequate: that image can conceal structure occurring precisely in the collapsed directions. The challenge is therefore to use the universal family of projections at the selected dimension without replacing it by a fixed axis projection or adding compactness, full dimensionality, or nonempty interior.

Formalization scope

The Lean declaration is Grunbaum2003.polytope_iff_polytope_projections, in the book-wide namespace Grunbaum2003. It takes Bornology.IsBounded K and Convex ℝ K as the exact domain hypotheses. Polytopality is written directly as existence of a finite set with convex hull equal to the set; no stronger book-local full-dimensional polytope predicate is used. Projections are all surjective real affine maps from Fin d → ℝ to Fin j → ℝ.

The explicit premise $3\leq d$ records the admissible ambient range required by $2\leq j<d$. In dimension three, the only possible target dimension is two. No displayed existential claim is made for dimensions zero, one, or two, where no such $j$ exists. Within every admissible dimension, empty sets, singletons, and other lower-dimensional bounded convex sets remain in scope. Surjectivity prevents a map from having rank below $j$, and the strict inequality $j<d$ ensures dimension loss. There are no expression-essential book-local definitions or supporting theorems; the only dependencies are Mathlib modules for convex hulls, boundedness, finite-dimensional coordinate spaces, and affine maps.

Selected references

• Branko Grünbaum, Convex Polytopes, 2nd ed., Graduate Texts in Mathematics 221, Springer, 2003, §3.1 and §5.1, especially Theorem 5.1.8 on printed page 74. Springer book record and DOI.

Motivation

A basic classification question in polytope theory asks what combinatorial types can occur when the dimension and number of vertices are fixed. The question is not merely whether there are finitely many types. Effective enumeration asks for a uniform algorithm which produces the complete list, with no omissions and no repeated combinatorial type. This converts a structural finiteness assertion into a finite procedure that can in principle support tabulation, comparison, and exhaustive study of small polytopes.

Grünbaum formulates this enumeration problem in §5.5 of Convex Polytopes and states its solvability as Theorem 5.5.2, printed p. 91 (PDF p. 117 of the supplied source). The surrounding discussion represents a combinatorial type by a finite scheme recording which subsets of labelled vertices form proper faces. The source then selects one representative for every realizable type. This mission follows that statement and encoding, as recorded in the supplied edition of the book (Springer DOI).

Setting

Fix natural numbers $d$ and $k$. A $d$-polytope is a nonempty finite convex hull in real coordinate space $\mathbb R^d$ whose affine span is the whole space. Its faces are exposed faces. Following Grünbaum's convention, this includes the empty face and the polytope itself as improper faces. The natural-valued function $f_j(P)$ counts nonempty exposed faces whose affine direction has dimension $j$; in particular, $f_0(P)$ is the number of vertices.

A finite scheme is encoded as a list $S$ of lists of natural numbers. Each inner list represents a finite subset of vertex labels; its order and repeated entries have no mathematical meaning. The predicate SchemeRealizes k S P supplies an injective labelling $V:\operatorname{Fin}(k)\to\mathbb R^d$ whose range is exactly the set of exposed singleton vertices of $P$. For every finite subset $J$ of natural numbers, membership of $J$ in the scheme is equivalent to the existence of a nonempty proper exposed face whose labelled vertices are exactly $J$. Quantifying over every finite natural-number subset prevents an out-of-range label from silently denoting a face.

Two polytopes have the same combinatorial type when their complete face posets are order-isomorphic. The Lean subtype PolytopeFace P contains every exposed face of $P$, including the two improper faces, and inherits the inclusion order. Thus Nonempty (PolytopeFace P ≃o PolytopeFace Q) is the formal equivalence relation used in the target.

Formalization target

The target is Grünbaum's Theorem 5.5.2 (book record and DOI). In Lean it states that there is a single function

$$E:\mathbb N\to\mathbb N\to \operatorname{List}(\operatorname{List}(\operatorname{List}(\mathbb N)))$$

which is computable and has the required behavior for every $d$ and $k$. Its finite output $E(d,k)$ satisfies three clauses. First, every output scheme is realized by some $d$-polytope. Second, every $d$-polytope with $k$ vertices realizes an output scheme. Third, if realizations of two output positions have order-isomorphic complete face posets, then those positions are equal. The three clauses jointly express soundness, completeness, and selection of a single representative per combinatorial type.

The theorem is Grunbaum2003.combinatorial_types_effectively_enumerable. Its body is an intentional sorry: this package supplies the reviewed, compiling statement and does not claim a machine-checked proof.

Significance

The conclusion gives more than abstract finiteness. It asserts one terminating procedure, uniform in both parameters, whose finite result represents all and only the desired types. Soundness prevents junk schemes; completeness prevents a legitimate polytope type from being missed; uniqueness prevents the output from counting the same type twice under different label lists. The theorem thereby isolates the precise data that an implementation or a formal proof must justify.

A formal proof would connect geometric realizability, finite incidence data, and computability in one development. The reusable infrastructure includes a full-dimensional finite-hull predicate, exposed-face counting, the complete exposed-face poset, and a labelled finite-scheme realization predicate. These definitions can also support formal statements about realization tests and enumerations under additional restrictions, without changing this mission's source obligation.

Difficulty

Finite syntactic generation alone is insufficient: most arbitrary families of vertex subsets need not be face systems of convex polytopes. Conversely, merely knowing that only finitely many combinatorial types exist does not provide an effective method for recognizing realizable schemes. The target must establish a total algorithm while simultaneously proving that every accepted scheme is geometrically realizable, every eligible polytope is represented, and no two selected entries encode order-isomorphic face posets.

Vertex relabelling is another source of redundancy. Two different nested lists can describe the same incidence structure, and two different geometric realizations can have the same face lattice. The uniqueness clause therefore compares realized complete face posets rather than list equality. A procedure that only enumerates labelled presentations, or one that decides equivalence without selecting representatives, would not prove the stated theorem.

Formalization scope

The Lean function $E$ returns nested finite lists, so finiteness of each output and of each scheme is built into the type. Mathlib's Computable₂ supplies total computability on the paired natural inputs. The quantifier order chooses one $E$ before $d$, $k$, and any polytope, preserving uniformity. No rational-coordinate, simplicial, or fixed-combinatorics hypothesis is introduced.

IsDPolytope requires a nonempty finite convex hull with full affine span. faceCount P 0 = k imposes the prescribed vertex count. SchemeRealizes requires exactly the exposed singleton vertices and exactly the nonempty proper exposed faces under an injective finite labelling. PolytopeFace retains the empty and full improper faces for the final order-isomorphism comparison. These choices prevent the statement from becoming vacuous through an unconstrained incidence code or a predicate that assumes realizability.

Natural-number boundary cases remain explicit. If no $d$-polytope with $k$ vertices exists, an empty output is permitted. In dimension zero, the unique point has one vertex and no nonempty proper face, so the empty scheme represents it. This coding extension does not remove any positive-dimensional case. The expression dependencies are exactly the four definitions listed above; proof-only lemmas and unrelated theorems from the book are not included as mission items.

Selected references

• Branko Grünbaum, Convex Polytopes, 2nd ed., prepared by Volker Kaibel, Victor Klee, and Günter M. Ziegler, Graduate Texts in Mathematics 221, Springer, 2003. §5.5, especially Theorem 5.5.2 on printed p. 91 / supplied PDF p. 117. https://doi.org/10.1007/978-1-4613-0019-9

Why subpolytopes matter

A convex polytope can be studied metrically, through coordinates and lengths, or combinatorially, through the inclusion order of its faces. Grünbaum's Convex Polytopes develops the second viewpoint systematically: two polytopes have the same combinatorial type when their complete face posets are order-isomorphic. Chapter 7 studies neighborly polytopes, which have as many low-dimensional faces as their vertex sets permit. These objects are central test cases because very strong local face incidence coexists with a large variety of realizations and combinatorial types.

The capstone of this mission is the rigidity statement attributed in §7.5 to Shemer: in even dimension, the combinatorial type of a neighborly polytope determines the combinatorial type of every subpolytope spanned by a subset of its vertices. Here “rigid” is exclusively combinatorial. It does not assert preservation of lengths, angles, coordinates, or projective realization. The source statement appears in Branko Grünbaum, Convex Polytopes, second edition, §7.5, printed p. 129b / PDF p. 161 (Springer edition).

Polytopes, faces, and neighborliness

The Lean development represents the ambient real space of dimension $d$ as Fin d → ℝ. A predicate IsDPolytope P says that $P$ is the convex hull of a finite nonempty vertex set and has full affine span. Faces are modeled by Mathlib's exposed-face predicate. The type PolytopeFace P contains all exposed faces ordered by inclusion, including the empty face and $P$ itself; an order isomorphism of these types is the formal representation of combinatorial equivalence.

For a positive integer $k$, a polytope is $k$-neighborly when every $k$-element set of vertices spans a proper face and is exactly the vertex set of that face. The definition IsKNeighborly k P states this directly for finite sets of exposed singleton vertices. Grünbaum defines an even-dimensional polytope of dimension $2r$ to be neighborly when it is $r$-neighborly. The theorem therefore assumes $r \ge 1$ and uses IsKNeighborly r for both parent polytopes.

Formalization target

Let $P$ and $Q$ be full-dimensional neighborly polytopes in $\mathbb{R}^{2r}$. Their vertices are enumerated injectively by maps $V,W : \operatorname{Fin}(m) \to \mathbb{R}^{2r}$. A permutation $\theta$ records the prescribed correspondence between the two vertex sets, and an order isomorphism $\Phi$ between the full face posets witnesses that this correspondence comes from a combinatorial equivalence of the parent polytopes.

For every index set $I \subseteq \operatorname{Fin}(m)$, the target produces an order isomorphism

$$\mathcal F\bigl(\operatorname{conv}(V(I))\bigr) \simeq \mathcal F\bigl(\operatorname{conv}(W(\theta(I)))\bigr),$$

and requires it to carry each selected singleton vertex $V(i)$ to $W(\theta(i))$. The quantifier over $I$ is unrestricted. Empty, singleton, lower-dimensional, and full vertex subsets are all included. No selected subpolytope is required to be full-dimensional or neighborly.

What the theorem determines

Knowing only how many neighborly combinatorial types exist would not reconstruct any particular vertex-induced subpolytope. The rigidity theorem is stronger: once the complete face-poset type of the parent and its vertex correspondence are fixed, the complete face-poset type of every labelled vertex subpolytope is fixed as well. This is why the formal conclusion keeps the label-preservation clause rather than stating only the existence of an abstract order isomorphism.

The result is known mathematics, while the Lean declaration supplied here is statement-only and retains sorry as its proof placeholder. The formalization contribution is therefore a precise target and its expression-essential vocabulary, not a claim that Shemer's proof has already been machine checked. A completed proof must establish exactly this uniform reconstruction theorem without adding metric hypotheses or restricting the allowed subsets.

Where the difficulty lies

The parent face-poset isomorphism directly identifies the faces already present in $P$ and $Q$, but a subpolytope can have faces that are not faces of its parent. Consequently, restricting $\Phi$ to selected vertices does not automatically yield the required subpolytope face-poset isomorphism. The theorem must control how all new faces created by taking a vertex subset depend on the original neighborly combinatorics. That gap is the substantive content of rigidity and prevents the conclusion from being a routine restriction of the given parent isomorphism.

Formalization scope

The scope is deliberately narrow. IsDPolytope, IsKNeighborly, and PolytopeFace are the only local definitions required to express the theorem. Vertices are exposed singletons, combinatorial types are full face-poset order types, and convex hulls remain in the original ambient space even when a selected subset is lower-dimensional. The theorem assumes positive even dimension through $2r$ with $r \ge 1$. It imposes no metric congruence, no choice of realization normal form, and no cardinality lower bound on the selected subset.

Useful contributions include a proof of the stated target and reusable lemmas connecting neighborliness, vertex subsets, and exposed-face posets. A reformulation that covers only nonempty or full-dimensional subsets, forgets the prescribed vertex labels, or replaces face-poset equivalence by equality of face counts would not satisfy this mission.

Selected references

• Branko Grünbaum, Convex Polytopes, 2nd ed., Graduate Texts in Mathematics 221, Springer, 2003, especially §§2.4, 3.1–3.2, 7.1–7.2, and 7.5. DOI

Why neighborly families matter

A neighborly family of convex polytopes is a collection in which every two distinct members meet in the largest dimension possible without having a full-dimensional overlap: their intersection has codimension one. The question is extremal. For a fixed ambient dimension, how large can such a family be when its members must also satisfy a geometric restriction? Chapter 7 of Branko Grünbaum's Convex Polytopes records Joseph Zaks's answer for central symmetry: in every dimension at least three, no finite upper bound exists. The result belongs to discrete geometry because it combines pairwise intersection constraints, dimension, and symmetry across an entire finite family rather than studying the face structure of one polytope.

The theorem is cited by Grünbaum in §7.5 as the resolution of a problem posed in §7.4. The original result is Zaks's 1986 paper, “Arbitrarily large neighborly families of symmetric convex polytopes”. This mission formalizes the centrally symmetric conclusion quoted in the textbook, without adding the stronger congruence variants discussed elsewhere.

Geometric setting

Fix an integer $d\ge 3$ and work in the real coordinate space $\mathbb{R}^d$. In Lean this space is represented by Fin d → ℝ. A $d$-polytope is a nonempty finite convex hull whose affine span is the entire ambient space. Full affine span is essential: it rules out treating a lower-dimensional polytope embedded in $\mathbb{R}^d$ as a $d$-polytope.

A polytope $P$ is centrally symmetric when there is a center $c\in\mathbb{R}^d$ such that reflection through $c$ leaves $P$ invariant. The center is chosen separately for each member of the family; the theorem does not require one common center. In coordinates the reflection is $x\mapsto 2c-x$, represented in Lean by AffineEquiv.pointReflection ℝ c.

A finite family $S$ of $d$-polytopes is neighborly in the sense of Grünbaum §7.4 when, for every distinct $P,Q\in S$, the intersection $P\cap Q$ has affine dimension $d-1$. This use of “neighborly” concerns pairwise intersections among several convex sets. It is different from the familiar notion of a neighborly polytope, where small subsets of the vertices of a single polytope span faces.

Formalization target

For every $d\ge 3$ and every natural-number threshold $N$, the target asserts the existence of a finite set $S$ such that

$$|S|\ge N,$$

every $P\in S$ is a centrally symmetric $d$-polytope, and every distinct pair $P,Q\in S$ satisfies

$$P\cap Q\ne\varnothing, \qquad \dim\!\bigl(\operatorname{aff}(P\cap Q)\bigr)=d-1.$$

Quantifying over every threshold $N$ is the precise finite formulation of “arbitrarily large.” It does not claim that one infinite family has all these properties. The witness family may depend on both $d$ and $N$.

Significance

The result shows that central symmetry does not impose a finite ceiling on neighborly-family size once $d\ge 3$. The conclusion is therefore a structural existence statement, not merely a construction of a single large example. It also separates two issues that can otherwise be conflated: each member has an internal symmetry, while neighborliness is a relation between distinct members.

The mathematics is known, but the Lean item in this mission is statement-only and remains to be proved. A complete formalization would connect finite convex-hull geometry, affine dimension, affine reflections, and pairwise intersections in one reusable development. The full-dimensional polytope predicate is shared across the textbook series and is packaged as an expression-essential definition rather than hidden inside the theorem.

Difficulty

The quantified size threshold prevents a finite catalogue or a fixed example from resolving the target. The pairwise condition also couples every new member to all earlier members: verifying central symmetry for each polytope alone gives no control over the dimensions of its intersections with the rest of the family. The explicit nonemptiness condition matters because affine dimension is represented with a natural-valued finrank; without it, conventions for the empty affine span could obscure the intended codimension-one requirement.

Formalization scope

The family is a Finset, so its members are distinct and its cardinality is the ordinary finite cardinality. Every member satisfies Grunbaum2003.IsDPolytope, which requires a nonempty finite generating set, equality with its convex hull, and full affine span. Central symmetry is expressed by invariance under a point reflection with an individually quantified center. For distinct members, the intersection must be nonempty and the rank of the direction of its affine span, plus one, must equal $d$.

No common center, congruence, translate-only model, face-to-face condition, or infinite-family claim is included. The case $d=3$ is included, while dimensions below three are excluded exactly as in the source. The case $N=0$ is harmless because the same theorem is quantified over every positive threshold as well. The scope contains the one reviewed Zaks theorem and its single expression-essential polytope definition; it does not introduce unrelated chapter theorems or a proof strategy.

Selected references

• Joseph Zaks, Arbitrarily large neighborly families of symmetric convex polytopes, Geometriae Dedicata 20 (1986), 175–179. DOI: 10.1007/BF00164398
• Branko Grünbaum, Convex Polytopes, 2nd ed., Graduate Texts in Mathematics 221, Springer, 2003. DOI: 10.1007/978-1-4613-0019-9

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.

Why boundary refinement and skeleton embeddings matter

A convex polytope carries more than its underlying topological ball. Its faces form a finite complex whose incidence relations record the polytope's combinatorial structure. Chapter 11 of Branko Grünbaum's Convex Polytopes asks how this structure can be represented by subdivisions and by embeddings into Euclidean spaces of smaller dimension. The first target places every polytope boundary over the simplest boundary complex in the same dimension, that of a simplex. The second determines exactly how much ambient dimension is needed to realize any prescribed skeleton, both topologically and as a genuine polytopal complex.

These are established mathematical results, not open conjectures. The mission poses their reviewed Lean statements as formal proof tasks. It groups Theorems 11.1.1 and 11.1.9 because both use the boundary-complex, carrier, refinement, skeleton, and incidence-equivalence model introduced at the start of §11.1. They remain separate statements with separate quantified objects; no common homeomorphism, realization, or witness is imposed between them.

Geometric and combinatorial setting

A d-polytope is represented in Lean as the convex hull of a nonempty finite subset of Fin d → ℝ whose affine span is the whole ambient space. A face uses Mathlib's exposed-face convention. For polytopes this includes the proper exposed faces as well as the empty and full improper faces.

The boundary complex boundaryFaces P consists of every exposed face of P except P itself. Thus the empty face is retained. Its carrier is the union of those cells. The statement BoundaryRefines P Q supplies one homeomorphism between the two complete boundary carriers. For each boundary face of Q, its inverse image must be exactly the union of a finite subfamily of boundary faces of P, and that subfamily must be closed under taking faces. Exact inverse-image equality is essential: containment alone would not express the source's refinement relation.

The k-skeleton face poset SkeletonFace P k contains the empty face and every nonempty exposed face of affine dimension at most k, ordered by inclusion. Its topological carrier skeletonCarrier P k is the union of these cells. A finite polytopal complex in real m-space is a finite family of polytopal cells, explicitly permitting the empty cell, closed under taking faces, with each pairwise intersection a face of both participating cells. Combinatorial equivalence is represented by an order isomorphism of the complete cell posets, rather than merely by a homeomorphism of their carriers.

Formalization targets

Boundary refinement by a simplex

For every natural dimension d, every full-dimensional d-polytope P, and every affinely independent family of d+1 vertices in real d-space, the first target states

$$\mathcal B(P)\text{ refines }\mathcal B(T^d).$$

The chosen vertices describe an arbitrary d-simplex. The result does not assume that P is simplicial. The same homeomorphism controls all target-face inverse images, and the zero-dimensional case retains its empty boundary carrier.

Exact skeleton embedding dimensions

For 1 ≤ k ≤ d and every d-polytope P, the second target identifies two attained minima. The first ranges over dimensions m for which the carrier of the k-skeleton is homeomorphic to some subset of real m-space. The second ranges over dimensions m for which a finite polytopal complex in real m-space has a cell poset order-isomorphic to the complete k-skeleton face poset. Both minima equal

$$a(d,k)=b(d,k)= \begin{cases} d, & d\le k+1,\\ \min(d-1,2k+1), & d>k+1. \end{cases}$$

This compact formula preserves the four cases stated in Theorem 11.1.4: d=k, d=k+1, k+2≤d≤2k+2, and d≥2k+2. The latter two formulas agree at their shared endpoint. Applying the arbitrary-polytope statement to simplices retains the source comparison with a(d,k) and b(d,k).

Significance

The refinement theorem gives a uniform relationship between the boundary complex of an arbitrary polytope and the simplex boundary. It preserves both topology and the subdivision data carried by faces. The embedding theorem then gives the exact ambient dimension required by every k-skeleton, while showing that allowing an arbitrary topological embedding does not improve on the best dimension obtainable from a combinatorially equivalent polytopal complex.

Formalizing these targets provides reusable infrastructure for boundary carriers, face-closed refinements, skeleton carriers, and finite polytopal complexes. The definitions distinguish topological equivalence from incidence equivalence and record attainment as well as lower bounds through IsLeast. The theorem bodies remain open: the proposal does not claim that either classical result already has a Lean proof.

Difficulty

For the refinement target, a homeomorphism of boundary carriers alone is insufficient. One must also prove, simultaneously for every target cell, that its inverse image is exactly a finite union of source cells closed under faces. The obvious topological equivalence of polytope boundaries therefore does not establish the required combinatorial refinement.

For the embedding target, constructing one realization in the displayed dimension proves only attainment. It does not rule out all realizations in smaller dimensions. Conversely, a lower-bound argument does not construct the topological subset or polytopal complex required by IsLeast. Both notions of realization must meet at the same explicit value without replacing the full cell-poset equivalence by a weaker topological condition.

Formalization scope

All ambient spaces are finite-dimensional real coordinate spaces. Polytopes are nonempty finite convex hulls, and the goal polytopes are full-dimensional. Exposed faces include the empty face and the whole polytope; the boundary removes only the whole polytope. Skeleton dimension is the real dimension of an affine-span direction, with the empty face admitted separately. The topological minimum ranges over arbitrary subsets with the subspace topology, while the combinatorial minimum ranges only over finite polytopal complexes satisfying face closure and the common-face intersection condition.

IsLeast asserts both membership of the displayed value and that it is a lower bound for every attainable dimension. The condition 1 ≤ k ≤ d excludes the source's untreated k=0 case. Natural subtraction occurs only in the branch d>k+1, so the formula does not gain a truncated-subtraction shortcut. Contributions must not drop attainment, restrict the arbitrary polytope, replace exact inverse-image equality by containment, omit empty faces, weaken order isomorphism to a carrier homeomorphism, or require the two source theorems to share a witness.

Selected references

• Branko Grünbaum, Convex Polytopes, 2nd ed., Graduate Texts in Mathematics 221, Springer, 2003, §11.1, Theorems 11.1.1, 11.1.4, and 11.1.9. DOI: 10.1007/978-1-4613-0019-9.

Why reconstruction from partial face data matters

A convex polytope has both a geometric realization and a finite combinatorial structure: its faces, ordered by inclusion. Reconstruction asks how much of that structure must be known before the rest is forced. Chapter 12 of Branko Grünbaum's Convex Polytopes distinguishes several forms of unambiguity and then proves reconstruction results for general polytopes and for important special classes. The central input is not a coordinate description. It is a lower-dimensional part of the face lattice, such as the graph or a higher skeleton.

This mission groups five established results that address the same recovery problem under different hypotheses. The main theorem reconstructs every d-polytope, for d ≥ 3, from a supplied equivalence of its (d−2)-skeleton. The supporting targets sharpen the amount of data needed for simple polytopes, simplicial polytopes, and zonotopes, and record a polynomial-time version whose output is the vertex–facet incidence relation. Each theorem retains its own quantified polytopes, equivalence, and reconstruction witness. Grouping them does not require a single witness to serve all five regimes.

Face lattices, skeletons, and unambiguity

A d-polytope is represented as the convex hull of a nonempty finite subset of Fin d → ℝ, with affine span equal to the whole ambient space. A face is an exposed face in Mathlib's sense. This convention includes the empty face and the polytope itself. PolytopeFace P is the resulting face poset ordered by set inclusion.

For a natural number k, the k-skeleton face poset SkeletonFace P k contains the empty face and every nonempty exposed face whose affine dimension is at most k. An equivalence of skeletons is an order equivalence, so it preserves and reflects every inclusion relation among the retained faces. Strong unambiguity is represented by demanding an extension of every supplied skeleton equivalence, rather than merely asserting that some full face-lattice equivalence exists. The extension equation requires agreement on every skeleton face.

The graph of a polytope is modeled through its vertices and one-dimensional faces. PolytopeVertex P consists of points whose singleton is exposed. Two distinct vertices are adjacent in polytopeGraph P when they lie in a common one-dimensional exposed face. A source polytope is simple when every vertex has exactly d graph neighbors. A simplicial polytope is one whose facets are simplices. A zonotope is a finite vector sum of closed line segments; full dimension is imposed separately by the d-polytope hypothesis.

Formalization targets

General reconstruction from the (d−2)-skeleton

For d ≥ 3, d-polytopes P and Q, and every supplied order equivalence

$$\varphi:\operatorname{Skel}_{d-2}(P)\simeq_o\operatorname{Skel}_{d-2}(Q),$$

the main target produces an order equivalence of the complete face posets whose restriction is exactly φ. This is the explicit face-lattice reformulation of Theorem 12.3.1. It asserts strong and weak d-unambiguity, but it does not add dimensional unambiguity.

Reconstruction from graphs and half-dimensional skeletons

The Blind–Mani target uses only the 1-skeleton when the source is simple. The target polytope is arbitrary in the same dimension; its simplicity is not assumed separately. The Björner–Edelman–Ziegler target likewise uses the 1-skeleton when the source is a full-dimensional zonotope, without requiring the target to be a zonotope.

Perles's target has a different domain. The source is a simplicial d-polytope, the target is an arbitrary e-polytope, and the input compares their floor(d/2)-skeletons. Its conclusion includes both e=d and extension of the supplied skeleton equivalence. Thus this clause, unlike the other reconstruction clauses, explicitly includes dimensional unambiguity.

Polynomial-time incidence reconstruction

The algorithmic target states that one binary function works uniformly for every d ≥ 3, every vertex count, and every valid labelled d-polytope input. The input contains the complete duplicate-free table of nonempty faces in dimensions at most d−2; the output contains exactly the facets, as labelled vertex sets. Dimension, vertex count, and row count are self-delimiting headers, followed by dense incidence rows. Correctness is required on valid encodings, while the binary function itself is total. ContainmentPolyTime uses Mathlib's Turing-machine polynomial-time predicate together with finite stack alphabets.

Significance

The general theorem says that codimension-two face data already fixes every missing facet and incidence relation. The special-class results show that much smaller data can suffice: only the graph for simple polytopes and zonotopes, and the half-dimensional skeleton for simplicial polytopes. Perles's result also recovers ambient dimension. The algorithmic theorem separates mere uniqueness from effective recovery by requiring one polynomial-time procedure and a concrete vertex–facet output.

Formalizing these results creates reusable interfaces for face-poset reconstruction, graph-based simplicity, zonotopes, and finite incidence encodings. It also records distinctions that informal summaries can blur: extension of every supplied equivalence versus existence of an unrelated isomorphism; combinatorial reconstruction versus dimension recovery; and uniqueness versus polynomial-time computability. The statements are established mathematics, but their Lean theorem bodies remain open and use sorry; this mission makes no proof-completion claim.

Difficulty

Counting faces or matching their dimensions does not reconstruct the face lattice. The conclusion must preserve every inclusion relation and agree with the specific equivalence supplied on the visible skeleton. An arbitrary isomorphism of complete face lattices would be too weak if it failed to extend that map.

For simple polytopes and zonotopes, graph isomorphism alone does not expose higher-dimensional faces directly; the target still asks for all incidences. In the simplicial case, reconstructing the lattice without proving e=d would omit the dimensional-unambiguity clause. For the effective result, a mathematical reconstruction argument is insufficient unless it yields one uniform polynomial-time binary function. Conversely, an efficient procedure on an incomplete or coordinate-dependent input would not meet the stated incidence model.

Formalization scope

All geometric ambient spaces are finite-dimensional real coordinate spaces. Full-dimensional polytopes are nonempty finite convex hulls. Exposed faces include both improper faces. Skeletons retain the empty face separately, avoiding a natural-number encoding of its source dimension −1. Natural subtraction in d−2 is protected by the explicit 3 ≤ d hypothesis wherever that threshold is used.

The graph definition removes loops and symmetrizes adjacency. Simplicity is the exact neighbor-cardinality condition at every vertex. The zonotope definition allows arbitrary segment endpoints and degenerate summands, but the separate full-dimensionality hypothesis rules out a lower-dimensional source. Only the simplicial theorem compares different ambient dimensions and concludes their equality.

The algorithm receives no real coordinates. Its vertex map is injective and has range exactly the exposed singleton faces. The input and output row predicates are biconditionals, so they prohibit missing faces and extraneous rows; Nodup prohibits repetitions. The empty face is implicit, and the output row order is unrestricted. Contributions must not weaken extension to unrelated existence, assume the target belongs to the source's special class, omit Perles's dimension equality, replace complete incidence tables by partial data, or allow the polynomial bound to depend on the individual instance.

Selected references

• Branko Grünbaum, Convex Polytopes, 2nd ed., Graduate Texts in Mathematics 221, Springer, 2003, §§12.1–12.4 and §15.1. DOI: 10.1007/978-1-4613-0019-9.
• Roswitha Blind and Peter Mani-Levitska, Puzzles and polytope isomorphisms, Aequationes Mathematicae 34 (1987), 287–297. DOI: 10.1007/BF01830678.
• Anders Björner, Paul H. Edelman, and Günter M. Ziegler, Hyperplane arrangements with a lattice of regions, Discrete & Computational Geometry 5 (1990), 263–288. DOI: 10.1007/BF02187791.

A polytope can be represented by cutting a higher-dimensional simplex with an affine flat. The geometry of the cut determines the resulting polytope. Perles's prescribed-point theorem adds a constraint to this representation: the cutting flat must pass through a point chosen in advance inside the simplex. Theorem 5.1.10 in Branko Grünbaum's Convex Polytopes, second edition (2003), shows that this requirement can always be met when the simplex has enough facets. The source is §5.1, printed page 74, with the section convention introduced on printed page 71.

A polytope is the convex hull of finitely many points. In this mission it is nonempty and full-dimensional in its ambient real coordinate space. Thus a d-polytope P in R^d contains enough points to span that space affinely. A face is the set of points on which a supporting linear functional attains its maximum; a facet is a face of dimension d−1. Different supporting functionals can describe the same face, so the facet allowance counts geometric faces rather than inequalities used to describe them.

A k-simplex is the convex hull of k+1 affinely independent points. Write its vertices as v₀,…,vₖ in R^k and its convex hull as T. Affine independence means there is no nontrivial affine relation among these vertices. The simplex therefore has dimension k, and its interior is taken in the whole space R^k. No restriction is placed on its side lengths or angles. A d-flat is a translate of a d-dimensional linear subspace. A section of T by such a flat L is the entire intersection T ∩ L.

The target is the following existence assertion. For every d-polytope P with at most k+1 facets, every k-simplex T in R^k, and every p in the interior of T, there is a d-flat L such that

$$p\in L,\qquad T\cap L\text{ is affinely equivalent to }P.$$

An affine equivalence here preserves affine combinations and is invertible on the affine spans. It can change lengths and angles. In the stated coordinates, it is represented by an injective real affine map A from R^d onto L satisfying

$$A(P)=T\cap L.$$

All input data, including the interior point p, are universally quantified before the flat and map are chosen. The flat can depend on these data. The source writes the facet allowance as f and the simplex dimension as f−1; the notation here uses f=k+1.

The prescribed-point conclusion gives control beyond the existence of some simplex section representing P. It permits the simplex and an interior point to be fixed while the cutting flat is selected to recover the given polytope. The conclusion concerns its full affine geometry: the image of every point of P lies in the section, and every point of the section belongs to that image. This is the additional representational constraint discussed immediately before Theorem 10 on printed page 74.

The difficulty lies in meeting these requirements simultaneously. A flat through the chosen point can have an intersection of the wrong affine shape. A section with the correct affine shape need not contain the prescribed point. The theorem requires both properties for every allowed simplex and point, while retaining the original facet bound. Neither a special regular simplex nor a selected interior point captures this quantifier structure.

The formal statement uses real coordinate spaces indexed by finite sets, finite convex hulls, affine spans, exposed faces, and affine maps. Nonempty faces are counted by their affine dimension. In dimension zero the facet allowance is automatic: under the convention counting the empty face it contributes at most one facet, which fits the allowance k+1. This avoids interpreting natural subtraction d−1 as a facet dimension at d=0. The zero-dimensional simplex and zero-dimensional polytope remain within the statement.

This is a known geometric theorem whose formal proof remains to be supplied. The target contains one proof placeholder. The definitions specify the underlying geometry concretely. The mission consists of the single prescribed-section theorem; its definitions support that statement, and no separate supporting theorem is included as a milestone. The source is Grünbaum, Convex Polytopes, second edition, Springer, 2003, §5.1, Theorem 10, printed page 74 (source.pdf page 100); see also §5.1, printed page 71 (PDF page 97), for the section convention.

Recognizing a convex set from its projections

A convex set can be studied through its images in spaces of smaller dimension. Each image records part of the geometry, while losing the information along the directions that are collapsed. A finite convex hull always has finite convex hulls as its affine images. The converse asks whether sufficiently rich projection data can force the original set to have a finite description by points. This mission concerns the recognition theorem attributed to Klee in Grünbaum's Convex Polytopes, §5.1, Theorem 8, printed page 74.

The question concerns all projections into a suitable dimension, rather than an individual view of a set. A single image may conceal directions in which the original set has additional structure. The theorem identifies a condition on the entire family of images that characterizes polytopes among bounded convex sets.

Sets, convex hulls, and affine projections

Fix an integer $d\geq3$. Real coordinate space $\mathbb R^d$ consists of vectors with $d$ real coordinates. A set $K\subseteq\mathbb R^d$ is convex if it contains the line segment joining any two of its points. It is bounded if its points remain within some finite distance of the origin. Neither condition requires $K$ to fill the ambient space.

The convex hull of a set $V$, written $\operatorname{conv}(V)$, is the smallest convex set containing $V$. A polytope is the convex hull of a finite set. The generating set need not be a minimal set of vertices. Grünbaum gives this characterization in §3.1, printed page 31. The empty generating set is permitted, as are generating sets contained in a proper affine subspace.

An affine map preserves affine combinations. A surjective affine map $f:\mathbb R^d\to\mathbb R^j$ has a $j$-dimensional target and reaches every point of that target. When $j<d$, such a map loses dimensions. This represents the singular affine images called projections in §5.1, printed page 71, with coordinates chosen on the target affine space. Translation of the target is allowed.

The recognition target

For every bounded convex set $K\subseteq\mathbb R^d$, the goal is the equivalence

$$K\text{ is a polytope} \quad\Longleftrightarrow\quad \exists j\in\mathbb N,\quad 2\leq j<d,\quad \forall f:\mathbb R^d\twoheadrightarrow\mathbb R^j\text{ affine},\quad f(K)\text{ is a polytope}.$$

The dimension $j$ may depend on $K$, but it is chosen before testing the affine maps. Every surjective affine map with that target dimension is tested. For each such map, the finite set generating the image can be different. No common set of projected vertices or uniform bound on the number of generators is required.

This is one recognition theorem, containing both implications. The selected source grouping does not introduce separate supporting theorem targets.

What the criterion establishes

The theorem characterizes a global finite convex-hull property through lower-dimensional images. In particular, the conclusion concerns the original set itself; it does not merely assert that its closure has a finite generating set. This distinction matters because boundedness and convexity alone do not assert closedness.

The result is a known mathematical theorem in the source. The formalization target is its complete equivalence with the stated domain and quantifier order. A proof of only the preservation of polytopes under affine maps would leave the recognition implication unresolved.

Why the converse requires more than one image

Every tested image can have its own finite generating set. Finiteness of each image does not directly supply a finite generating set that works in the original ambient space. The recognition implication must connect the universal family of images to the geometry of the whole set. Replacing that family by a convenient fixed projection would change the question.

Mathematical conventions

Real $d$-space is represented by functions from Fin d to the real numbers. Boundedness and convexity use the ordinary Mathlib predicates, and being a polytope is expressed directly by existence of a finite set with the specified convex hull. No full-dimensional polytope structure is imposed on $K$.

The hypothesis $d\geq3$ makes explicit the admissible ambient dimension needed for $2\leq j<d$. In dimension three, the only available target dimension is two. No assertion of the displayed existential criterion is made in dimensions zero, one, or two. Empty sets, singleton sets, and other lower-dimensional subsets remain within the domain in every admissible ambient dimension.

Affine maps are required to be surjective onto the selected coordinate space. Thus their rank is exactly the selected target dimension, rather than an accidentally smaller rank. Closedness, nonemptiness, rational coordinates, and a predetermined number of vertices are not additional hypotheses. The mathematical ingredients are real convex hulls, finite sets, bounded sets, and affine images.

Selected references

Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003. Theorem 5.1.8, printed page 74 (source.pdf page 100); projection convention, printed page 71 (PDF97); polytope convention, printed page 31 (PDF51). The source pages are included in this package's evidence directory.

Binary choices and polyhedral complexity

A vector whose coordinates are all zero or one records a collection of yes-or-no choices. Taking the convex hull of a collection of these vectors gives a 0/1-polytope, also called a binary polytope. Such objects connect discrete choices with geometry: points describe feasible combinations, while supporting inequalities describe restrictions that every feasible combination satisfies. Grünbaum's discussion in §4.9 emphasizes the role of facets of these polytopes in combinatorial optimization and cutting-plane descriptions.

The question here concerns how many facets can occur when the dimension grows. Restricting every generating point to binary coordinates gives a finite, highly structured collection of possible points. Nevertheless, this restriction still allows polytopes with very many distinct boundary faces. The theorem of Bárány and Pór establishes superexponential growth in the largest possible number of facets. The mission concerns the form of this growth asserted in Grünbaum's 2003 notes, printed page 69a, rather than a prescribed numerical constant.

Polytopes, dimension, and facets

Fix a natural number d. The ambient space is the real coordinate space R^d. A convex hull consists of all convex combinations of the generating points, meaning weighted averages with nonnegative weights whose sum is one. A polytope is the convex hull of a finite set of points. It is full-dimensional when its affine span is all of R^d; this rules out a polytope lying in a proper affine subspace.

For a binary polytope, every generating point belongs to {0,1}^d. A subset of this cube is automatically finite. Nonemptiness and full dimension are imposed separately in the target. Consequently, the dimension in the facet bound is the actual dimension of the polytope as well as the dimension of its coordinate space.

An exposed face is the set of all points of the polytope that maximize a given linear functional. A facet is a face of affine dimension d−1. Facets are counted as geometric sets. Two different inequalities that expose the same face do not contribute two facets. Write f_(d−1)(P) for this number.

The growth target

The target is the following existence statement:

$$\exists c>1\;\exists D\in\mathbb N,\ D\ge2,\quad \forall d\ge D\;\exists P\subseteq\mathbb R^d,\quad P\text{ is a full-dimensional binary polytope},\qquad f_{d-1}(P)>c^{d\ln d}.$$

The constant c and threshold D are chosen before the dimension d. The polytope P may depend on d. The assertion therefore supplies a witness in every sufficiently large dimension. It does not merely assert the existence of one complicated polytope or of witnesses along an unspecified subsequence.

The logarithm is natural. Replacing it by another fixed base greater than one changes the admissible constant c, while preserving the shape of the theorem. The statement leaves both c and D unspecified. The Bárány–Pór paper, Theorem 1.1, supplies the asymptotic context for the book's formulation.

What superexponential growth says

For any fixed c greater than one, the expression c^(d ln d) eventually exceeds A^d for every fixed A greater than one. Thus a single exponential base cannot bound the facet counts of all binary polytopes across dimensions. The binary-coordinate restriction alone does not yield that kind of uniform bound.

The underlying mathematical result is established in the literature. The formalization task is to prove its stated existence conclusion with the precise geometric definitions above. The conclusion concerns actual facets of actual polytopes, so a family of redundant inequalities or a list with repetitions would not satisfy the counting requirement.

Why the existence statement is demanding

A large supply of binary points does not by itself identify the supporting hyperplanes of their convex hull. Counting points and counting facets are different tasks. Moreover, the theorem requires the same growth constant across all sufficiently large dimensions. Verifying individual examples, even examples with many facets, leaves that uniform asymptotic requirement unresolved.

The book describes certain random polytopes as witnesses. Its stated conclusion gives no probability distribution or numerical probability bound. The target records the resulting extremal existence assertion; it imposes no extra probabilistic hypothesis on the witness.

Geometric conventions

The coordinate model is Fin d → ℝ. IsDPolytope requires a nonempty finite convex hull with full affine span. IsZeroOnePolytope specifies the hull of binary-coordinate points. faceCount P k counts nonempty exposed faces with affine dimension k. These concrete notions also apply to other questions about finite-dimensional polytopes.

Face counts use natural cardinality. On the domain of finite polytopes there are only finitely many faces, so this is the ordinary finite count. Requiring D at least two ensures that d−1 represents the facet dimension without a low-dimensional subtraction convention and that the logarithm's argument is positive. Full dimension excludes the whole polytope from the facet count, and nonemptiness excludes the empty face.

Selected references

• Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003, §4.9, printed p.69a; definitions in §§2.4 and 3.1. Book.
• Imre Bárány and Attila Pór, On 0-1 Polytopes with Many Facets, Advances in Mathematics 161 (2001), 209–228, Theorem 1.1. Paper.

A convex polytope has both geometric coordinates and a finite pattern of faces. Moving its vertices can change distances and angles while preserving which vertices belong to which faces. Enumeration by combinatorial type asks for those incidence patterns, with geometrically different realizations of the same pattern counted together. Grünbaum’s enumeration theorem establishes that the complete collection can be determined algorithmically when the dimension and number of vertices are prescribed Convex Polytopes, §5.5, p.91.

A d-polytope here is a nonempty convex hull of finitely many points in real d-dimensional coordinate space, with affine span equal to the whole space. A face is obtained by maximizing a linear functional over the polytope; the collection of faces also includes the empty face and the polytope itself. Inclusion orders this collection. Two polytopes have the same combinatorial type when their full face collections admit an order isomorphism. This notion retains the incidence structure and forgets metric measurements.

To describe a type with finite data, label the k vertices by the integers from zero through k−1. Record the set of vertex labels belonging to each nonempty proper face. This family of subsets is the polytope’s scheme. A finite list of finite lists of natural numbers encodes such a family. The order of labels and repeated occurrences of a label do not change the represented subset. A scheme is realized only when its recorded subsets are exactly the vertex sets of the nonempty proper faces: it cannot add faces, omit faces, or introduce labels outside the prescribed range.

The target is a single total computable function

$$E : \mathbb N\times\mathbb N\longrightarrow \operatorname{List}(\operatorname{List}(\operatorname{List}(\mathbb N))).$$

For every dimension d and vertex count k, each scheme in E(d,k) must have a realizing d-polytope with exactly k vertices. Every d-polytope with k vertices must realize some scheme in that output. Finally, if polytopes realizing two output positions have isomorphic full face posets, those positions must be equal. These requirements say that the output contains precisely one representative of every combinatorial type. The existential choice of one function precedes both numerical inputs, so the algorithm must work uniformly for all dimensions and vertex counts.

The result supplies an effective finite classification at each prescribed size. It is stronger than the observation that only finitely many incidence families can be written down: those families need not all arise from real convex polytopes. It also addresses termination, since a total algorithm must return its entire finite answer for every input. The theorem is a known mathematical result in the cited textbook. The present formal target asks for a proof of its stated algorithmic conclusion; no machine-checked proof of that conclusion is asserted here.

The principal difficulty is the connection between finite incidence data and geometric realizability. Combinatorial consistency alone does not supply real coordinates for a convex polytope. The source distinguishes this realizability question from the enumeration conclusion and identifies decidability over the real numbers as relevant to it §5.5, p.91. The mission retains the complete enumeration conclusion, including realizability of each answer, coverage of every type, and absence of duplicate types.

The formal representation uses real coordinates without a rationality restriction and permits nonsimplicial polytopes. Vertices are labelled injectively and exhaustively. The number of vertices is expressed as the number of nonempty zero-dimensional exposed faces. Nonemptiness separates the empty face, whose book dimension is −1, from the natural-valued dimension used to count faces. For finite convex hulls the face collections are finite, so this cardinality has its usual meaning.

Natural-number dimensions include dimension zero. The unique point has one vertex and no nonempty proper faces, and therefore uses an empty scheme. This is an explicit extension of the source’s positive-dimensional scheme convention. Unrealizable dimension and vertex-count pairs require an empty output. Finite-polytope faces, their ordered collection, vertex counts, and finite scheme realizations are the concrete objects needed to state the goal; total computability applies to the complete finite output rather than to individual tests alone.

Reference: Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003, §5.5, Theorem 2 (5.5.2), printed p.91, PDF p.117; definitions in §§2.4 and 3.1. Source text.