HingeOrbitTypeModComplement
plain-language theorem explainer
Enumerates the four lattice orbits of triangle-hinge difference-mask types under the triangulation-preserving group generated by coordinate permutations and bitwise complement. Anyone assembling the flat Hessian of the 4D Regge action from per-orbit star kernels cites this as the coarse orbit label. It is a plain inductive type with four constructors, derived DecidableEq/Fintype.
Claim. An inductive type with four constructors $o_{11}$, $o_{12}$, $o_{13}$, $o_{22}$, classifying triangle-hinge difference-mask popcount pairs up to the action of $S_4\rtimes\{\mathrm{id},\mathrm{complement}\}$. The six $S_4$-orbits of type $(|a|,|b|)\in\{(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)\}$ collapse by identifying $(i,j)\sim(j,i)$ under bitwise complement $m\mapsto m\oplus 15$.
background
The module classifies triangle hinges inside one unit 4-cube Kuhn triangulation, up to lattice translation (difference masks) and triangulation-preserving symmetry. Every index-triple triangle 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 type is the popcount pair $(|a|,|b|)$.
Under coordinate permutation alone there are six orbits, recorded by the sibling inductive type with constructors $t_{11},t_{12},t_{21},t_{13},t_{31},t_{22}$. Bitwise complement $m\mapsto m\oplus 15$ sends Kuhn vertex-sets to Kuhn vertex-sets and swaps type $(i,j)$ with $(j,i)$. The larger group $S_4\rtimes{\mathrm{id},\mathrm{complement}}$ therefore merges $(1,2)\sim(2,1)$ and $(1,3)\sim(3,1)$, leaving four orbits.
Scope is combinatorics only: no star-kernel evaluation and no claim about the flat Hessian of the 4D Regge action.
proof idea
Definitional inductive type, not a proved statement. Four constructors name the complement-merged orbits. The companion map from the six $S_4$-orbit labels sends $t_{11}\mapsto o_{11}$, collapses ${t_{12},t_{21}}\mapsto o_{12}$ and ${t_{13},t_{31}}\mapsto o_{13}$, and sends $t_{22}\mapsto o_{22}$. DecidableEq, Repr, and Fintype are derived automatically.
why it matters
Deliverable A of the QG full-theory campaign needs a coarse orbit label once complement symmetry is quotiented in. Downstream, orbit_count_S4_complement proves there are exactly four such orbits by decide on the Fintype instance. The six-type sibling remains the fine label under pure $S_4$; this type is the one used when star kernels are assembled up to the full triangulation-preserving group.
It does not itself evaluate kernels or close the flat-Hessian or $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ goals flagged in the module doc. It is the combinatorial bookkeeping step that makes those later sums finite and orbit-indexed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.