allOnes
plain-language theorem explainer
Defines the natural number consisting of d consecutive one-bits in binary. Researchers formalizing binary reflected Gray code paths for cycle covers in d-dimensional pattern spaces reference this mask value. The definition is a direct arithmetic expression using exponentiation and subtraction with no further steps.
Claim. The map sending each natural number $d$ to the integer $2^d - 1$.
background
This definition sits inside the module that builds Gray cycles for arbitrary dimension $d$ from the binary reflected Gray code formula $gray(n) = n$ XOR $(n >>> 1)$. The module supplies a bounded bitwise development whose successor-adjacency claims route through GrayCodeAxioms when $d ≤ 64$. The value $2^d - 1$ functions as the bit mask that isolates the highest bit position in the subsequent lemmas on testBit and successor representations.
proof idea
The definition is a one-line arithmetic expression. It supplies the base case for the bit lemmas allOnes_succ_eq_bit, allOnes_testBit_lt and allOnes_testBit_eq_false_at that follow immediately in the same file.
why it matters
The definition supports the one-bit adjacency argument in brgc_wrap_oneBitDiff, which closes the wrap-around step of the BRGC path and thereby yields a GrayCycle d. It therefore contributes to the general-dimension construction that the module contrasts with the axiom-free D=3 case in GrayCycle.lean. The parent result is the packaged GrayCover and GrayCycle objects for the Patterns domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.