orbit_count_S4_complement
plain-language theorem explainer
There are exactly four lattice orbits of triangle hinges in the unit 4-cube Kuhn triangulation once coordinate permutation is enlarged by bitwise complement. Anyone assembling the flat Hessian from per-orbit star kernels cites this count. The proof is a one-line `decide` on the finite inductive type of complement-merged orbit labels.
Claim. The set of triangle-hinge orbit types under the group $S_4 \rtimes \{\mathrm{id},\,\mathrm{complement}\}$ is finite of cardinality $4$.
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 building 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 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|)\in{(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, giving six orbits.
Bitwise complement $m\mapsto m\oplus 15$ preserves Kuhn vertex-sets and swaps type $(i,j)$ with $(j,i)$. Under the larger group $S_4\rtimes{\mathrm{id},\mathrm{complement}}$, the pairs $(1,2)\sim(2,1)$ and $(1,3)\sim(3,1)$ merge. The inductive type HingeOrbitTypeModComplement packages the resulting four labels: $o_{11}$, $o_{12}$, $o_{13}$, $o_{22}$.
proof idea
One-line decidability proof. The target type derives Fintype and DecidableEq from its four constructors, so Fintype.card _ = 4 is a closed propositional goal discharged by decide. No lemmas about masks, popcounts, or group actions are invoked; the count is purely the cardinality of the inductive enumeration.
why it matters
Deliverable A of the Regge 4D hinge-orbit campaign states that complement symmetry collapses the six $S_4$ type-orbits to four lattice orbits. This theorem records that collapse as a machine-checked cardinality fact: the complement-merged orbit type has exactly four inhabitants.
In the QG full-theory stack, orbit counts fix how many independent star-kernel blocks enter the flat Hessian assembly. Downstream work that sums or indexes over complement-merged orbits needs a proved finite basis of size four; this declaration supplies that basis size. It does not yet appear in a parent theorem (used_by is empty), but it closes the enumeration half of the module's complement-symmetry claim.
Framework context: combinatorial scaffolding for 4D Regge gravity toward continuum recovery ($S_{\mathrm{RS}}\to$ Einstein-Hilbert), not a forcing-chain (T0-T8) step. It touches neither mass ladders nor $\alpha$ bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.