classCoeff_axisTTPlus_sq
plain-language theorem explainer
For each of the fifteen 0/1 edge-displacement classes in 4D, the squared class coefficient of the unnormalized plus TT polarization equals a 0-or-1 natural indicator that bits 2 and 3 differ. Gravity analysts evaluating the provisional finite TT quadratic on pure plus polarization cite this identity. The proof rewrites by the closed form for the coefficient, case-splits the two class bits, and normalizes.
Claim. For every edge class $d\in\{0,\ldots,14\}$, let $c_d$ be the edge-class coefficient $D^\top H D$ of the plus TT matrix $H=\mathrm{diag}(0,0,1,-1)$, and let $n_d\in\{0,1\}$ be $1$ precisely when the class bits on axes $2$ and $3$ differ. Then $c_d^2=n_d$ as real numbers.
background
This module packages the 4D Regge edge stencil after the TT-attachment layer: fifteen Freudenthal-style nonzero displacement classes in ${0,1}^4$, indexed by bit masks. For a symmetric $4\times 4$ matrix $H$ and class $d$, the edge-class coefficient is $c_d(H)=D^\top H D$ (same convention as 3D polEdgeCoeff / 4D edge load), with $D$ the $0/1$ displacement of the class. Class bits read individual coordinates of that mask.
The plus polarization is the unnormalized TT matrix $\mathrm{diag}(0,0,1,-1)$. An upstream closed form already evaluates its class coefficient as the difference of two $0/1$ indicators on bits $2$ and $3$. The companion natural square is defined to be $1$ exactly when those two bits differ, else $0$. The provisional finite TT quadratic aggregates $\sum_d c_d(H)^2$ with all-ones class weights (true 4D Regge weights remain OPEN).
proof idea
One short tactic proof. Rewrite the left-hand side by the closed form for the plus-class coefficient (difference of bit-$2$ and bit-$3$ indicators). Unfold the natural square definition. Case-split on the two Boolean class bits; each of the four branches is a numeric identity discharged by norm_num.
why it matters
Feeds the nonvacuity check that the provisional finite TT quadratic equals $8$ on pure plus polarization: the parent theorem rewrites the sum of squared coefficients through this identity, casts the natural sum, and evaluates it. That check sits in the honest-scope list of the 4D Regge edge stencil (QG full-theory campaign, next kernel-checked increment after TT attachment). It does not touch true Regge Hessian weights, Einstein-Hilbert recovery, or the ledger name for full edge-TT decomposition; those remain OPEN per the module contract.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.