sum_hasBit0
plain-language theorem explainer
Among the 15 nonzero 0/1 displacement classes in four dimensions, exactly eight have the zeroth coordinate bit set. Anyone counting axis-aligned contributions in the provisional 4D Regge edge stencil cites this. The proof unfolds the bit-mask definitions and finishes by finite decision.
Claim. Let the fifteen nonzero edge classes be indexed by $d \in \{0,\ldots,14\}$ with bit-masks $m(d)=d+1 \in \{1,\ldots,15\}$. Write $h_0(d)=1$ if bit $0$ of $m(d)$ is set and $h_0(d)=0$ otherwise. Then $\sum_d h_0(d)=8$.
background
This module packages the 4D Freudenthal-style edge classes for a provisional finite TT quadratic on the Regge edge stencil. Nonzero displacement vectors in ${0,1}^4$ are indexed by Fin 15 via masks $m(d)=d+1\in{1,\ldots,15}$.
For each class $d$ and coordinate $i\in{0,1,2,3}$, the Boolean classBit asks whether bit $i$ is set in $m(d)$. The Nat indicator hasBit0 is $1$ precisely when coordinate $0$ participates in the displacement of class $d$, and $0$ otherwise.
The local campaign is the 4D lift of the 3D finite TT edge-class packaging. Class weights of the true 4D Regge Hessian remain open; the provisional aggregate uses weight $1$ on every nonzero class.
proof idea
Term-mode proof by unfolding. Expand hasBit0, classBit, and maskOf so the sum becomes an explicit sum of fifteen Boolean-to-Nat indicators on the fixed masks $1,\ldots,15$. The tactic decide then evaluates the finite sum in the kernel and closes equality with $8$. No external lemmas are required beyond the three local definitions.
why it matters
Feeds finiteTTQuadratic_gaugePart_axisWave, which evaluates the provisional finite TT quadratic on the pure-gauge load gaugePart axisWave axisGaugeVector and obtains the exact value $32$. That evaluation needs a clean count of how many classes carry a fixed axis bit, because pure-gauge class coefficients factor as $2(m\cdot D)(v\cdot D)$ and the squared aggregate reduces to a weighted sum of bit indicators along the chosen axes.
In the module's honest scope this is part of the nonvacuity and decoy suite: the aggregate is $8$ on axisTTPlus, $32$ on pure gauge, and $80$ on pure trace. It does not touch true Regge Hessian weights, does not prove $S_{\mathrm{RS}}$ converges to Einstein-Hilbert in 4D, and does not flip gap_action_recovery. It is a small combinatorial kernel fact that keeps the gauge-entry identities exact rather than numerical.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.