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.