simplex0Classes
plain-language theorem explainer
Explicit finite set of the ten edge classes carried by Freudenthal 4-simplex 0 (axis order 0,1,2,3) inside the 15-class Regge edge stencil. Gravity analysts cite it as the combinatorial support table for that simplex when building seed-hinge incidence. The body is a literal Finset literal on Fin 15.
Claim. The edge-class support of Freudenthal simplex $0$ (the monotone $4$-simplex for axis permutation $(0,1,2,3)$) is the ten-element subset $\{0,1,2,3,5,6,7,11,13,14\}$ of the fifteen stencil classes indexed by $\mathrm{Fin}\,15$.
background
This module is the next kernel-checked increment after the 4D Regge edge stencil: it enumerates the 24 Freudenthal/Kuhn 4-simplices of the unit 4-cube (one per axis permutation) and records which of the fifteen global edge classes appear as local edges on each simplex. The stencil itself is imported and never redefined.
Each 4-simplex has five nested vertices and ten edges. Those ten edges land in ten of the fifteen stencil classes; the remaining three classes are combinatorial decoys for that simplex. Simplex $0$ is the identity permutation $(0,1,2,3)$.
The only external name in the dependency cone is the foundational oriented-edge inductive type from multi-distinction geometry; here the relevant object is the stencil class index in $\mathrm{Fin},15$, not the square-edge constructors.
proof idea
Pure definition: the body is the closed Finset literal ${0,1,2,3,5,6,7,11,13,14}$ of type $\mathrm{Finset},(\mathrm{Fin},15)$. No lemmas, tactics, or computation are invoked at the definition site. Downstream theorems discharge membership and completeness by finite case analysis (fin_cases + decide) against the independently computed local-edge map for simplex $0$.
why it matters
This table is the combinatorial support for simplex $0$ in the seed-hinge incidence calculus. It is consumed by the incidence multiplicity seedHingeIncidenceNat (adds one when the class lies in this set or in the simplex-$1$ twin), by the correctness theorem that every local edge of simplex $0$ lands in the table, by the completeness theorem that every listed class is realized by some local slot, and by the total-mass identity that the seed hinge carries incidence sum $20$ ($2$ simplices $\times$ $10$ edges).
In the module's honest scope this is deliverable B infrastructure: A-shaped gates on combinatorial support for the flat-Hessian assembly skeleton. 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_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ or gap-action recovery. It sits in the gravity analysis layer that prepares class weights for later Recognition-to-Einstein–Hilbert comparison, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.