oneTetComplex_isSimplicial
plain-language theorem explainer
The single-tetrahedron incidence configuration (four vertices, six skeleton edges, one tet) satisfies the four simplicial axioms: distinct edge ends, no multi-edges, injective corners, and full 1-skeleton closure. Anyone building metric decorations or non-vacuous positivity of the simplicial subclass cites this witness. The proof is a pure finite `decide` on Fin 4 / Fin 6 / Fin 1 index types.
Claim. The explicit one-tetrahedron bounded complex (four vertices, six edges forming the complete $K_4$ skeleton, one tetrahedron) is simplicial: every edge has distinct endpoints; edges are pairwise distinct as unordered pairs; the tetrahedron map is injective on its four corners; and every unordered pair of those corners is realized by exactly one listed edge.
background
In the SevenGaps path-sum hierarchy, BoundedComplex B is the garbage-inclusive superclass of incidence data (vertex/edge/tet lists with a complexity cap). It admits degenerate edges, multi-edges, repeated tet corners, and tets whose 1-skeleton is missing from the edge list. The module carves out the true simplicial subclass via the predicate IsSimplicial.
That predicate is the conjunction of four combinatorial conditions: (i) no degenerate edges, (ii) no multi-edges (injectivity of edges as unordered vertex pairs), (iii) injective tetrahedron corners, and (iv) skeleton closure (every corner pair of every tet appears as an edge). Face/triangle data is not carried by the incidence shape, so triangle closure is out of scope by design.
The one-tetrahedron complex is the canonical non-empty witness: four vertices, the six edges of $K_4$, and a single tet on those vertices. Establishing that this witness is simplicial makes subclass positivity independent of the empty complex.
proof idea
One-line kernel check: decide. All four conjuncts of IsSimplicial quantify only over the finite index types of the explicit witness (Fin 4 vertices, Fin 6 edges, Fin 1 tetrahedron), so Lean’s decidable instance for the predicate discharges the goal by exhaustive evaluation. No algebraic lemmas, no native_decide, and no external hypotheses.
why it matters
This is the non-vacuous simplicial witness for Full Theory Phase 0b. Downstream, exists_simplicial_with_tet relaxes the witness into every cap $B \ge 6$ and concludes that the simplicial subclass contains a genuinely 3-dimensional configuration (positive tet count), so positivity is not carried by the empty complex alone.
It is also the carrier for the metric-refinement blocker: unitMetricOneTet and doubleMetricOneTet package unit and double edge-length decorations over this same simplicial complex, and oneTetClass_has_two_metric_decorations uses the proof to show two inequivalent metric decorations live on one genuine carrier of complexity six. That separation is the combinatorial half of the claim that metric data is not recoverable from the incidence carrier alone.
Within the gravity/Regge side of Recognition Science, the witness anchors the simplicial path-sum subclass before any continuum or curvature analysis; it does not itself touch the forcing chain (T0–T8) or the J-cost identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.