simplex0Classes_complete
plain-language theorem explainer
Every edge class in the Freudenthal simplex-0 table is realized by at least one of that simplex's ten local edge slots. Anyone checking the 4D Regge incidence support against the 15-class stencil cites this. The proof is exhaustive Fin-case analysis with decide after reverting membership.
Claim. Let $C_0 = \{0,1,2,3,5,6,7,11,13,14\}$ be the edge-class set of Freudenthal simplex $0$ (axis permutation $(0,1,2,3)$). For every $d \in C_0$, simplex $0$ carries class $d$ among its ten local edges.
background
This module builds the combinatorial skeleton for the flat Hessian of the 4D Regge action on the Freudenthal (Kuhn) triangulation of the 4-cube. The 15 edge classes come from the imported stencil ReggeEdgeStencil4D and are never redefined here. The 24 monotone 4-simplices are the axis permutations; each has five nested vertices and ten local edges, each edge tagged by one of the 15 classes.
simplex0Classes is the explicit Finset of ten classes belonging to simplex 0 (permutation $(0,1,2,3)$). simplexHasClass s d is the Boolean that asks whether some local edge slot of simplex $s$ has class $d$. The theorem asserts that the table for simplex 0 is faithful: every listed class really appears.
The broader campaign treats per-hinge deficit and area kernels as OPEN parameters. What is closed here is only the combinatorial support of the seed-hinge orbit and its incidence multiplicities.
proof idea
Term-mode proof by exhaustive case split. Membership of $d$ in the ten-element Finset is reverted, then fin_cases d branches over all fifteen possible classes in Fin 15. On each branch decide discharges the Boolean equality simplexHasClass 0 d = true (or the false membership cases vanish because the hypothesis is gone). No external lemmas beyond the definitions of the class table and the local-edge predicate.
why it matters
Closes one honesty gate on deliverable B of the Regge 4D flat-kernel campaign: the simplex-0 class table is not a decorative list but a realized incidence set. That feeds the incidence-multiplicity counts (how many seed-simplices carry each of the 15 classes as a local edge) and the nonvacuity / decoy statements that three classes lie outside the support.
No downstream theorem yet consumes this lemma directly. It does not evaluate OPEN per-hinge area or deficit kernels, does not assemble the numeric flat Hessian, and does not touch S_RS_converges_EH_4d or gap_action_recovery. Within Recognition gravity it is pure combinatorial hygiene before any continuum or Einstein–Hilbert comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.