localMask
plain-language theorem explainer
Bitwise change of frame that sends an absolute 4D lattice vertex mask into the local coordinates of a chosen unit-cube corner. Anyone enumerating Freudenthal simplices around a fixed Regge hinge cites it. The body is the single operation XOR with the corner's 4-bit shift mask.
Claim. Given a cube corner $c$ (a 4-bit mask in $\{0,\ldots,15\}$, bit $i$ set iff the corner sits at coordinate $-1$ on axis $i$) and an absolute vertex mask $m\in\mathbb{N}$, the local mask is $m\oplus c$.
background
The module builds the full periodic-lattice star deficit kernel for the type-(2,2) Regge hinge ${0,e_0+e_1,e_0+e_1+e_2+e_3}$ (absolute masks ${0,3,15}$) in 4D Freudenthal triangulation. Cube corners are the 16 axis-aligned unit cubes with coordinates in ${-1,0}$, encoded as CubeCorner $\simeq$ Fin 16: bit $i$ set means the corner is shifted by $-1$ on axis $i$.
Absolute vertex labels are integer bitmasks on the integer lattice. To test incidence of a hinge with a Kuhn simplex inside a translated cube, those absolute masks must be rewritten in the cube's local ${0,1}^4$ frame. The geometric containment rule (every negatively shifted axis must have absolute coordinate $0$) is stated on the sibling CubeCorner documentation; the present definition supplies the coordinate change that makes that test local.
proof idea
One-line definitional wrapper: return Nat.xor m c.val. No lemmas, no tactics. The XOR flips precisely the axes on which the corner is shifted by $-1$, converting absolute lattice coordinates into the unit cube's local bit coordinates.
why it matters
Immediate consumer is localHingeMasks, which images the absolute hinge vertex set under this map to obtain the hinge's local masks inside each candidate corner. That local set is the input to the star-enumeration deliverable of the module: exactly four (cube translate, Kuhn simplex) pairs contain the (2,2) hinge, and only the origin corner among the 16 candidates contains the absolute hinge.
The definition is pure scaffolding for the QG full-theory campaign's type-(2,2) kernel increment. It does not itself touch flat cosine multisets, the $2\pi$ angle-sum gate, or the 15-class deficit kernel, but every later incidence check in the star depends on having local masks first. Framework context: discrete Regge gravity on the 4D periodic lattice en route to the still-open S_RS_converges_EH_4d and gap_action_recovery goals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.