classDispSq
plain-language theorem explainer
Squared Euclidean length of a 4D Freudenthal edge-class displacement: for each of the 15 nonzero {0,1}^4 masks, sum the four squared components. Equals the Hamming weight of the mask. Cited wherever the provisional TT quadratic or period-doubling carrier needs flat class lengths. Definition is a four-term sum of 0/1 products.
Claim. For each nonzero edge class $d\in\{1,\ldots,15\}$, write $D(d)\in\{0,1\}^4$ for its displacement vector. Define the flat squared length $\|D(d)\|_2^2:=\sum_{i=0}^{3} D(d)_i^2$. This equals the Hamming weight of the bit mask of $d$.
background
This module packages the 4D Regge edge stencil after the TT-attachment layer: fifteen Freudenthal-style edge classes, namely the nonzero displacement vectors in ${0,1}^4$, indexed by Fin 15 via bit masks $d.val+1$. Each class carries a displacement $D(d)$ with entries in ${0,1}$ (the sibling classDisp).
The squared length is the natural scalar attached to that vector under the flat Euclidean metric on the four coordinate axes. Because entries are 0/1, $|D|_2^2$ coincides with the number of set bits (Hamming weight of the class mask). The module treats this as the provisional class weight in the finite quadratic aggregate; true 4D Regge Hessian weights at flat remain OPEN and must not be reverse-engineered from Einstein-Hilbert.
Upstream, the displacement itself is the bit-wise indicator of the mask. Downstream equalities identify this squared length with the natural-number weight and with the period-doubling carrier's squared class lengths.
proof idea
Pure definition: expand the squared Euclidean norm of the four-component 0/1 displacement as $\sum_{i:\mathrm{Fin},4} D(d)_i\cdot D(d)_i$. No lemmas are applied at the definition site. Later theorems (classDispSq_eq_weight) discharge the identification with Hamming weight by unfolding and case-splitting the four bits.
why it matters
Supplies the scalar length that the provisional finite TT quadratic and the decoy-trace coefficient read off each Freudenthal class. Parent results: classDispSq_eq_weight (squared length equals natural Hamming weight), classCoeff_decoyTrace (on the identity decoy, the class coefficient collapses to this length), and in Gap2 Freudenthal period-doubling, periodicDispSqEdge4_eq_classDispSq together with dispWeight4_eq_classWeightNat, which place the carrier's squared class lengths on the recognition ladder via Gap1ClassLengths.classLength_in_recognition_ladder.
In the QG campaign this is the 4D analogue of the 3D edge-class packaging. It does not close the OPEN item on true Regge weights, nor S_RS_converges_EH_4d, nor full edge_tt_decomposition. It is the honest flat yardstick against which gauge non-invariance of the all-ones provisional aggregate is measured (pure gauge yields $\sum_d 4(m\cdot D)^2(v\cdot D)^2\neq 0$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.