SimplicialComplex
plain-language theorem explainer
For each size cap B, the simplicial complexes are the subtype of bounded incidence configurations that satisfy the four simplicial conditions (no degenerate edges, no multi-edges, four distinct tet vertices, skeleton closure). Gravity path-sum work cites this as the honest configuration space for the restricted sum Zsimp. The declaration is a one-line subtype abbreviation over BoundedComplex and IsSimplicial.
Claim. For each natural number $B$, write $\mathrm{SimplicialComplex}(B)$ for the type of pairs $(K,h)$ where $K$ is a bounded incidence configuration of cap $B$ and $h$ asserts that $K$ is simplicial: edges have distinct endpoints, edges are unique as unordered pairs, every tetrahedron has four distinct vertices, and every vertex pair of every tetrahedron appears as an edge.
background
The ambient object is the bounded path-sum configuration class: for a size cap $B$, a bounded complex packages finite vertex, edge, and tetrahedron lists with length bounds. That superclass is deliberately garbage-inclusive. It admits degenerate edges, multi-edges, repeated tet vertices, and tets whose 1-skeleton is missing from the edge list.
This module carves out the true simplicial subclass by a decidable predicate with four combinatorial clauses: (1) no degenerate edges; (2) no multi-edges (injectivity on unordered vertex pairs); (3) four distinct vertices per tetrahedron; (4) skeleton closure (every tet edge is present). Face (triangle) data is not carried by the bounded-complex shape, so triangle closure is out of scope by design.
The local setting is Full Theory Phase 0b for the gravity path sum: restrict the configuration space before writing the restricted measure and the UV bound on the sum.
proof idea
Definitional abbreviation only. The type is the subtype of bounded complexes of cap $B$ whose carrier satisfies the simplicial predicate. No proof obligations live on the abbreviation itself; finiteness, positivity, and witnesses are proved on the subtype in sibling declarations (Fintype instance via subtype finiteness plus decidability, empty complex, one-tetrahedron witness).
why it matters
This type is the configuration space for the restricted path sum: the sum over simplicial complexes with the same $1/|\mathrm{Aut}|$ measure and weight as the unrestricted sum. Downstream, the Fintype instance and positive cardinality give a nontrivial finite space for every cap; the one-tetrahedron witness shows positivity is not vacuous for $B\ge 6$. The UV-finiteness theorem then bounds the restricted sum by the simplicial configuration count for unit-modulus weights.
In the Seven Gaps gravity program this is the honest combinatorial cut between garbage-inclusive incidence data and abstract simplicial 3-complexes presented by tets and 1-skeleton. It does not touch the forcing chain (T0–T8) or the Recognition Composition Law directly; it supplies the discrete geometry layer on which a finite path-sum measure can sit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.