sum_axisTTPlusSqNat
plain-language theorem explainer
Over the fifteen nonzero binary edge classes in 4D, the sum of the 0/1 squared plus-class coefficients equals 8. Gravity analysts cite it when evaluating the provisional finite TT quadratic on the axis-plus mode. The proof unfolds the bit-mask definitions and closes by finite decision on Fin 15.
Claim. Let the fifteen nonzero displacement classes in $\{0,1\}^4$ be indexed by $d\in\mathrm{Fin}\,15$, with bit-mask $m(d)=d+1$. Write $b_i(d)$ for the $i$-th bit of $m(d)$. Then $\sum_d \mathbf{1}_{b_2(d)\neq b_3(d)}=8$.
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 bit masks $m(d)=d.val+1\in{1,\ldots,15}$. For each class, classBit reads whether coordinate $i$ is set in that mask.
The auxiliary axisTTPlusSqNat is the natural square of the plus-class coefficient on a fixed axis-plus TT seed: it is $1$ when bits $2$ and $3$ of the class differ, and $0$ otherwise. The module's provisional finite quadratic aggregates squared class coefficients with all-ones weights (true 4D Regge Hessian weights remain OPEN).
Local setting is the QG full-theory campaign's kernel-checked increment: plane-wave midpoint loading and a polarization identity in $H$, without claiming Einstein-Hilbert recovery or full edge-TT decomposition.
proof idea
Term-mode proof by unfolding. Expand axisTTPlusSqNat, then classBit and maskOf, so each summand becomes the concrete Boolean test that bits $2$ and $3$ of $d.val+1$ differ. The remaining goal is a closed natural-number identity over the finite type Fin 15, discharged by decide.
why it matters
Supplies the exact integer tally needed by finiteTTQuadratic_axisTTPlus, which shows the provisional aggregate equals $8$ on the axis-plus TT seed. That evaluation is the module's nonvacuity check: the aggregate is $8$ on axis-plus, versus the distinct predicted values $32$ (pure gauge) and $80$ (pure trace).
In the Recognition gravity chain this is bookkeeping for the 4D lift of the 3D TT edge-class packaging, not a dynamics claim. It does not touch T0-T8 forcing, RCL, or the alpha band; it only certifies one finite sum inside the provisional stencil. True Regge class weights and S_RS_converges_EH_4d remain explicitly open upstream of this lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.