inOrbitOfRep
plain-language theorem explainer
Boolean predicate: a difference-mask pair (a,b) lies in the S4-orbit of the canonical representative of a given hinge orbit type. Combinatorialists assembling the flat Hessian from per-orbit star kernels cite it as the membership test for the six lattice orbits under coordinate permutation. Implemented by decidable search over the 24 axis permutations applied to the type's fixed representative.
Claim. For a hinge orbit type $\tau\in\{t_{11},t_{12},t_{21},t_{13},t_{31},t_{22}\}$ and natural numbers $a,b$, return true iff there exists a coordinate permutation $\sigma\in S_4$ such that $\sigma$ applied bitwise to the canonical representative pair $(a_\tau,b_\tau)$ yields $(a,b)$.
background
In the Kuhn triangulation of the unit 4-cube, every oriented triangle hinge 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)$. The type of the hinge is the popcount pair $(|a|,|b|)\in{(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$, encoded by the inductive type HingeOrbitType.
Coordinate permutations act on 4-bit masks by permuting bit positions. The map that sends a pair through a permutation $\sigma$ is permDiffPair; the 24 elements of $S_4$ are enumerated by coordPermOf. Each type has a fixed canonical representative pair via orbitRep (e.g. $t_{11}\mapsto(1,2)$, $t_{12}\mapsto(1,6)$).
This module is the combinatorial prerequisite for assembling the flat Hessian of the 4D Regge action from per-orbit star kernels. Scope is combinatorics only of triangle hinges up to lattice translation and triangulation-preserving symmetry; it does not evaluate kernels or complete the Hessian.
proof idea
Definitional, not a proof. The body is a single decide over existential quantification on Fin 24: check whether some axis permutation coordPermOf p, pushed through permDiffPair on the two components of orbitRep ty, recovers the input pair $(a,b)$. Decidability follows from finite search over the 24 permutations and equality on natural numbers.
why it matters
Membership test underlying the lattice-orbit classification (deliverable A.3 of the module): $S_4$ preserves type and is transitive on realizable pairs of each type, giving six orbits. Downstream theorems realizable_in_type_orbit and realizable_matches_rep_orbit use it to state that every realizable difference pair of a given type lies in the single $S_4$-orbit of that type's representative.
Those theorems close the transitivity half of the orbit story needed before per-orbit star kernels can be glued into the flat Hessian. The module explicitly does not flip gap_action_recovery or prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D; this predicate is only the combinatorial gate for that later assembly. Complement symmetry (merging $(i,j)$ with $(j,i)$ under $S_4\rtimes{\mathrm{id},\mathrm{complement}}$) sits in the next section and is independent of this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.