simplex0Classes_correct
plain-language theorem explainer
Every local edge of Freudenthal simplex 0 lands in the tabulated ten-class set {0,1,2,3,5,6,7,11,13,14}. Anyone checking the combinatorial support of the 4D Regge hinge stencil cites this. The proof is exhaustive case-split on the ten edge slots, each discharged by decidable membership.
Claim. For every edge slot $e \in \{0,\ldots,9\}$, the local edge class of slot $e$ inside Freudenthal simplex $0$ (the monotone 4-simplex for axis order $(0,1,2,3)$) belongs to the finite set $\{0,1,2,3,5,6,7,11,13,14\} \subset \{0,\ldots,14\}$.
background
This module builds the Freudenthal/Kuhn triangulation of the 4-cube for a Regge hinge analysis. The 24 monotone 4-simplices are the axis permutations; each simplex has five nested vertices and ten local edges. Edge geometry is classified into the fixed 15-class stencil imported from ReggeEdgeStencil4D, never redefined here.
localEdgeClass s e is the stencil class (an element of $\mathrm{Fin},15$) of local edge slot $e$ in simplex $s$, obtained by shifting the corresponding edge mask down by one. For simplex $0$ (permutation $(0,1,2,3)$), the intended support is the explicit finset simplex0Classes $= {0,1,2,3,5,6,7,11,13,14}$.
The surrounding campaign is deliverable B of the QG full-theory path: combinatorial incidence of a seed hinge orbit, with open per-hinge deficit and area kernels left as parameters in the flat-Hessian assembly skeleton.
proof idea
Pure finite exhaustion. Case-split on the ten values of $e : \mathrm{Fin},10$, then close each goal by decide on membership of the concrete localEdgeClass 0 e value in the literal finset. No lemmas beyond the definitions of localEdgeClass and simplex0Classes are required; the computation is fully kernel-checked.
why it matters
This is the first correctness gate for the tabulated edge-class supports of the 24 Freudenthal simplices. Matching the table for simplex 0 certifies that the combinatorial support used later for incidence multiplicities, decoy classes, and the flat-Hessian assembly skeleton is not an ad-hoc list: it is exactly the image of the local-edge map on that simplex.
Module scope is explicit: this does not evaluate dihedral or Cayley–Menger kernels, does not complete the flat Hessian of the 4D Regge action, and does not prove continuum recovery ($S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$) or flip gap_action_recovery. It is a kernel-checked combinatorial lemma inside the hinge-incidence layer that feeds those later MODEL/OPEN steps. No downstream theorems yet depend on it in the graph; sibling tables for the remaining simplices follow the same pattern.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.