simplex1Classes
plain-language theorem explainer
Explicit finite set of the ten edge classes (among the fifteen stencil classes) carried by Freudenthal 4-simplex 1, the axis permutation (0,1,3,2). Gravity and discrete-Regge analysts cite it as the combinatorial support table for the second seed-containing simplex. The body is a literal Finset literal of ten indices in Fin 15.
Claim. Let the fifteen edge classes of the 4D Regge edge stencil be indexed by $\{0,\ldots,14\}$. The edge-class support of Freudenthal simplex $1$ (the monotone 4-simplex for the axis permutation $(0,1,3,2)$) is the ten-element set $\{0,1,2,3,7,9,10,11,13,14\}\subset\{0,\ldots,14\}$.
background
This module sits in the QG full-theory campaign immediately after the 15-class edge stencil of ReggeEdgeStencil4D. The setting is the Freudenthal/Kuhn triangulation of the 4-cube: twenty-four monotone 4-simplices, one per permutation of the four coordinate axes, each contributing five nested vertices and ten local edges whose classes live among the fifteen global stencil classes.
The seed hinge is the triangle with vertex masks $0$, $e_0$, $e_0+e_1$ (classes $0,1,3$). Exactly two of the twenty-four simplices contain that hinge: the permutations that begin $(0,1,\ldots)$. Simplex $0$ is one; simplex $1$ is the other, corresponding to the axis order $(0,1,3,2)$. The present definition records which ten of the fifteen classes appear as local edges of that second simplex.
Sibling machinery (localEdgeClass, simplexHasClass, axis/vertex masks) computes those classes from the permutation; this Finset is the static table those computations are checked against.
proof idea
Pure definition: a Finset literal on Fin 15 listing the ten indices ${0,1,2,3,7,9,10,11,13,14}$. No tactics, no lemmas. Correctness and completeness relative to the computed local edges of simplex $1$ are discharged later by the decide-driven theorems that consume this table.
why it matters
This table is half of the combinatorial incidence support for the seed hinge. Downstream, seedHingeIncidenceNat adds the indicator of membership in this set to the corresponding indicator for simplex $0$, giving the number of seed-containing simplices that carry each class $d$. The theorems simplex1Classes_correct and simplex1Classes_complete certify that the table matches the ten computed local edges of simplex $1$ and that every listed class is realized. Their sum identity sum_seedHingeIncidenceNat then closes the mass count $2\times 10=20$.
In the module's honest scope this is deliverable-B scaffolding for flat-Hessian assembly: incidence multiplicities force the MODEL class form to vanish off support. It does not evaluate OPEN per-hinge deficit or area kernels, does not complete the flat Hessian of the 4D Regge action, and does not touch S_RS_converges_EH_4d or gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.