simplicialClassStatus
plain-language theorem explainer
Phase-0b status record for the simplicial subclass of bounded path-sum complexes. It marks four combinatorial repairs as done (decidable predicate, Fintype subclass, positive cardinality, non-empty tetrahedron witness) and records that triangle closure is not expressible in this incidence shape. Downstream flag lemmas cite it by reflexivity. Pure structure literal: five Bool fields.
Claim. The Phase-0b status record for the simplicial subclass sets: the simplicial predicate is decidable; the subclass is proved a finite type; its cardinality is proved strictly positive; a non-vacuous simplicial witness has been constructed; triangle (2-face) closure is not expressible in the underlying bounded incidence shape.
background
In the Seven Gaps gravity stack, BoundedComplex B is the garbage-inclusive superclass of bounded incidence configurations: every bounded combinatorial triangulation sits inside it, but so do non-simplicial junk (degenerate edges, repeated tet vertices, multi-edges, tets whose 1-skeleton is missing). Phase 0b carves out the true simplicial subclass via four conditions: distinct edge endpoints, no multi-edges as unordered pairs, four distinct tet vertices, and skeleton closure (every tet vertex pair appears as an edge).
The status structure is an honest scoreboard for that repair. Face (triangle) data is not carried by the bounded complex, so triangle closure cannot even be stated at this shape; the four proved conditions are the full simplicial content available here. The module claims theorem status with zero sorry and zero new axioms; decide is used only on the explicit one-tetrahedron witness.
proof idea
Definitional construction, not a proof. The declaration is a structure value of type SimplicialClassStatus with five literal Bool fields: four set to true (decidable predicate, Fintype subclass, positive card, nonvacuous witness) and triangle_closure_expressible set to false. No tactics, no lemmas applied. Downstream, the companion flags theorem discharges equalities by rfl against these literals.
why it matters
Gives the Phase-0b simplicial-subclass repair a machine-checkable status board inside the gravity Seven Gaps path-sum measure stack. Parent consumer is the flags theorem, which packages the five Bool equalities as a single conjunction for audit and CI. The false triangle-closure flag is deliberate scope honesty: BoundedComplex carries vertex/edge/tet lists only, so 2-face closure is out of band until the incidence shape is extended. This sits upstream of any claim that the path-sum configuration class has been cleaned to abstract simplicial 3-complexes; without the nonvacuous one-tet witness and positive-card proof, positivity would rest on the empty complex alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.