emptyComplex_isSimplicial
plain-language theorem explainer
For every size bound B, the empty incidence configuration is simplicial: all four simpliciality conditions hold vacuously because there are no edges and no tetrahedra. Path-sum and SevenGaps authors cite it to seed a nonempty simplicial subclass before the one-tetrahedron witness. The proof is a four-goal refine, each discharged by empty-type elimination.
Claim. For every natural number $B$, the empty bounded incidence complex of size cap $B$ satisfies the simplicial predicate: 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
In the SevenGaps path-sum setup, BoundedComplex B is the garbage-inclusive class of bounded incidence configurations (vertex, edge, and tetrahedron lists under a size cap $B$). It admits non-simplicial junk: degenerate edges, multi-edges, repeated tet corners, and tets whose 1-skeleton is missing from the edge list.
The predicate IsSimplicial carves out the true simplicial subclass by four conditions: (1) no degenerate edges, (2) no multi-edges (injectivity on unordered endpoint pairs), (3) injective tetrahedron corner maps, (4) skeleton closure (every corner pair of every tet is realized by an edge). Face/triangle data is not carried, so triangle closure is out of scope.
The empty complex is the configuration with zero edges and zero tetrahedra. This lemma records that it meets IsSimplicial vacuously, which is enough to populate the subtype before a nontrivial witness is built.
proof idea
Term-mode proof via refine on the four conjuncts of IsSimplicial. Each goal is a universal quantifier over Fin K.nE or Fin K.nT for the empty complex, hence over the empty type. Every branch closes by elim0 on the empty index (no edges to check for degeneracy or multi-edges; no tets to check for injectivity or skeleton closure). No combinatorial lemmas are needed.
why it matters
Phase 0b of the full gravity/path-sum theory needs a simplicial subclass that is a Fintype of strictly positive cardinality, so the restricted path sum has a nontrivial configuration space. This lemma discharges the empty complex as a simplicial point and immediately feeds the Nonempty (SimplicialComplex B) instance in the same module.
The module status note is explicit: positivity must not rest on the empty complex alone; the one-tetrahedron complex with full 1-skeleton is the nontrivial witness. Still, the empty case is the cheapest seed for the subtype and for downstream cardinality arguments (simplicialComplex_card_pos). It sits inside the combinatorial cleanup of the path-sum measure, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.