sum_crossNat
plain-language theorem explainer
The signed cross-term contributions over the fifteen nonzero 0/1 edge classes in four dimensions sum to zero. Anyone checking exact cancellation of the axis-TT / pure-gauge cross piece in the provisional finite TT bilinear will cite this. The proof unfolds the bit-mask definitions and discharges the finite sum by decision procedure.
Claim. Let the fifteen Freudenthal-style edge classes be indexed by $d \in \{0,\ldots,14\}$, each with bit-mask $m(d)=d+1$. Write $c_+(d)=\mathbf{1}_{\mathrm{bit}\,2}(m(d))-\mathbf{1}_{\mathrm{bit}\,3}(m(d))$ and $c_g(d)=\mathbf{1}_{\mathrm{bit}\,0}(m(d))$. Then $\sum_d c_+(d)\,c_g(d)=0$ in $\mathbb{Z}$.
background
This module builds the 4D Regge edge stencil after the TT-attachment layer: fifteen nonzero displacement vectors in ${0,1}^4$, indexed by bit masks $d.val+1\in{1,\ldots,15}$. For each class one reads coordinate bits via classBit and forms plane-wave midpoint loads classCoeff H d = D^T H D.
The provisional finite TT quadratic aggregates squared class coefficients with all-ones weights (true 4D Regge weights remain OPEN). Pure gauge loads as $2(m\cdot D)(v\cdot D)$, so the quadratic on pure gauge is not identically zero; exact identities that do hold must be recorded separately.
The integer crossNat d packages the product $c_+(d),c_g(d)$ that appears when polarizing an axis-TT mode against a pure-gauge mode: $c_+$ is the signed difference of the last two spatial bits, $c_g$ the first-coordinate bit. The claim is that these signed products cancel in the sum over all fifteen classes.
proof idea
Term-mode proof by exhaustive evaluation. Unfold crossNat, classBit, and maskOf so each summand is an explicit integer built from Nat.testBit on $d.val+1$. The finite sum over Fin 15 is then closed by decide. No external lemmas are required beyond the three local definitions.
why it matters
Feeds finiteTTBilinear_axisTTPlus_gauge, which asserts that the provisional finite TT bilinear pairing of the axis-TT-plus mode with a pure-gauge load vanishes. That identity is the exact cross-term cancellation needed while documenting that the provisional all-ones quadratic itself is not gauge-invariant.
In the QG campaign this sits inside the 4D Freudenthal edge-class packaging (analogue of the 3D polEdgeCoeff / hinge-diagonal chain). It does not touch true Regge Hessian weights, does not prove $S_{RS}$ converges to Einstein-Hilbert in 4D, and does not flip gap_action_recovery. It is a kernel-checked bookkeeping step that keeps the gauge-entry analysis honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.