simplex1Classes_correct
plain-language theorem explainer
Every local edge slot of Freudenthal 4-simplex 1 (axis order (0,1,3,2)) has its computed stencil class inside the fixed ten-element table for that simplex. Combinatorial auditors of the 4D Regge hinge incidence cite this to trust the simplex-1 row of the class tables. The proof is an exhaustive Fin-10 case split discharged by decide.
Claim. Let simplex $1$ be the Freudenthal 4-simplex for the axis permutation $(0,1,3,2)$. For every local edge slot $e\in\{0,\ldots,9\}$, the local edge class of $e$ in that simplex lies in the set $\{0,1,2,3,7,9,10,11,13,14\}$ among the fifteen Regge edge-stencil classes.
background
This module builds the combinatorial skeleton for the flat Hessian of the 4D Regge action on the Freudenthal (Kuhn) subdivision of the 4-cube. There are 24 monotone 4-simplices, one per permutation of the four axes; each simplex has five nested vertices and ten local edges. Those edges are labeled by masks drawn from the fifteen global edge classes of the imported 4D edge stencil; the three classes that never appear on a given simplex are combinatorial decoys for that cell.
localEdgeClass s e is the stencil class (in Fin 15) of local edge slot $e$ inside simplex $s$. The table simplex1Classes hardcodes the ten classes realized by simplex 1, namely the permutation $(0,1,3,2)$: ${0,1,2,3,7,9,10,11,13,14}$. The present theorem asserts that the computed local classes match that table entrywise.
The larger campaign treats per-hinge area weights and deficit second-variation kernels as open parameters; only incidence support and the assembly skeleton are kernel-checked here.
proof idea
Pure finite exhaustion. fin_cases e splits the goal into the ten concrete values of e : Fin 10. On each branch, decide evaluates membership of localEdgeClass 1 e in the literal finset simplex1Classes and closes the goal. No algebraic lemmas are required beyond the definitions of the local mask, the class coercion, and the hardcoded table.
why it matters
This is one of the per-simplex correctness gates that make the Freudenthal incidence tables trustworthy. The module's deliverable B needs every simplex row to agree with the computed local edges before incidence multiplicities, seed-hinge orbit counts, and the flat-Hessian assembly skeleton can be cited. Downstream used-by is currently empty, so the theorem is infrastructure rather than a direct input to a named parent result.
It does not evaluate dihedral or Cayley–Menger kernels, does not prove convergence of the RS action to Einstein–Hilbert in 4D, and does not close gap_action_recovery. It only certifies that the simplex-1 class table is not a hand-edited mismatch with the mask arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.