allOnes_testBit_lt
plain-language theorem explainer
The lemma shows that every bit position k below width t in the integer 2^t - 1 is set. It is invoked inside the one-bit adjacency argument for the wrap-around step of the bounded BRGC Gray path. The proof proceeds by induction on t, rewriting the all-ones mask via the successor-bit lemma and applying the Nat bit-test shift rules.
Claim. For all natural numbers $t$ and $k$ with $k < t$, the $k$-th bit of $2^t - 1$ equals 1.
background
The module Patterns.GrayCycleGeneral builds a bounded Gray cover for general dimension $d$ from the BRGC formula $gray(n) = n$ XOR $(n >>> 1)$. It defines the auxiliary mask $allOnes(t) := 2^t - 1$ and supplies the supporting fact $allOnes(t+1) = Nat.bit true (allOnes t)$. The local development is deliberately restricted to $d ≤ 64$ and routes successor adjacency through GrayCodeAxioms. Upstream results include the definition of one in the integer and rational logic embeddings together with the spin-statistics one, all used only for numeric constants in the surrounding file.
proof idea
The tactic proof performs case analysis on the pair $(t, k)$. The $t = 0$ case is discharged by the absurdity of $k < 0$. For $t+1$ and $k = 0$ it rewrites the mask with allOnes_succ_eq_bit and applies Nat.testBit_bit_zero. For $t+1$ and $k+1$ it obtains the smaller index via Nat.lt_of_succ_lt_succ, rewrites the test-bit via Nat.testBit_bit_succ, then invokes the inductive hypothesis.
why it matters
The lemma supplies the bit-level fact required by the downstream theorem brgc_wrap_oneBitDiff, which asserts that the last and first elements of brgcPath differ by exactly one bit. It therefore closes the wrap-around adjacency needed to package the bounded BRGC construction as a GrayCycle d. The result sits inside the Workstream A generalization that extends the D=3 axiom-free cycle to arbitrary dimension under the 64-bit bound; it does not address the recursive, axiom-free construction given in GrayCycleBRGC.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.