localSqOfDiff
plain-language theorem explainer
Given two difference masks of a triangle hinge, return the triple of Hamming weights of a, b, and a∨b. Those weights are the flat squared lengths of the three boundary edges. Orbit classifiers and the slot-matching theorem cite this constructor. The body is a three-field structure pack of maskPop.
Claim. For difference masks $a,b\in\mathbb{N}$, define the local squared-length triple $(|a|,|b|,|a\vee b|)$, where $|\cdot|$ is the Hamming weight on the four low bits (masks in $\{0,\ldots,15\}$). This is the flat edge-length data of the hinge with those difference masks.
background
The 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 assembling the flat Hessian of the 4D Regge action from per-orbit star kernels; it does not evaluate those kernels or complete the Hessian.
Every index-triple triangle 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)$. Types are popcount pairs $(|a|,|b|)$ in ${(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$.
maskPop is the Hamming weight on the four low bits. OrbitLocalSq packages the three boundary squared lengths as those weights: $|a|$, $|b|$, and $|a\vee b|$.
proof idea
Definitional constructor only: pack OrbitLocalSq with fields maskPop a, maskPop b, and maskPop (a ∨ b) (bitwise OR). No lemmas or tactics.
why it matters
Supplies the length triple that labels each hinge orbit by its flat edge data. Downstream, orbitLocalSq applies it to the canonical difference-mask representative of each HingeOrbitType. The theorem slot_localSq then asserts that every cell triangle's difference masks yield the same triple as its orbit type: local squared lengths match difference-mask Hamming data.
That matching is part of deliverable A in the QG full-theory campaign: six $S_4$ orbits (four under the larger group with complement), with fixed per-type slot counts. Without a uniform length map from masks, orbit kernels cannot be indexed cleanly when the flat Hessian is later assembled. This definition does not itself touch $S_{\mathrm{RS}}\to$ Einstein–Hilbert recovery or gap-action flags.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.