SimplicialClassStatus
plain-language theorem explainer
Status record for Phase 0b of the simplicial-subclass repair on bounded path-sum complexes. Five boolean flags track decidability of the simplicial predicate, Fintype structure, positive cardinality, a non-empty witness, and whether triangle closure is expressible. Gravity auditors cite it to read the honest combinatorial scope of BoundedComplex. Pure structure definition with no proof body.
Claim. A five-field boolean status record for the simplicial subclass of bounded incidence complexes: whether the simplicial predicate is decidable; whether that subclass is a finite type; whether its cardinality is strictly positive; whether a non-empty simplicial witness has been built; and whether triangle (2-face) closure is expressible in the underlying incidence shape.
background
Phase 0b of the SevenGaps gravity path carves a true simplicial subclass out of BoundedComplex, the garbage-inclusive superclass of bounded incidence configurations (vertex, edge, and tetrahedron lists). That superclass admits degenerate edges, multi-edges, repeated tet vertices, and tets whose 1-skeleton is missing from the edge list.
The simplicial conditions enforced here are: distinct edge endpoints; edges injective as unordered pairs; four distinct vertices per tetrahedron; and skeleton closure (every vertex pair of every tet appears as an edge). These are the full combinatorial content of an abstract simplicial 3-complex presented by tetrahedra and 1-skeleton in this incidence shape.
Face (triangle) data is not carried by the bounded-complex type, so 2-face closure is not expressible. The module records that honest scope in this status structure. Related status patterns appear elsewhere in the monolith (RS-native units, discrete Lichnerowicz operator convergence) as plain claim ledgers.
proof idea
No proof: this is a structure declaration whose five fields are plain Bool slots. Downstream, a single value of the structure is filled by assigning true to the four proved combinatorial claims and false to triangle-closure expressibility. The actual theorems (decidability, Fintype, positive card, one-tetrahedron witness) live as sibling declarations in the same module.
why it matters
Gives Phase 0b a single readable claim ledger so the simplicial repair is auditable without scanning every lemma. The sole downstream consumer is the concrete status value, which sets the four combinatorial flags true and triangle closure false, matching the module claim of zero sorry and zero new axioms.
In the Recognition gravity stack this sits under SevenGaps path-sum measure work: before continuum or discrete-curvature statements can rest on combinatorial complexes, the incidence class must exclude non-simplicial garbage. The structure makes the missing triangle layer explicit rather than silent. It does not itself touch T0–T8 forcing, RCL, or the mass ladder; it is infrastructure for later discrete-geometry claims (e.g. discrete Lichnerowicz-type operator work on simplicial backgrounds).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.