popToOrbitType
plain-language theorem explainer
Maps a pair of natural numbers (popcounts of two disjoint difference masks) to one of the six lattice orbit types of a 4D Kuhn triangle hinge, or to none if the pair is not among the six admissible types. Combinatorial gravity work cites it when converting raw mask popcounts into typed orbits under coordinate permutation. The body is a pure pattern match on the six allowed pairs.
Claim. Define a partial map from pairs of natural numbers to hinge orbit types by sending $(1,1)\mapsto t_{11}$, $(1,2)\mapsto t_{12}$, $(2,1)\mapsto t_{21}$, $(1,3)\mapsto t_{13}$, $(3,1)\mapsto t_{31}$, $(2,2)\mapsto t_{22}$, and every other pair to undefined. Here each $t_{ij}$ is the lattice orbit type of a triangle hinge whose two successive difference masks have Hamming weights $i$ and $j$.
background
In the 4D Regge campaign on a unit hypercube Kuhn triangulation, every oriented triangle hinge inside a simplex is a monotone three-step vertex-mask chain $m_0 \subset m_1 \subset m_2$. The successive bitwise differences $a = m_1 \oplus m_0$ and $b = m_2 \oplus m_1$ are disjoint and nonzero; the combinatorial type of the hinge is the popcount pair $(|a|,|b|)$.
Module scope is pure combinatorics of those hinges up to lattice translation and triangulation-preserving symmetry. Exactly six popcount pairs arise: ${(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$. The inductive type of orbit labels has one constructor per pair. This definition is the dictionary from raw popcount pairs into that inductive type (with a none branch for impossible pairs).
Upstream mask and stencil APIs supply the 24 Kuhn simplices and the 15-class edge masks; this map never redefines them. It only classifies already-computed popcounts.
proof idea
No proof: the declaration is a total pattern-matching definition on $\mathbb{N}\times\mathbb{N}$. Six explicit clauses return some of the corresponding orbit constructor; the catch-all returns none. Downstream theorems discharge the none branch by exhaustive case analysis on the finite set of triangle slots.
why it matters
This dictionary is the bridge from raw difference-mask popcounts to typed orbits. The theorem that every triangle slot has one of the six orbit types is exactly the statement that applying this map to the hinge popcount never yields none. The typed orbit extractor for a slot is defined by applying the map and defaulting (safely, once that theorem is in hand). Transitivity of the $S_4$ action on realizable pairs of a fixed type also routes through this map when selecting the orbit representative.
Downstream, the Bloch-fold side uses the same dictionary to characterize the seed $(1,1)$ orbit via an iff with popcount equality. In the broader QG campaign this is deliverable A of the hinge classification: combinatorial prerequisite for assembling the flat Hessian from per-orbit star kernels. It does not itself evaluate kernels, complete the Hessian, or touch action-recovery gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.