HingeOrbitType
plain-language theorem explainer
Six discrete labels for triangle-hinge difference-mask types in the unit 4-cube Kuhn triangulation, one per realizable popcount pair (|a|,|b|). Gravity analysts cite it when summing per-orbit star kernels into the flat Hessian or zero-momentum moment. It is a bare inductive enumeration with a popcount projection; no proof content.
Claim. There are exactly six lattice orbit types of oriented triangle hinges under coordinate permutation of the 4-cube, labelled by the ordered popcount pairs $(|a|,|b|)\in\{(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)\}$ of the disjoint nonzero difference masks along a monotone vertex-mask chain. Each type projects to its pair via a canonical map to $\mathbb{N}\times\mathbb{N}$.
background
In the 4D Regge setting on a Freudenthal/Kuhn triangulation of the unit 4-cube, every oriented triangle hinge inside a Kuhn simplex is a monotone chain of vertex masks $m_0\subset m_1\subset m_2$. The successive bitwise differences $(a,b)=(m_1\oplus m_0,m_2\oplus m_1)$ are disjoint and nonzero; the combinatorial type of the hinge is the popcount pair $(|a|,|b|)$.
Only six pairs arise: $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$, $(2,2)$. The $S_4$ action on bit positions preserves type and is transitive on realizable pairs of each type, so these six labels are precisely the lattice orbits under coordinate permutation. The seed hinge ${0,e_0,e_0+e_1}$ has type $(1,1)$.
The module is combinatorics-only: it classifies hinges up to lattice translation (difference masks) and triangulation-preserving symmetry, and does not evaluate star kernels or assemble the flat Hessian. A coarser four-orbit quotient under $S_4\rtimes{\mathrm{id},\mathrm{complement}}$ is recorded separately by merging $(i,j)$ with $(j,i)$.
proof idea
No proof: this is an inductive type with six constructors t11 through t22, deriving DecidableEq, Repr, and Fintype. The companion map sends each constructor to its popcount pair by pattern match. Downstream code treats the type as a finite index set for orbit-wise sums.
why it matters
This enumeration is the discrete index set for every per-orbit contribution in the 4D Regge algebraic closer. Downstream, fullMomentOrbitContribution is defined by orbit type, and fullMomentZeroMomentum sums those contributions over all six types; vanishing theorems (axis TT-plus, decoy gauge, deficit-zero) are stated uniformly for each type. Exact-action symbols such as exactDeficitDot likewise case on the type.
In the QG campaign this is deliverable A of the hinge-orbit classification: the combinatorial prerequisite before assembling the flat Hessian from per-orbit star kernels. It does not itself close continuum recovery (S_RS_converges_EH_4d) or flip gap_action_recovery; those remain open targets that consume the orbit sum once Bloch/finite-momentum symbols land.
Relative to the Recognition forcing chain this sits in the gravity analysis layer (Regge discrete action), not in T0–T8 foundation. Its role is bookkeeping: six orbits, fixed multiplicities $(72,48,48,24,24,24)$ in the 240 oriented slots, ready for kernel attachment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.