localEdgeMask
plain-language theorem explainer
Bitwise XOR of the two endpoint vertex masks yields the edge mask for local edge slot e inside Freudenthal 4-simplex s. Anyone assembling the 4D Regge flat-Hessian incidence layer or seed-hinge orbit cites this. Pure combinatorial definition: look up the ten edge pairs, XOR the nested vertex bit-masks.
Claim. For each of the $24$ Freudenthal $4$-simplices $s$ and each of the ten local edge slots $e$ among its five nested vertices, the edge mask is the bitwise XOR of the bit-masks of the two endpoints of $e$. The result is a natural number in $\{1,\ldots,15\}$ indexing one of the fifteen global edge classes.
background
This module is the next kernel-checked increment after the $15$-class Regge edge stencil: explicit Freudenthal/Kuhn enumeration of the $24$ monotone $4$-simplices of the unit $4$-cube, their five nested vertices, and the ten local edges among those vertices. Vertex masks are bit-masks in ${0,\ldots,15}$ built by cumulative axis bits along the permutation that labels simplex $s$.
localEdgePair enumerates the ten unordered pairs among five vertices (slots $0..9$). vertexMask s k is the nested Freudenthal vertex after $k$ steps along $s$ (starting at the origin mask $0$). The edge connecting two nested vertices is the symmetric difference of their axis sets, which on bit-masks is XOR.
The surrounding campaign is MODEL/OPEN on true per-hinge dihedral and area kernels; only combinatorial incidence and the flat-Hessian assembly skeleton are closed here.
proof idea
One-line definitional wrapper. Resolve local edge slot $e$ to its endpoint pair via localEdgePair, then return Nat.xor of the two vertexMask values at those endpoints. No proof obligations; the numeric range $1\le\mathrm{mask}\le 15$ is discharged later by exhaustive fin_cases/decide in the bounds lemma.
why it matters
This is the bridge from nested vertex geometry to the $15$-class stencil imported from ReggeEdgeStencil4D. Downstream, localEdgeClass subtracts one and packages the mask as a Fin 15 class index; localEdgeClass_mask recovers the mask; localEdgeMask_bounds proves the range. The dihedral-kernel side uses it to match seed flat squared lengths to bit-weights for the two seed simplices that contain the hinge triangle (masks $0,1,3$).
It underwrites the incidence-multiplicity count (which classes appear how often in the seed orbit) that forces the flat-Hessian class form to vanish off support. It does not evaluate OPEN deficit/area kernels 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.