simplicialClassStatus_flags
plain-language theorem explainer
Records the Phase-0b bookkeeping flags for the simplicial subclass of bounded path-sum complexes: the simplicial predicate is decidable, the subclass is a nonempty finite type with a concrete one-tetrahedron witness, and triangle closure is not expressible on this incidence shape. Gravity auditors cite it as the machine-checked status snapshot. Proof is five reflexivity checks against the status definition.
Claim. The Phase-0b status record asserts: the simplicial predicate is decidable; the simplicial subclass is proved to be a finite type; its cardinality is proved strictly positive; a nonvacuous simplicial witness has been constructed; and triangle (face) closure is not expressible on the underlying incidence data. Concretely these five boolean fields equal $true, true, true, true, false$ respectively.
background
In the SevenGaps path-sum gravity stack, BoundedComplex B is the garbage-inclusive superclass of bounded incidence configurations: every bounded combinatorial triangulation sits inside it, but so do degenerate edges, repeated tet vertices, multi-edges, and tets whose 1-skeleton is missing. Phase 0b carves out the true simplicial subclass via four combinatorial conditions: no degenerate edges, no multi-edges (edges as injective unordered pairs), four distinct vertices per tetrahedron, and skeleton closure (every vertex pair of every tet appears as an edge).
Face (triangle) data is not carried by the incidence shape, so triangle closure cannot be stated here; the module records that limitation honestly in the status record. Upstream, simplicialClassStatus is the concrete record with those five booleans hard-coded from the surrounding proofs (decidability, Fintype instance, positive cardinality via simplicialComplex_card_pos, and the explicit oneTetComplex witness).
proof idea
Pure term-mode reflexivity. The theorem packages the five field equalities as a single conjunction and discharges each conjunct by rfl against the definitional values in simplicialClassStatus. No lemmas, no tactics, no computation beyond definitional equality.
why it matters
This is the Phase-0b status seal for the simplicial subclass inside the gravity SevenGaps path-sum measure development. The module doc frames the work as Full Theory Phase 0b: theorem-grade (zero sorry, zero new axioms), with decide used only for finite checks on the explicit one-tetrahedron witness. Downstream consumers of the status record can pattern-match on these flags without re-auditing the surrounding proofs.
No parent theorems currently depend on this declaration (used_by is empty); it is a terminal bookkeeping node. It does not touch the forcing chain T0–T8, RCL, or the mass ladder; its role is local hygiene for the combinatorial geometry underlying path-sum gravity configurations. The explicit triangle_closure_expressible = false flag documents an honest scope cut rather than a hidden gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.