Discrete Geometry

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

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

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.