classCoeff_axisTTPlus
plain-language theorem explainer
For the unnormalized plus polarization diag(0,0,1,−1), the edge-class coefficient on each of the 15 nonzero 0/1 displacements equals the bit-2 indicator minus the bit-3 indicator. Anyone assembling the provisional finite TT quadratic, its square, or the axis-TT/gauge bilinear cites this closed form. The proof unfolds the quadratic form, sums over four coordinates, and finishes by case split and ring.
Claim. Let $H_+=\mathrm{diag}(0,0,1,-1)$ be the unnormalized plus polarization on $\mathbb{R}^4$, and let $D(d)\in\{0,1\}^4$ be the Freudenthal displacement of class $d\in\mathrm{Fin}\,15$. Then the edge-class coefficient satisfies $$D(d)^{\!T} H_+ D(d) = \mathbf{1}_{\mathrm{bit}\,2}(d) - \mathbf{1}_{\mathrm{bit}\,3}(d).$$
background
This module packages the 4D Regge edge stencil after the TT-attachment layer: fifteen Freudenthal-style edge classes, the nonzero vectors in ${0,1}^4$, indexed by bit masks. For a symmetric $4\times 4$ matrix $H$, the class coefficient is the edge load $c_d(H)=D^{!T}HD$ on the $0/1$ displacement of class $d$ (same convention as 3D polEdgeCoeff).
The plus polarization $H_+=\mathrm{diag}(0,0,1,-1)$ is the unnormalized axis TT mode from the edge-TT decomposition. Class bits read the mask of $d$; the displacement has a $1$ in coordinate $i$ exactly when bit $i$ is set. The provisional finite TT quadratic aggregates $\sum_d c_d(H)^2$ with all-ones weights; true 4D Regge weights remain open.
Spatial dimension is fixed at $D=3$ by the forcing chain (T8), so the ambient matrix algebra is $4\times 4$ (three space plus time).
proof idea
Term-mode proof by direct expansion. Unfold the definitions of class coefficient (edge load of the class displacement), the plus-polarization matrix, and the $0/1$ displacement. The quadratic form reduces to a four-term sum over coordinates; Fin.sum_univ_four collapses it. Only the $(2,2)$ and $(3,3)$ diagonal entries of $H_+$ survive, giving $D_2^2-D_3^2$. Since each $D_i\in{0,1}$, this equals the bit-2 indicator minus the bit-3 indicator. Case-split on the two Boolean bits and finish with ring.
why it matters
Closed form for plus-polarization class coefficients is the workhorse for the nonvacuity and decoy suite in this module: the provisional aggregate evaluates to $8$ on axis TT-plus, and the squared-coefficient identity classCoeff_axisTTPlus_sq is an immediate rewrite. Downstream, the Bloch-fold layer specializes it at low masks (classCoeff_axisTTPlus_mask_1/2/3), the integer-coefficient bridge classCoeff_axisTTPlus_int feeds flat Hessian assembly, and finiteTTBilinear_axisTTPlus_gauge uses it to prove the axis-TT/pure-gauge cross term vanishes under the provisional bilinear.
In the QG campaign this is a kernel-checked increment toward a 4D finite TT symbol, not a proof that the RS action converges to Einstein–Hilbert in 4D, nor a derivation of true Regge class weights. It sits downstream of T8 ($D=3$) only through the ambient $4\times 4$ matrix size.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.