localHingeMasks
plain-language theorem explainer
Maps each of the four unit-cube translates that meet the seed hinge to the three vertex bitmasks of that hinge in local Freudenthal coordinates. Gravity analysts working the 4D Regge star deficit cite it when filtering which Kuhn simplices contain the hinge. Pure case-split definition on the cube-translate inductive; no proof obligations.
Claim. For each cube translate $c\in\{\mathrm{origin},\,-e_2,\,-e_3,\,-e_2-e_3\}$, the local hinge mask set is the three-element finite set of vertex bitmasks of the seed triangle hinge $\{0,\,e_0,\,e_0+e_1\}$ in that cube's coordinates: $\{0,1,3\}$, $\{4,5,7\}$, $\{8,9,11\}$, and $\{12,13,15\}$ respectively.
background
In the Freudenthal–Kuhn triangulation of the integer lattice, each unit 4-cube is cut into 24 ordered 4-simplices. Vertices carry bitmasks in ${0,\ldots,15}$ recording which of the four basis steps have been taken. The seed hinge of this module is the triangle on masks $0$, $1=e_0$, and $3=e_0+e_1$.
The full periodic star of that hinge meets exactly four unit cubes. Those cubes are labeled by the inductive type of cube translates: the origin cube together with the three negative shifts along $e_2$, $e_3$, and $e_2+e_3$. Parallel mask tables appear in the type-(1,2), (1,3), and (2,2) hinge-orbit kernels.
The module is the next kernel-checked increment after the dihedral cosine calculus. Scope is the seed hinge orbit only; other lattice hinge orbits remain open.
proof idea
Definition by exhaustive pattern match on the four constructors of the cube-translate inductive. Each branch returns a hard-coded three-element finite set of natural numbers: the local vertex masks of the seed hinge inside that cube. No lemmas, no tactics, no computation.
why it matters
Direct input to the hinge-containment predicate, which decides whether a Kuhn simplex (indexed in $\mathrm{Fin},24$) contains the hinge by checking that every local mask appears among the simplex's five vertex masks. That predicate drives the star-member list and the six-simplex star enumeration (deliverable A.1: exactly six cube-translate/Kuhn-simplex pairs contain the seed hinge).
Downstream the same masks feed flat-cosine multisets, the $2\pi$ flatness gate, and the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$. The definition is scaffolding for the QG full-theory campaign; it does not itself close flat Hessian assembly, $S_{\mathrm{RS}}$ convergence to Einstein–Hilbert in 4D, or the action-recovery gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.