triangleVertexMasks
plain-language theorem explainer
For each of the 24 Kuhn 4-simplices and each of the 10 oriented triangle slots, this returns the ordered triple of 4-bit vertex masks of that triangle. Orbit classification and Bloch-phase bookkeeping cite it as the canonical base data for a hinge. The body is a one-line unpack of the combinatorial index triple through the Freudenthal vertex-mask map.
Claim. Given a Kuhn simplex index $s \in \{0,\ldots,23\}$ and a triangle slot $t \in \{0,\ldots,9\}$, let $(i,j,k)$ be the increasing vertex-index triple for slot $t$ in a 4-simplex. Return the ordered triple of nested Freudenthal bit-masks $\bigl(m(s,i),\, m(s,j),\, m(s,k)\bigr) \in \{0,\ldots,15\}^3$.
background
The module classifies triangle hinges in the unit 4-cube Kuhn (Freudenthal) triangulation up to lattice translation and triangulation-preserving symmetry. Scope is pure combinatorics: 24 simplices, $C(5,3)=10$ oriented triangle slots per simplex, difference-mask types, and $S_4$ (plus complement) orbits. It does not evaluate star kernels or assemble the flat Hessian.
Each simplex $s$ is a monotone chain of nested vertex masks. The upstream map vertexMask sends a step index $r \in {0,\ldots,4}$ to the 4-bit mask of the nested Freudenthal vertex after $r$ axis steps along the permutation of $s$ (values in ${0,\ldots,15}$). The sibling triangleIndexTriple enumerates the ten increasing triples of vertex indices in a 4-simplex, e.g. $(0,1,2)$, $(0,1,3)$, … .
A triangle hinge is therefore three nested masks along that chain. Downstream Bloch and orbit code reads the first component as the hinge base and the successive XORs as difference masks $(a,b)$ whose popcounts label the six combinatorial types.
proof idea
Definitional one-liner. Unpack $t$ via triangleIndexTriple to an ordered index triple $(i,j,k)$ in $\mathrm{Fin},5$, then apply vertexMask s componentwise and return the resulting $\mathbb{N}\times\mathbb{N}\times\mathbb{N}$ triple. No lemmas, no tactics.
why it matters
This is the shared hinge-base extractor for the 4D Regge Bloch and orbit pipeline. Downstream, hingeBase and hingeBaseZ read the first mask as lattice coordinates; baseTurns, phase2Nat, and phase2NatE0 count low bits of that mask to build quarter-turn and double-phase integers; phaseScale_eq_phase2Nat equates the continuous phase scale to that integer formula. Within the module, absoluteTriple and the difference-mask utilities (diffMaskA, diffMaskB, hingeTypePop) build on the same triple to prove the six popcount types and the four lattice orbits under $S_4 \rtimes {\mathrm{id},\mathrm{complement}}$.
In the QG campaign this is deliverable-A scaffolding: combinatorial prerequisite for assembling the flat Hessian from per-orbit star kernels. It does not itself close Hessian assembly, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ convergence, or gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.