oneTetComplex
plain-language theorem explainer
The single-tetrahedron incidence complex with four vertices, six edges (the complete 1-skeleton of K4), and one tetrahedron, packaged at complexity bound six. Mesh-refinement and Regge-metric arguments in the SevenGaps gravity stack cite it as the minimal non-empty simplicial carrier. The body is a structure literal: bound inequalities by omega/reflexivity, edges from the standard tet edge list, and the unique tet labeled by the identity on Fin 4.
Claim. The single-tetrahedron bounded complex of complexity bound $6$ is the incidence configuration with $n_V=4$ vertices, $n_E=6$ edges, and $n_T=1$ tetrahedron, whose edge-endpoint map is the six unordered pairs of the complete graph $K_4$, and whose unique tetrahedron is the ordered 4-tuple of all vertices.
background
BoundedComplex B (from the path-sum measure layer) is the garbage-inclusive superclass of bounded incidence configurations: vertex, edge, and tetrahedron counts capped by $B$, together with endpoint and corner maps. It admits non-simplicial junk (degenerate edges, multi-edges, tets whose 1-skeleton is missing).
This module carves out the true simplicial subclass via four combinatorial conditions: distinct edge endpoints, no multi-edges as unordered pairs, four distinct tet corners, and skeleton closure (every corner pair realized by an edge). Face/triangle data is not carried, so triangle closure is out of scope.
The single-tetrahedron complex is the explicit non-empty witness at the minimal interesting cap: four vertices, the full six-edge 1-skeleton, one tet. Its edge list is the standard tet edge table (tetEdges); the tet-vertex map is the identity on the four indices.
proof idea
Pure structure definition, not a proof. Fields are set to $n_V=4$, $n_E=6$, $n_T=1$. The three bound obligations ($n_V\le 6$, $n_E\le 6$, $n_T\le 6$) are discharged by omega or le_refl. Edge endpoints are taken from the sibling table of the six $K_4$ pairs; the single tetrahedron is labeled by fun _ i => i, i.e. corners $0,1,2,3$ in order.
why it matters
Module status depends on a non-vacuous simplicial witness so that positivity of the simplicial subclass is not carried only by the empty complex. Downstream, the metric-refinement carrier blocker builds every one-tet decoration on this carrier: unit and double squared-edge metrics, first-edge length, the Cayley-Menger observable $288V^2$ for the Regge API, the quotient class at cap six, and the theorem that one combinatorial class admits two distinct metric decorations. That pair is the concrete mesh blocker: combinatorial quotient data alone cannot fix the metric. In the SevenGaps gravity stack this is the Phase 0b anchor before metric observables and refinement obstructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.