hingeOrbitType_toPop
plain-language theorem explainer
Round-trip identity: the typed lattice orbit of a Kuhn triangle slot, converted back to a popcount pair, recovers the raw difference-mask popcounts. Orbit-membership lemmas in the Bloch and fold modules cite it to equate typed predicates with concrete $(|a|,|b|)$ equalities. Proof is exhaustive finite case split on the 24 simplices and 10 slots, discharged by decide.
Claim. For every Kuhn simplex index $s\in\{0,\ldots,23\}$ and every oriented triangle slot $t\in\{0,\ldots,9\}$, if one maps the popcount pair of the two difference masks of $(s,t)$ to a typed orbit and then reads that type back as a popcount pair, the result equals the original pair $(\mathrm{pop}(a),\mathrm{pop}(b))$.
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 complete the Hessian.
Each oriented triangle slot in a Kuhn simplex is a monotone vertex-mask chain whose successive XOR differences $(a,b)$ are nonzero and bitwise disjoint. The popcount-pair type is $(\mathrm{pop}(a),\mathrm{pop}(b))\in{(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$. The definition hingeTypePop returns that pair; hingeOrbitType packages it as a six-valued orbit enum via popToOrbitType, defaulting to the seed type $(1,1)$.
The six types are the lattice orbits under coordinate permutation $S_4$ on bit positions. Complement symmetry merges $(i,j)$ with $(j,i)$, yielding four orbits under the larger group.
proof idea
Pure finite exhaustion. Split on the simplex index $s:\mathrm{Fin},24$, then on the triangle slot $t:\mathrm{Fin},10$, and discharge each of the $240$ concrete equalities by decide. No algebraic lemma is invoked beyond the definitions of typed orbit and popcount pair; the round-trip holds because every realizable popcount pair is in the domain of the orbit encoding and toPop is its left inverse on that image.
why it matters
Closes the dictionary between the enum HingeOrbitType and the concrete popcount pairs used in mask arithmetic. Downstream, isOrbit_iff_pop rewrites typed orbit membership as hingeTypePop s t = ty.toPop, and isT11_iff_pop specializes to the seed type $(1,1)$; both proofs open by applying this identity.
In the QG campaign this is deliverable-A glue: cell enumeration and orbit counts are already established, and star-kernel assembly needs a clean bridge from typed predicates to mask popcounts. It does not touch the forcing chain (T0–T8), RCL, or continuum limits; it only stabilizes the combinatorial typing layer that those later steps will sum over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.