localEdgeClass
plain-language theorem explainer
Maps each of the ten local edges of a Freudenthal 4-simplex onto one of the fifteen global edge classes of the 4-cube stencil. Anyone assembling per-simplex kernels onto the class basis cites this. The definition is the XOR endpoint mask shifted down by one, with membership in Fin 15 discharged by the mask bounds lemma.
Claim. For each of the $24$ monotone $4$-simplices $s$ and each local edge slot $e\in\{0,\ldots,9\}$, the local edge class is $\mathrm{mask}(s,e)-1\in\{0,\ldots,14\}$, where $\mathrm{mask}(s,e)$ is the XOR of the two endpoint vertex masks of that edge in $s$.
background
This module is the next kernel-checked increment after the 4D Regge edge stencil: it enumerates the $24$ Freudenthal/Kuhn monotone $4$-simplices of the unit $4$-cube and their ten local edges among the fifteen global edge classes. The fifteen-class stencil is imported, never redefined.
Each simplex is labeled by a permutation of the four axes. Vertices carry bitmasks built by cumulative axis flips along that permutation. A local edge is a pair of nested vertices; its XOR mask is a nonzero integer in ${1,\ldots,15}$ indexing the stencil class of that geometric edge.
The upstream mask definition returns that XOR as a natural number. The bounds theorem states $0 < \mathrm{mask}(s,e)\le 15$ for every simplex and slot, proved by exhaustive fin_cases/decide.
proof idea
One-line definitional packaging: form the subtype $\langle \mathrm{mask}(s,e)-1,_\rangle:(\mathrm{Fin},15)$ and discharge the inequality $0\le \mathrm{mask}-1<15$ by invoking the upstream bounds theorem and omega. No further case analysis lives here; the exhaustive work is already in the bounds lemma.
why it matters
This is the bridge from local simplex edge slots to the global fifteen-class basis used throughout the flat-Hessian assembly. Downstream, assembleClassKernel sums a Fin-10 local kernel onto classes by equality with this map; the evaluation theorem reduces that sum to the two active deficit slots. Partial deficit class kernels for classes $3$, $7$, $11$ (and vanishing off those classes) are proved by deciding concrete values of this map on the seed simplex.
In the QG campaign this is deliverable-B combinatorial support only: incidence and class routing for the MODEL assembly skeleton. It does not supply the OPEN per-hinge dihedral/Cayley–Menger weights, nor complete the flat Hessian of the 4D Regge action, nor touch $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ or gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.