IsSimplicial
plain-language theorem explainer
A bounded incidence configuration is simplicial when edges are non-degenerate and unique as unordered pairs, every tetrahedron has four distinct corners, and every corner pair appears as an edge. Gravity and mesh-refinement arguments cite this to restrict the garbage-inclusive path-sum class to genuine abstract 3-complexes. The body is a pure Prop conjunction of four finite quantifiers over edge and tet indices.
Claim. For a bound $B\in\mathbb{N}$ and a bounded incidence configuration $K$ with $n_E$ edges and $n_T$ tetrahedra, $K$ is simplicial when: (i) every edge has distinct endpoints; (ii) distinct edge indices never realize the same unordered vertex pair; (iii) each tetrahedron map $\mathrm{Fin}\,4\to$ vertices is injective; (iv) for every tet and every pair of distinct corner indices, some edge realizes that unordered pair (1-skeleton closure).
background
Phase 0b of the SevenGaps gravity stack starts from BoundedComplex B, the garbage-inclusive superclass of bounded incidence configurations used by the path-sum measure. That type holds vertex/edge/tet lists with a size cap $B$, but admits degenerate edges, multi-edges, repeated tet corners, and tets whose 1-skeleton is missing from the edge list.
This predicate carves out the combinatorial content of an abstract simplicial 3-complex presented by tetrahedra and 1-skeleton: no loops, simple edges, four distinct corners per tet, and skeleton closure. Face (triangle) data is not carried by the bounded complex, so triangle closure is intentionally out of scope.
Upstream geometry supplies the edge and tet vertex maps (Freudenthal-style incidence tables); the same unordered-pair helper identifies multi-edges. The module proves the predicate decidable on finite index types and builds the subtype of simplicial configurations as a nonempty Fintype.
proof idea
Definitional, not a derived theorem. The body is the four-way conjunction of universal statements over Fin K.nE and Fin K.nT: endpoint inequality; uniqueness of edges up to the unordered-pair relation; injectivity of each tet corner map; and existence of an edge for every distinct corner pair. A sibling DecidablePred instance unfolds the definition and lets Lean infer decidability from finite quantifiers, enabling later decide checks on explicit witnesses.
why it matters
This is the gate that turns the path-sum configuration class into a true simplicial subclass. Downstream, the subtype SimplicialComplex B is exactly configurations satisfying the predicate; empty and one-tetrahedron complexes are proved simplicial, and cap relaxation preserves it definitionally.
Metric refinement builds on it: a metric-decorated complex is a simplicial carrier plus edge/volume data, and the one-tet class is shown to admit two distinct metric decorations over one genuine simplicial carrier of complexity six. Without this filter, mesh-sensitive observables would evaluate on non-complex garbage.
In the Recognition gravity stack this is Phase 0b bookkeeping, not a forcing-chain step (T0–T8). It closes the combinatorial honesty gap recorded in the module status: positivity of the simplicial class does not rest on the empty complex alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.