orbitLocalSq
plain-language theorem explainer
Each of the six S₄ lattice orbit types of triangle hinges is assigned the triple of flat squared edge lengths of a canonical difference-mask representative. The lengths are the Hamming weights |a|, |b|, |a∨b| of that pair. Combinatorial gravity work cites this when matching cell triangles to orbit geometry. The body is a one-line composition of the orbit representative with the local-square constructor.
Claim. To each of the six coordinate-permutation orbit types $\tau$ of triangle hinges, associate the triple of flat squared edge lengths of a fixed representative difference-mask pair $(a_\tau,b_\tau)$: $\bigl(|a_\tau|,\,|b_\tau|,\,|a_\tau\lor b_\tau|\bigr)$, where $|\cdot|$ is Hamming weight (popcount) on 4-bit masks.
background
The module classifies triangle hinges in one unit 4-cube Kuhn triangulation up to lattice translation and triangulation-preserving symmetry. Every index-triple triangle is a monotone mask chain with disjoint nonzero difference masks $(a,b)$; its type is the popcount pair $(|a|,|b|)$ in ${(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$. Those six pairs are the constructors of the inductive type of lattice orbit types under coordinate permutation.
Canonical $S_4$-orbit representatives supply one concrete disjoint pair per type (e.g. type $(1,1)$ uses $(1,2)$). The structure of flat squared edge lengths packages three natural numbers: the Hamming weights of $a$, of $b$, and of the bitwise OR $a\lor b$, which are the squared lengths of the three boundary edges of the hinge in the flat embedding. The local-square map from a raw difference pair is exactly that triple of popcounts.
Scope is combinatorics only: no per-orbit star kernels beyond the committed seed, and no flat Hessian of the 4D Regge action.
proof idea
Definitional one-liner. On an orbit type $\tau$, read the canonical representative pair from the orbit-representative table, then apply the local-square constructor: popcount of the first mask, popcount of the second, and popcount of their bitwise OR. No case split or proof obligation beyond the existing representative table.
why it matters
Gives a uniform geometric label (three flat squared lengths) for each lattice orbit, so downstream statements can compare cell triangles to orbit data without re-deriving Hamming weights. The value table theorem records the six concrete triples $\langle 1,1,2\rangle,\langle 1,2,3\rangle,\langle 2,1,3\rangle,\langle 1,3,4\rangle,\langle 3,1,4\rangle,\langle 2,2,4\rangle$. The slot theorem then asserts that every cell triangle's difference-mask local square equals this map on its orbit type (proved by exhaustive fin_cases and decide).
That match is a combinatorial prerequisite for assembling the flat Hessian from per-orbit star kernels in the QG full-theory campaign. It does not itself evaluate kernels, complete the Hessian, or touch $S_{\mathrm{RS}}\to EH$ convergence or gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.