OrbitLocalSq
plain-language theorem explainer
A three-field record holding the flat squared edge lengths of a triangle hinge with difference masks (a,b): Hamming weights |a|, |b|, and |a∨b|. Gravity analysts packaging Kuhn-cell hinge geometry before star-kernel assembly cite it. Pure data structure (no proof content); downstream maps build instances from masks or orbit types.
Claim. A record of three natural numbers $(\ell_A,\ell_B,\ell_{AB})$ equal to the Hamming weights $|a|$, $|b|$, and $|a\vee b|$ of a hinge difference-mask pair $(a,b)$. These are the flat squared lengths of the three boundary edges of the hinge in the unit 4-cube Kuhn triangulation.
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)$. The hinge type is the popcount pair $(|a|,|b|)$ in ${(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$. Under $S_4$ on bit positions there are six lattice orbits; adjoining bitwise complement merges swaps and yields four orbits.
Flat squared edge lengths on the lattice are exactly those Hamming weights: the three boundary edges of the hinge have lengths squared $|a|$, $|b|$, and $|a\vee b|$. This structure packages that triple.
proof idea
No proof: a bare structure with three ℕ fields (lenA, lenB, lenAB) deriving decidable equality and a printer. Instances are built by the sibling constructors localSqOfDiff (from raw masks via popcount and bitwise OR) and orbitLocalSq (from a hinge orbit type via a fixed representative pair).
why it matters
Supplies the local geometric payload that orbit classification attaches to each hinge type. Downstream, localSqOfDiff fills the triple from difference masks, and orbitLocalSq lifts a HingeOrbitType to that triple via the orbit representative. That packaging is the combinatorial input needed later when per-orbit star kernels are assembled into the flat Hessian of the 4D Regge action (QG full-theory campaign). It does not itself touch kernel evaluation, Einstein–Hilbert recovery, or the action-gap flag; it only freezes the length data that those later steps will consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.