hingeTypePop
plain-language theorem explainer
Assigns to each oriented triangle slot in a Kuhn 4-cube the popcount pair of its two successive difference masks. That pair is the combinatorial type used throughout the Regge hinge orbit census. Anyone assembling flat Hessian star kernels or counting lattice orbits under coordinate permutation cites it. The body is a one-line pairing of the two mask Hamming weights.
Claim. For each Kuhn simplex index $s \in \{0,\ldots,23\}$ and each oriented triangle slot $t \in \{0,\ldots,9\}$ inside that simplex, return the pair $\bigl(|a|,|b|\bigr)$ where $a = m_1 \oplus m_0$ and $b = m_2 \oplus m_1$ are the successive difference masks of the monotone vertex-mask chain $m_0 \subset m_1 \subset m_2$, and $|\cdot|$ is the Hamming weight on the four low bits.
background
This module classifies triangle hinges in one unit 4-cube Kuhn triangulation up to lattice translation and triangulation-preserving symmetry. It is a combinatorial prerequisite for assembling the flat Hessian of the 4D Regge action from per-orbit star kernels; it does not evaluate those kernels or prove continuum recovery.
Every index-triple triangle in a Kuhn simplex is a monotone mask chain $m_0 \subset m_1 \subset m_2$ with disjoint nonzero difference masks $(a,b)=(m_1\oplus m_0,, m_2\oplus m_1)$. The first and second difference masks are extracted by XOR on the three vertex masks of the slot. Hamming weight is taken only on the four low bits (masks live in ${0,\ldots,15}$).
The realizable popcount pairs are exactly ${(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$. These six pairs label the lattice orbits under coordinate permutation $S_4$ on bit positions; the seed hinge has type $(1,1)$.
proof idea
Pure definitional wrapper. Read the three vertex masks of slot $(s,t)$, form the two successive XOR difference masks, and return the pair of their four-bit Hamming weights. No lemmas or tactics; the body is the ordered pair of those two popcounts.
why it matters
This is the type map that turns every oriented triangle slot into a discrete orbit label. Downstream, orbit membership is rewritten as equality of this pair with a canonical pop pair (isOrbit_iff_pop), and the same equality specializes the seed type $(1,1)$ (isT11_iff_pop). Cell counts per type, including the committed $72$ slots of type $(1,1)$, are obtained by summing indicators built from it.
Complement symmetry is stated by swapping the two components of the pair, and the honest refinement that absolute $(1,1)$ triangles are not $S_4$-transitive compares two slots that share this type but lie in distinct absolute orbits. In the QG campaign this sits at deliverable A of the hinge classification: six $S_4$ orbits (four under the larger group with complement), feeding later Bloch-fold and flat-Hessian assembly without yet evaluating star kernels or closing $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.