absHingeMasks
plain-language theorem explainer
The absolute vertex set of the type-(2,2) Regge triangle hinge in 4D, recorded as the three 4-bit masks {0, 3, 15}. Anyone assembling the full periodic Freudenthal star for this hinge orbit cites this set as the fixed absolute hinge. It is a literal Finset definition: origin, e0+e1, and the full diagonal e0+e1+e2+e3.
Claim. The absolute vertex masks of the type-$(2,2)$ triangle hinge are the three 4-bit integers $\{0, 3, 15\}$, encoding the lattice points $0$, $e_0+e_1$, and $e_0+e_1+e_2+e_3$ on the 4D unit cube.
background
This module builds the full-star deficit class kernel for one hinge orbit in the 4D periodic Freudenthal lattice: the type-(2,2) triangle hinge. Cube corners are encoded as 4-bit masks; bit $i$ set means coordinate $-1$ on axis $i$, else $0$. Vertices of simplices and hinges are likewise absolute masks in ${0,\ldots,15}$.
The hinge itself is the triangle ${0,, e_0+e_1,, e_0+e_1+e_2+e_3}$, written in mask form as ${0,3,15}$ with difference masks $(3,12)$. The campaign imports the Freudenthal incidence layer, the 15-class edge stencil, and the Gram-projection cosine calculus; it does not redefine those APIs.
Downstream checks (which cube corners contain the hinge, and how absolute masks map to local masks inside a corner) all read this fixed three-element set.
proof idea
Pure definition: the Finset literal ${0, 3, 15}$. No lemmas, no tactics. The three integers are the binary encodings of the three absolute hinge vertices stated in the module scope.
why it matters
This is the seed data for the type-(2,2) star kernel deliverable. cornerContainsHinge decides whether a cube corner contains every absolute hinge mask; localHingeMasks maps the absolute set into a corner by XOR with the corner bitmask. Both sit on the path to star enumeration (exactly four (cube translate, Kuhn simplex) pairs contain the hinge), the flat cosine multiset, the flatness gate (star angle sum $2\pi$), and the full-star deficit class kernel on all 15 stencil classes.
In the QG full-theory campaign this is the next kernel-checked increment after the type-(1,1) seed orbit. It does not close flat Hessian assembly over all hinges, nor $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, nor the action-recovery gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.