classDispSq_eq_weight
plain-language theorem explainer
For each of the fifteen Freudenthal edge classes of the 4-cube, the squared Euclidean length of the {0,1}^4 displacement equals that class's natural weight. Gravity analysts cite it when turning class-length identities into integer weight arithmetic on decoy and kernel dots. The proof is exhaustive case analysis on the four class bits after unfolding.
Claim. For every nonzero displacement class $d$ among the fifteen Freudenthal edge classes of the $4$-cube, if $D_d\in\{0,1\}^4$ is the corresponding bit-mask displacement, then $\|D_d\|_2^2$ equals the natural class weight of $d$ (as a real number).
background
This module packages the 4D Regge edge stencil after the TT-attachment layer: fifteen Freudenthal-style edge classes, namely the nonzero vectors in ${0,1}^4$, indexed by Fin 15 via bit masks. Each class $d$ has four bits; the displacement $D_d$ is assembled from those bits, and the squared length is the sum of squares of the four components.
Because components are $0$ or $1$, squared length coincides with Hamming weight. The natural class weight is exactly that count, cast to $\mathbb{R}$. The module's provisional finite quadratic uses weight $1$ on every nonzero class; true 4D Regge Hessian weights remain open and must not be reverse-engineered from Einstein-Hilbert.
The local convention matches the 3D polEdgeCoeff / 4D edge-load pattern: class coefficients are of the form $D^\top H D$, later multiplied by a midpoint plane-wave phase. This identity is the bridge from geometric length to the integer weight used in decoy and kernel calculations.
proof idea
Term-mode proof by definition chase and finite exhaustion. Unfold the squared-displacement, displacement, and natural-weight definitions. Simplify the sum over Fin 4 with the universe-sum lemma. Case-split on each of the four class bits (sixteen branches). Each branch is a concrete $0/1$ vector; norm_num checks that the sum of squares equals the bit count.
why it matters
Feeds the decoy-trace coefficient identity: squared class coefficient on pure trace equals squared natural weight. That rewrite is the first step in the flat 4D Hessian assembly proofs that each full-star deficit kernel is orthogonal to the pure-trace decoy (kernels 11, 12, 13, 22).
Also closes the Gap-2 carrier comparison: periodic squared class lengths equal stencil squared lengths, hence sit on the recognition ladder via the Gap-1 class-length theorem. In the QG campaign this is a small but load-bearing arithmetic fact inside the Freudenthal 4-cube packaging; it does not itself recover Einstein-Hilbert or flip action-recovery gaps.
Framework contact is indirect: the 4-cube and eight-tick octave sit behind the stencil design (T7/T8 landmarks), while the identity itself is pure finite geometry of ${0,1}^4$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.