orbitLocalSq_values
plain-language theorem explainer
For each of the six triangle-hinge orbit types in the 4D Kuhn cell, the local squared edge lengths equal the Hamming weights of the two difference masks and their sum. Gravity analysts assembling per-orbit Regge star kernels cite this as the explicit length dictionary. The proof is a single decide over the six finite representatives.
Claim. For the six difference-mask orbit types $(|a|,|b|)\in\{(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)\}$ of triangle hinges in a unit 4-cube Kuhn triangulation, the triple of local squared edge lengths is $\langle |a|,|b|,|a|+|b|\rangle$: namely $\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$, and $\langle 2,2,4\rangle$ respectively.
background
In the 4D Regge calculus campaign, triangle hinges of the Freudenthal/Kuhn triangulation of the unit 4-cube are classified by disjoint nonzero difference masks $(a,b)$ along a monotone vertex-mask chain $m_0\subset m_1\subset m_2$. The orbit type is the popcount pair $(|a|,|b|)$, taking one of the six values $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$, $(2,2)$.
The local-squared-length map sends each orbit type to the Euclidean squared lengths of the three edges of a fixed representative cell triangle. On the unit hypercube lattice those lengths equal the Hamming weights of $a$, of $b$, and of $a\oplus b$ (hence $|a|+|b|$, since $a$ and $b$ are disjoint).
This module is combinatorics only: it enumerates orbits under lattice translation and triangulation-preserving symmetry, as a prerequisite for assembling the flat Hessian from per-orbit star kernels. It does not evaluate those kernels or complete the Hessian.
proof idea
The local-squared-length map is defined by evaluating squared lengths on the difference-mask pair of a fixed orbit representative. Unfolding that definition on the six orbit-type constructors produces six concrete triples of natural numbers. The claimed conjunction of equalities is therefore a purely decidable proposition on a finite enumerated type, discharged by a single decide.
why it matters
This is the explicit length lookup table inside deliverable A of the Regge 4D hinge-orbit classification. Any later construction of per-orbit star kernels, or of the flat Hessian of the 4D Regge action, needs the squared-edge data of each orbit type in closed form rather than by recomputing masks. The module frames the whole file as a combinatorial prerequisite for the QG full-theory campaign toward continuum recovery of Einstein-Hilbert 4D; this theorem pins the metric content of the six orbits. The dependency graph currently lists no downstream users, so the result sits as a ready leaf for kernel assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.