How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Finite convex cell complex and linear subdivision
Definition
A compact convex polyhedral cell is a nonempty bounded set in a finite-dimensional Euclidean affine subspace given by finitely many affine inequalities . It is closed, hence compact by Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line in positive ambient dimension; in dimension zero it is a singleton. A face is the empty set, the cell itself, or its intersection with a supporting hyperplane where on the cell. Equivalently, every nonempty face arises by turning some of the defining inequalities into equalities; this equivalence is proved in the face calculus below.
A finite convex cell complex is a finite family of such cells and the empty cell, containing every face of each cell, such that the intersection of any two cells is a face of each. Its underlying set is the union of its cells. A finite linear simplicial complex is one whose cells are geometric simplices. Its topology is the Euclidean subspace topology; for a finite abstract complex it agrees by Finite simplicial weak topology agrees with euclidean topology with its realization topology from The geometric realization of an abstract simplicial complex.
A linear subdivision of a finite convex cell complex is a finite linear simplicial complex with the same underlying set and with every new simplex contained in an old cell. A subdivision on a subcomplex is compatible if it is precisely the restriction of the new triangulation. Zero-dimensional cells are singletons, whose only proper face is empty. The empty complex here means the family consisting only of the empty cell. These are convex polyhedral cells, not general CW cells.
Source locators
Chapter 2, Cells and Cell Complexes, pp.13–15.
Depends on
The geometric realization of an abstract simplicial complex
Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line
Finite simplicial weak topology agrees with euclidean topology