hasBit0
plain-language theorem explainer
Natural-number indicator that is 1 precisely when a Freudenthal 4-cube edge class has its zeroth coordinate bit set in the 0/1 displacement, else 0. Cited when counting or weighting classes that involve the first axis in the provisional finite TT quadratic. One-line Boolean-to-Nat conversion of the class bit test.
Claim. For each of the 15 nonzero edge classes $d$ (indexed by bit masks on $\{0,1\}^4$), define the indicator $\mathbf{1}_{\mathrm{bit}\,0}(d) \in \mathbb{N}$ by $1$ if the displacement of $d$ has coordinate $0$ set, and $0$ otherwise.
background
The module packages the 4D Regge edge stencil after the TT-attachment layer: fifteen Freudenthal-style edge classes, namely the nonzero displacement vectors in ${0,1}^4$, indexed by Fin 15 via masks $d.val+1$. Each class carries a 0/1 displacement whose coordinate bits are read by the Boolean test that asks whether coordinate $i$ is set in that mask.
The present definition turns the bit-0 instance of that test into a natural number, so it can be summed or multiplied inside Nat-valued aggregates. The local campaign is deliberately provisional on class weights (all-ones rather than true 4D Regge Hessian weights) and does not claim Einstein-Hilbert recovery or full edge-TT decomposition.
proof idea
Definition only: return $1$ if the class-bit test at coordinate $0$ holds for $d$, otherwise $0$. No lemmas, no tactics.
why it matters
Feeds the exact count that the sum of these indicators over all fifteen classes equals 8, which is the combinatorial half of the cube with first-axis support. That count is the bookkeeping step used when evaluating the provisional finite TT quadratic on pure gauge loads such as the axis-wave gauge part (where the aggregate evaluates to 32). In the QG campaign this is scaffolding arithmetic for the gauge-entry identity, not a claim about true Regge weights or $S_{RS}\to EH$ in 4D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.