orbitRep_realizable
plain-language theorem explainer
Every one of the six lattice orbit types of a 4D Kuhn triangle hinge has a canonical difference-mask pair that actually arises from some cell triangle. Combinatorialists building the flat Hessian of the 4D Regge action cite this to seed each S4 orbit with a concrete realizable pair. The proof is a finite case split on the six orbit labels, each discharged by decide.
Claim. For every hinge orbit type $\tau$ among the six popcount classes $\{(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)\}$, the canonical $S_4$-orbit representative pair $(a,b)$ assigned to $\tau$ is realizable: there exist a Kuhn simplex index $s\in\{0,\ldots,23\}$ and a triangle slot $t\in\{0,\ldots,9\}$ whose difference masks equal $a$ and $b$.
background
In the 4D Kuhn triangulation of the unit hypercube there are 24 simplices and $C(5,3)=10$ oriented triangle slots per simplex (240 hinges total). Each hinge is a monotone vertex-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)$. The type of a hinge is the popcount pair $(|a|,|b|)$, taking values in the six classes above.
The module classifies these hinges up to lattice translation (difference masks) and coordinate permutation ($S_4$ acting on the four bit positions). An inductive label type enumerates the six popcount classes. A Boolean predicate asks whether a concrete pair $(a,b)$ arises as the difference pair of some cell triangle (existential search over the 24-by-10 finite set). A companion map picks one canonical pair per class, e.g. $(1,2)$ for type $(1,1)$ and $(1,6)$ for type $(1,2)$.
Local setting (module doc): combinatorics only of triangle hinges in one unit 4-cube Kuhn triangulation; prerequisite for assembling the flat Hessian from per-orbit star kernels. It does not evaluate those kernels or prove Einstein-Hilbert recovery.
proof idea
One-line wrapper. Case-split on the six constructors of the orbit-type inductive; each branch is a ground Boolean equality isRealizableDiffPair a b = true for the concrete pair returned by the representative map, discharged by decide (exhaustive search over the finite simplex and triangle-slot indices).
why it matters
Fills deliverable item 3 of the module: lattice orbits under coordinate permutation. Every realizable disjoint difference pair appears, and the $S_4$ action is transitive on each type, so six orbits; the seed hinge ${0,e_0,e_0+e_1}$ has type $(1,1)$. This theorem certifies that the chosen canonical pairs really sit inside those orbits, so later star-kernel and Hessian assembly can quote a single concrete seed per type.
No downstream consumers are wired yet (used_by empty). The larger triangulation-preserving group $S_4\rtimes{\mathrm{id},\mathrm{complement}}$ merges $(1,2)\sim(2,1)$ and $(1,3)\sim(3,1)$ into four orbits; that refinement is separate. The module explicitly does not flip gap-action recovery or $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.