hingeOrbitType
plain-language theorem explainer
Assigns each oriented triangle slot in the 24 Kuhn simplices of the unit 4-cube to one of six lattice orbit types under coordinate permutation. The type is the popcount pair of the two successive difference masks along the monotone vertex chain. Downstream Bloch-orbit and fold lemmas cite it as the canonical classifier. Implementation is a thin composition: popcounts, optional map to the inductive type, defaulting to the (1,1) seed.
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 lattice orbit type of the triangle: the element of $\{t_{11}, t_{12}, t_{21}, t_{13}, t_{31}, t_{22}\}$ whose popcount pair matches $(|a|,|b|)$, where $(a,b)$ are the successive disjoint difference masks of the triangle's monotone vertex-mask chain. If the pair is not one of the six realizable types, return $t_{11}$ by default.
background
This module classifies triangle hinges in one unit 4-cube Kuhn triangulation, up to lattice translation (difference masks) and triangulation-preserving symmetry. It is a combinatorial prerequisite for assembling the flat Hessian of the 4D Regge action from per-orbit star kernels. Scope is combinatorics only: no star-kernel evaluation and no claim that the Regge action converges to Einstein-Hilbert.
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)$. Its raw type is the popcount pair $(|a|,|b|)\in{(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$. The inductive type HingeOrbitType names those six classes under the $S_4$ action on bit positions.
Upstream, hingeTypePop computes that pair from the two difference masks of slot $(s,t)$. popToOrbitType maps each realizable pair to the corresponding constructor and returns none otherwise.
proof idea
Definitional one-liner. Evaluate the popcount pair of the two successive difference masks via hingeTypePop s t, feed it to popToOrbitType, and take .getD .t11 so an unrealizable pair collapses to the seed type $t_{11}$. No tactics; pure composition of the three local helpers.
why it matters
Canonical typed classifier for every triangle slot in the 4D Kuhn cell. Downstream, isOrbit and isOrbit_iff_pop (ReggeBlochAllOrbitSymbol4D) define membership in a named lattice orbit by equality with this value; isT11 / isT11_iff_pop specialize to the seed orbit used in fold identities. Orbit-transport theorems orbitCoveringPerm_covers and orbitCoveringPerm_spec index covering permutations by this type, so every slot is reduced to its representative difference pair.
In the QG campaign this is deliverable A of the hinge-orbit classification: six $S_4$-orbits (four under the larger $S_4\rtimes{\mathrm{id},\mathrm{complement}}$ group). It does not itself evaluate star kernels or close the flat Hessian, but every later per-orbit assembly step routes through it. Local inverse hingeOrbitType_toPop and realizability matching also depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.