Convex Polytopes

Motivation

Convex hulls are often defined using arbitrary finite convex combinations. In finite dimensional geometry, Carathéodory's theorem gives a uniform bound on how many points are needed to represent any one point of the hull. This is the finite representation result stated in Branko Grünbaum's Convex Polytopes, second edition (2003), §2.3, Theorem 2.3.5, printed page 15 (PDF page 33). It matters when one wants a description whose number of witnesses depends on the ambient dimension rather than on the size of the generating set. The mission concerns that exact textbook statement for an arbitrary subset of real coordinate space.

Setting

Fix a natural number $d$. The ambient space $\mathbb R^d$ is represented in Lean as Fin d → ℝ: a point assigns a real coordinate to each of the $d$ indices. Let $A$ be any set of such points. Its convex hull, written $\operatorname{conv}(A)$ in the book and convexHull ℝ A in Lean, is the smallest convex set containing $A$. A convex combination is a finite weighted sum of points of $A$ whose real weights are nonnegative and total one. No finiteness, closedness, boundedness, convexity, or nonemptiness assumption is imposed on $A$.

The witnesses in the target are indexed by Fin (d + 1), which has exactly $d+1$ elements, corresponding to the book's indices $0,\ldots,d$. Repeated points and zero weights are permitted. They allow a representation that uses fewer than $d+1$ distinct points to be written with the same fixed index type.

Formalization targets

Theorem 2.3.5: Carathéodory's finite convex representation

For every $x\in\operatorname{conv}(A)$, find points $x_0,\ldots,x_d\in A$ and real numbers $\alpha_0,\ldots,\alpha_d\geq 0$ such that

$$\sum_{i=0}^{d}\alpha_i=1, \qquad x=\sum_{i=0}^{d}\alpha_i x_i.$$

The Lean goal is Grunbaum2003.caratheodory_convex_representation. It quantifies over every natural dimension, every set $A$ in that real coordinate space, and every point $x$ of its convex hull. The existential witnesses and all four required clauses are part of one theorem. This is the sole goal and sole source obligation in the frozen mission grouping; there is no separate supporting milestone to attest.

Significance

The result turns membership in a convex hull into a representation with a dimension controlled number of generators. The bound is independent of the cardinality of $A$, which may even be infinite. In the textbook's chapter, this is the finite representation model from which other discussions of convex sets can proceed. It does not itself claim a separation theorem, a compactness statement about closures, or a representation of unbounded closed convex sets using recession directions; those are distinct statements with different hypotheses and conclusions.

A formal proof of this statement would establish the textbook result in Lean for the exact source quantifiers and index bound. The present proposal contains a statement with sorry, not a proof. The original statement compiled in the local Lean workspace and passed source aware moderation; successful compilation verifies that its expression is well formed but does not settle the theorem. The open work in this mission is to replace the placeholder with a machine checked proof of the stated result.

Difficulty

The definition of convexHull ℝ A establishes membership by finite convex combinations, but such a combination can have arbitrarily many terms. The target asks for a bound of $d+1$ terms, uniformly for every point and every generating set. Merely unfolding convex hull membership therefore does not deliver the claimed index bound. The witness must also keep membership in $A$, nonnegative coefficients, normalization, and the exact vector equality simultaneously. These constraints explain why a general finite combination cannot simply be relabelled as a Fin (d + 1) family.

Formalization scope

The representation uses real scalars and the coordinate space Fin d → ℝ. The Lean statement uses convexHull ℝ A for the hull, Fin (d + 1) for both point and weight families, and a finite sum for normalization and the represented point. d = 0 is included. When $A$ is empty, the hypothesis $x\in\operatorname{conv}(A)$ has no instance; no artificial nonemptiness premise is added. There is no extra affine independence or strict positivity condition on the witnesses.

The only expression dependencies are Mathlib's convex hull, real numbers, finite indexing, finite sums, and scalar multiplication. The proposal does not introduce a duplicate convex hull definition or a book specific representation predicate. A complete proof may use Mathlib's existing convexity library, but the theorem statement and its source obligations remain fixed. Contributions that prove the exact quantified statement are within scope; variants with a restricted $A$, a changed ambient space, or fewer clauses would answer a different question.

Selected references

• Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003, §2.3, Theorem 2.3.5, printed p. 15, PDF p. 33. Publisher record. Source copy: source.pdf in the book record; SHA-256 070befaa8c47f043ef9da1df0705910480eb692f044d1843c9f048f3e61fecac.

Motivation

A polytope can be represented not only by vertices or supporting inequalities, but also as a section of a simplex in a higher-dimensional space. Perles's prescribed-point theorem strengthens this representation: the cutting flat can be required to pass through an interior point selected in advance. This is Theorem 5.1.10 in Branko Grünbaum's Convex Polytopes, second edition, §5.1, printed p. 74. The result isolates how a bound on the number of facets controls the dimension of a universal simplex while retaining freedom to prescribe a point in the section.

Setting

Fix natural numbers $d$ and $k$. A $d$-polytope $P\subseteq\mathbb R^d$ is represented here as a nonempty convex hull of finitely many points whose affine span is all of $\mathbb R^d$. A face is the complete maximizing locus of a supporting linear functional, and a facet is a nonempty face of affine dimension $d-1$. The quantity used in the target counts geometric faces, not the number of inequalities in a chosen description.

A $k$-simplex is the convex hull of $k+1$ affinely independent points $v_0,\ldots,v_k$ in $\mathbb R^k$. Write this simplex as $T$. Affine independence makes $T$ full-dimensional, so $\operatorname{int} T$ is its ordinary ambient interior. No regularity, coordinate normalization, or metric condition is imposed on $T$. A $d$-flat is a translate of a $d$-dimensional linear subspace. Its section of $T$ is the whole intersection $T\cap L$.

Two subsets are affinely equivalent when an affine bijection between their affine spans maps one set exactly onto the other. Distances and angles need not be preserved. In the formal statement this equivalence is witnessed by an injective affine map $A:\mathbb R^d\to\mathbb R^k$ whose range is $L$ and whose image of $P$ equals $T\cap L$.

Formalization target

The single target is the prescribed-point section theorem:

$$\begin{aligned} &P\subseteq\mathbb R^d\text{ is a }d\text{-polytope with at most }k+1\text{ facets},\\ &T\subseteq\mathbb R^k\text{ is a }k\text{-simplex},\quad p\in\operatorname{int}T\\ &\qquad\Longrightarrow\quad \exists\text{ a }d\text{-flat }L\subseteq\mathbb R^k:\ p\in L \text{ and }T\cap L\cong_{\mathrm{aff}}P. \end{aligned}$$

Grünbaum writes the number of allowed facets as $f$ and uses an $(f-1)$-simplex in $\mathbb R^{f-1}$. The Lean statement sets $f=k+1$. Every input, including the simplex and its interior point, is universally quantified before $L$ and $A$ are chosen. Thus the witnesses may depend on all the input data, but neither the simplex nor the prescribed point may be chosen to suit $P$.

Significance

The theorem gives a controlled simplex-section representation for every polytope with a bounded number of facets. Its prescribed-point clause is stronger than merely asserting that some section somewhere is affinely equivalent to $P$: it permits the ambient simplex and any one of its interior points to be fixed first. The equality $A(P)=T\cap L$ also covers the entire section, excluding a weaker containment statement.

This is a known theorem, not an open conjecture. The package supplies a source-reviewed, compiling Lean statement with a proof placeholder. A complete contribution would replace that placeholder by a machine-checked proof while preserving the facet bound, the arbitrary-simplex quantifier, the prescribed point, the flat dimension, and the exact affine-equivalence conclusion.

Difficulty

A flat chosen only to pass through $p$ may cut out the wrong affine shape, while a flat producing the correct shape need not contain the prescribed point. The theorem requires both conditions simultaneously for every allowed simplex and every interior point. Restricting to a regular simplex, moving the chosen point, or proving only an unrestricted section representation would lose essential quantifiers from the source statement.

The facet allowance also refers to geometric facets rather than a particular inequality presentation. A formal proof must therefore connect the combinatorial boundary data of $P$ with the geometry of the simplex section without replacing the source hypothesis by a representation-dependent count.

Formalization scope

Lean represents $\mathbb R^d$ by Fin d → ℝ. Grunbaum2003.IsDPolytope requires a finite nonempty convex-hull presentation and full affine span. Grunbaum2003.faceCount P r is the finite cardinality of nonempty exposed faces whose affine-span direction has dimension $r$. For $d>0$, the hypothesis uses faceCount P (d - 1). For $d=0$, the formal statement makes the facet allowance automatic; this avoids natural-number underflow while retaining the zero-dimensional source case.

The simplex is convexHull ℝ (Set.range v) under AffineIndependent ℝ v, and interior is ambient interior. The witness L is an affine subspace containing $p$ with direction dimension $d$. The affine map is injective, has range exactly $L$, and maps all of $P$ onto the full intersection. These conventions rule out degenerate simplices, lower-dimensional input polytopes, containment-only conclusions, and vacuous facet counts.

The two definition files are expression-essential and shared with other missions in this textbook series. No proof-only theorem is packaged, and there is no separate reviewed source lemma to list as a milestone.

Selected references

• Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003, §5.1, Theorem 5.1.10, printed p. 74; section convention printed p. 71. DOI.

A convex set contains the segment joining any two of its points. For a bounded closed convex set in finite-dimensional real space, extreme points describe the set through convex combinations. An extreme point cannot lie strictly between two distinct points of the set. Allowing unbounded sets introduces a second ingredient: directions in which one can move indefinitely while remaining in the set.

This mission concerns that second ingredient and its interaction with extreme points. A closed convex set is line-free if it contains no entire straight line. It may nevertheless contain rays and be unbounded. Its characteristic cone consists of directions v for which x + t v stays in the set whenever x belongs to the set and t is nonnegative. For a nonempty closed convex set, checking one basepoint gives the same cone as checking every basepoint. Thus the cone records the directions of recession without singling out an origin inside the set.

The goal is Grünbaum’s Theorem 2.5.6:

$$K = \operatorname{cc} K + \operatorname{conv}(\operatorname{ext} K)$$

for every line-free, closed convex set K in real d-dimensional space. The plus sign denotes Minkowski addition: all sums of one point from each set. The equation says that every point of K is a recession vector plus a finite convex combination of extreme points. Conversely, each such sum belongs to K. There is no topological closure around the convex hull in this equation.

A ray illustrates the two ingredients. Its endpoint is its only extreme point, while its characteristic cone supplies every nonnegative displacement along the ray. A singleton has only itself as an extreme point and has zero characteristic cone. A whole straight line shows why the line-free hypothesis matters: it has no extreme points and cannot be recovered from their convex hull by this formula.

The ambient dimension is arbitrary and finite; the set need not be full-dimensional or polyhedral. The characteristic cone is defined using all basepoints, so its value on the empty set is the whole ambient space. Since the empty set has no extreme points, its convex hull and the displayed Minkowski sum are empty, and the equation remains valid. This convention extends the formula without asserting that the book defines a characteristic cone at an absent basepoint.

The source is Branko Grünbaum, Convex Polytopes, second edition (2003), §2.5, Theorem 6, printed page 25 (PDF page 43). The characteristic cone and line-free condition appear on printed page 24 (PDF page 42); extreme points are defined in §2.4 on printed page 17 (PDF page 35). These definitions supply the vocabulary for the single representation goal.

Finite representations in convex geometry

A convex combination expresses a point as a weighted average of other points. Such representations connect geometric sets with finite lists of coordinates and coefficients. A point in a convex hull may initially be described using many generators, even when the ambient space has small dimension. Carathéodory's theorem gives a bound depending only on that dimension. Grünbaum presents this result as a basic theorem of convexity in Convex Polytopes, §2.3, Theorem 5, printed page 15 (the supplied source PDF, page 33).

Sets, points, and weights

Fix a natural number $d$. Real $d$-space consists of vectors with $d$ real coordinates. Let $A$ be any subset of this space. A convex combination of points of $A$ is a finite sum of those points multiplied by nonnegative real coefficients, with the coefficients adding to one. The convex hull $\operatorname{conv} A$ is the set of all such combinations; equivalently, it is the smallest convex set containing $A$.

The generating set $A$ can be finite or infinite. It need not be closed, bounded, or convex. Membership of a point $x$ in its convex hull is the sole geometric assumption. The theorem concerns exact equality of vectors, so the representation is not an approximation or a limiting expression.

A dimension bound for every hull point

For every $x\in\operatorname{conv} A$, find points $v_0,\ldots,v_d\in A$ and real numbers $w_0,\ldots,w_d$ satisfying

$$w_i\geq 0\quad(0\leq i\leq d),\qquad \sum_{i=0}^{d}w_i=1,\qquad x=\sum_{i=0}^{d}w_i v_i.$$

This is the complete target of Theorem 2.3.5. The witnesses may depend on $d$, $A$, and $x$. No single selection of points must work for every point of the hull. Repeated points are permitted, and some coefficients may be zero. Thus the fixed list of $d+1$ positions can express a combination that uses fewer distinct points.

What the representation provides

The result gives a finite certificate for membership in a convex hull whose length is controlled by dimension rather than by the size of the generating set. In the plane it gives three positions, and in three-dimensional space it gives four. Infinite generating sets remain within the same statement: once a particular hull point is chosen, only finitely many generators are needed for its certificate.

The mission asks for a formal proof of this known mathematical result in its fixed-length formulation. Its content is the existence of points and normalized coefficients together. Supplying coefficients without ensuring that their points lie in $A$, or supplying a finite representation without the dimension bound, would leave part of the target unestablished.

The constraint that must be met

The definition of the convex hull guarantees a finite representation but does not directly fix its length at $d+1$. The dimension bound must hold while preserving nonnegativity, normalization, membership in the original generating set, and exact equality with the selected point. None of these constraints can be replaced by a condition on nearby points or on the closure of $A$.

Scope and boundary conventions

The coordinate model is Fin d → ℝ. Both the point list and the coefficient list are indexed by Fin (d + 1), corresponding to the source indices from zero through $d$. The convex hull, finite sums, and real scalar multiplication have their standard mathematical meanings. No additional geometric definition is needed.

Dimension zero has one position in the representation. If $A$ is empty, its convex hull is empty, so there is no hull point to represent. A singleton generating set and sets contained in a proper affine subspace are allowed. Neither strict positivity of the weights nor affine independence of the selected points is required. The target does not assert uniqueness of a representation.

Selected reference

Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003, Chapter 2, §2.3, Theorem 5, printed page 15; supplied source.pdf, page 33.