Discrete Geometry

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

Ellipsoids are the simplest convex bodies that can approximate an arbitrary convex set to within a factor depending only on the dimension. They are used for exactly that in control (reachable sets of linear systems), robust optimization (uncertainty sets) and the ellipsoid method. A linear system $x(t+1)=Ax(t)+Bu(t)$ with $\|u(t)\|_2\le1$ illustrates the need. Its reachable set grows by an arithmetic sum at every step, so an ellipsoidal description of it requires approximating a sum of ellipsoids by a single ellipsoid, recursively and cheaply.

Timeline. Fritz John (1948) proved that every convex body has a unique maximal-volume inscribed ellipsoid and a unique minimal-volume circumscribed one, each within a factor $n$ ($\sqrt n$ for symmetric bodies) of the body; the circumscribed case goes back to Löwner. Boyd, El Ghaoui, Feron and Balakrishnan (1994) gave semidefinite programs whose solutions are ellipsoids that provably contain a sum of ellipsoids. Nesterov (1998) and Ye (1999) proved a $\pi/2$ approximation bound for semidefinite relaxations of quadratic maximization with commuting constraint matrices. Ben-Tal and Nemirovski (2001), Lecture 4, §4.9, combine the last two: the semidefinite outer ellipsoid of a sum of ellipsoids has volume at most $(\pi/2)^{n/2}$ times that of the smallest one.

Setting

All objects live in $\mathbb R^n$, with $u^Tu=\sum_ju_j^2$.

• An ellipsoid is a set $E(A,c)=\{Au+c \mid u^Tu\le1\}$ with $A\in\mathbb R^{n\times q}$. It is full-dimensional if it can be written with $A$ square and $\operatorname{Det}A\ne0$.
• Volume is normalized: $\operatorname{Vol}(G)$ is the Lebesgue measure of $G$ divided by that of the unit Euclidean ball. Then $\operatorname{Vol}(E(A,c))=|\operatorname{Det}A|$ and $\operatorname{Vol}(W[Z])=(\operatorname{Det}Z)^{-1/2}$, where $W[Z]=\{x \mid x^TZx\le1\}$ for $Z\succ0$.
• A solid is a closed, bounded, convex set with nonempty interior.
• Fix positive definite $B_1,\dots,B_m$ and the centred ellipsoids $W_i=W[B_i]$. Their arithmetic sum is $W=W_1+\dots+W_m=\{w_1+\dots+w_m \mid w_i\in W_i\}$.
• Let $B^i$ be the $(mn)\times(mn)$ block-diagonal matrix whose only nonzero $n\times n$ diagonal block is the $i$-th, equal to $B_i$. Let $M[Z]$ be the $(mn)\times(mn)$ matrix of $m^2$ blocks, all equal to $Z$.
• The semidefinite program

$$\max_{t,Z,\lambda}\Big\{t \;\Big|\; t\le\operatorname{Det}^{1/n}(Z),\ \sum_{i=1}^m\lambda_iB^i\succeq M[Z],\ \lambda\ge0,\ Z\succeq0,\ \sum_{i=1}^m\lambda_i=1\Big\}\qquad(\tilde O)$$

produces, from each feasible solution with $t>0$, an ellipsoid $W[Z]\supseteq W$.

Formalization targets

Goal: Proposition 4.9.5

Let $(t_*,Z_*,\lambda_*)$ be any optimal solution of $(\tilde O)$. Let $Z_{**}\succ0$ be such that $W[Z_{**}]$ is the smallest-volume full-dimensional ellipsoid containing $W$. Then

$$\operatorname{Vol}(W[Z_*])\le\Big(\frac\pi2\Big)^{n/2}\operatorname{Vol}(W[Z_{**}]).$$

This is the book's ratio $\vartheta=\operatorname{Vol}(W[Z_*])/\operatorname{Vol}(W[Z_{**}])\le(\pi/2)^{n/2}$ in product form.

Milestones

1. (D): if every $X\succeq0$ with $\operatorname{Tr}(B^iX)\le1$ for all $i$ has $\operatorname{Tr}(M[Z]X)\le1$, then $W\subseteq W[Z]$.
2. Proposition 4.9.4: feasible solutions of $(\tilde O)$ with $t>0$ give $Z\succ0$, $W\subseteq W[Z]$ and $\operatorname{Vol}(W[Z])\le t^{-n/2}$. Optimal solutions give the smallest such volume.
3. Proposition 4.10.5 (Nesterov–Ye): for commuting $B_i$, strictly feasible constraints $x^TB_ix\le d_i$ and $A\succeq0$, the semidefinite value satisfies $F^*\le\frac\pi2f^*$, and the dual is solvable.
4. Theorem 4.9.1 (Löwner–Fritz John) for solids, both the inscribed and the circumscribed ellipsoid, with factors $n$ and $\sqrt n$.
5. Proposition 4.9.3: containment of $E(Z,z)$ ($Z\in\mathbb R^{n\times q}$, $q\ge1$) in a full-dimensional ellipsoid is equivalent to a linear matrix inequality in one scalar.
6. Lemma 4.9.1: $|\operatorname{Det}(S+C)|\ge\operatorname{Det}S$ for $S\succ0$ and $C$ skew-symmetric.
7. Proposition 4.9.6: the inner program $(\tilde I)$ gives ellipsoids contained in $W$ of volume at least $t^n$. Optimal solutions give the largest such volume.

Significance

The goal is a quantitative guarantee for a tractable surrogate. Computing the smallest ellipsoid containing a sum of ellipsoids is believed hard when $m$ is part of the input. A single semidefinite program gives an ellipsoid within a factor $\sqrt{\pi/2}\approx1.253$ in average linear size, uniformly in $n$ and $m$. The reachable-set recursion of the motivating example therefore loses at most a fixed factor per step. Proposition 4.10.5 is also the textbook instance of a constant-factor semidefinite relaxation bound for quadratic maximization, used well beyond this chapter.

All results are proved in the book, except Theorem 4.9.1 (Exercise 4.71) and Proposition 4.10.5 (Exercise 4.58 from Exercise 4.38). Some ellipsoid results already exist as Lean statements on Prove2Me, in the Boyd–Vandenberghe convex optimization series: existence, uniqueness and $1/n$-rounding of the Löwner–John ellipsoid of a finite point set. None of the statements here is formalized there. In particular, nothing exists for general solids, the inscribed ellipsoid, the $\sqrt n$ symmetric factor, sums of ellipsoids, or the Nesterov–Ye bound.

Difficulty

The goal's statement is short, but its proof crosses several fields. The obvious idea, comparing $W[Z_*]$ with $W[Z_{**}]$ directly, fails: $W[Z_{**}]$ is in general not of the form produced by $(\tilde O)$, since $(\tilde O)$ only reaches ellipsoids certified by a semidefinite relaxation. Closing that gap requires the full Nesterov–Ye bound $\pi/2$ for a quadratic maximization over the product of the $W_i$. That bound is itself a substantial theorem, which the book proves only through a chain of exercises. Mathlib has volumes, determinants and positive semidefinite matrices. It has no Löwner–John theory for convex bodies, no Schur-complement LMI calculus for block matrices over sum types, and no semidefinite duality.

The book's Proposition 4.9.6 is false as printed. Its constraint $t\le(\operatorname{Det}\cdot)^{1/n}$ admits every $t\le0$. For $n=2$, $A_1=I$, $X_1=0$, $t=-10$, the ellipsoid is $\{0\}$ while $t^n=100$. A corrected variant adds $t\ge0$.

Formalization scope

Vectors are Fin n → ℝ, and matrices are Matrix (Fin n) (Fin q) ℝ. $\succeq0$ and $\succ0$ are Mathlib's PosSemidef and PosDef, which include symmetry. The unit ball is written with the dot product, because Mathlib's metric ball on Fin n → ℝ is a cube. Volume is Mathlib's volume divided by the volume of the Euclidean unit ball, valued in $[0,\infty]$, so flat ellipsoids have volume $0$. $\operatorname{Det}^{1/n}$ is Real.rpow. The $(mn)\times(mn)$ block matrices are indexed by Fin m × Fin n. Optimal values appear only as explicit predicates: optimal = feasible with maximal objective, least upper bound, attained minimum.

In the goal, $W[Z_{**}]$ enters through hypotheses: $Z_{**}\succ0$, $W\subseteq W[Z_{**}]$, and no full-dimensional ellipsoid with any centre that contains $W$ has smaller volume. These hypotheses are satisfiable, by Theorem 4.9.1 and the central symmetry of $W$, so the goal is not vacuous. Volume is the measure-theoretic volume, not a formula in $\operatorname{Det}$ assumed as a definition: a formalization that defines the volume of $W[Z]$ as $(\operatorname{Det}Z)^{-1/2}$ for every $Z$ would not be the book's statement.

Two variants accompany the faithful statements. The first, [Corrected] Proposition 4.9.6, adds $t\ge0$, following finding F1. A Lean disproof of the printed statement on the instance above exists locally. The second, [Strengthened] Proposition 4.9.5, drops the minimality of $W[Z_{**}]$ (finding F2): the printed proof uses only $Z_{**}\succ0$ and $W\subseteq W[Z_{**}]$. Proofs of either variant, and disproofs of the printed Proposition 4.9.6, are welcome.

A complete development needs: Lebesgue volume of linear images ($|\operatorname{Det}|$ scaling); Schur complements for symmetric block matrices; semidefinite weak and strong duality, at least for the strictly feasible case; simultaneous diagonalization of commuting symmetric matrices; and the $\pi/2$ relaxation bound itself. The last four are reusable across the series' Lecture 4 missions.

Selected references

• A. Ben-Tal, A. Nemirovski, Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications, SIAM, 2001, §4.9 and §4.10.5. https://doi.org/10.1137/1.9780898718829
• F. John, Extremum problems with inequalities as subsidiary conditions, Studies and Essays Presented to R. Courant, Interscience, 1948, 187–204. https://doi.org/10.1007/978-3-0348-0439-4_9
• S. Boyd, L. El Ghaoui, E. Feron, V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777
• Yu. Nesterov, Semidefinite relaxation and nonconvex quadratic optimization, Optimization Methods and Software 9 (1998), 141–160. https://doi.org/10.1080/10556789808805690
• Y. Ye, Approximating quadratic programming with bound and quadratic constraints, Mathematical Programming 84 (1999), 219–226. https://doi.org/10.1007/s10107980012a