classCoeff_decoyTrace_sq
plain-language theorem explainer
For each of the fifteen 4D edge-displacement classes, the squared class coefficient of the pure-trace decoy (Euclidean identity) equals the square of that class's Hamming weight. Gravity analysts cite this when evaluating the provisional finite TT quadratic on pure-trace inputs. The proof is a two-step rewrite through the identity load formula and the weight identification of squared displacement length.
Claim. For every edge class $d \in \{0,\ldots,14\}$, if $c_d(I)$ is the edge-class coefficient of the Euclidean identity and $w(d)$ is the Hamming weight of the class mask, then $c_d(I)^2 = w(d)^2$.
background
This module builds the 4D Regge edge stencil: fifteen Freudenthal-style nonzero displacement classes in ${0,1}^4$, indexed by Fin 15 via bit masks. Each class carries a displacement vector $D$ and a natural Hamming weight $w(d)$ (number of set bits among the four coordinates).
The edge-class coefficient is $c_d(H) = D^T H D$, the same load convention as the 3D polarized edge coefficient. The pure-trace decoy is the Euclidean identity matrix $I$ (explicitly not transverse-traceless). A prior lemma shows $c_d(I) = |D|^2$, and another identifies $|D|^2$ with the real cast of $w(d)$ by exhaustive bit cases.
The local campaign records a provisional finite quadratic aggregate $\sum_d c_d(H)^2$ with all-ones class weights. True 4D Regge Hessian weights remain OPEN; this file does not claim Einstein-Hilbert recovery or full edge-TT decomposition.
proof idea
One-line wrapper. Rewrite the left-hand side by the pure-trace load identity $c_d(I) = |D|^2$, then replace $|D|^2$ by the real cast of the Hamming weight via the squared-displacement-equals-weight lemma. Both sides become $w(d)^2$ in $\mathbb{R}$.
why it matters
Feeds the nonvacuity check that the provisional finite TT quadratic evaluates to 80 on the pure-trace decoy. That parent theorem unfolds the aggregate, rewrites every summand by this square identity, then casts and sums the fifteen Hamming-weight squares. Together with the axis-TT value 8 and the pure-gauge value 32, it documents that the provisional aggregate separates TT, gauge, and trace inputs by distinct predicted numbers.
In the QG full-theory campaign this is a kernel-checked increment after the 4D TT attachment layer: decoy bookkeeping, not a claim that the all-ones weights match the true 4D Regge Hessian. The module explicitly leaves true class weights OPEN and does not flip gap-action recovery or $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.