allOnes_testBit_eq_false_at
plain-language theorem explainer
The lemma shows that 2^t minus 1 has its t-th bit unset. It is invoked inside the proof that the BRGC path wrap-around differs by exactly one bit. The short tactic proof first derives the strict inequality allOnes t < 2^t via Nat.sub_lt and then applies the library fact Nat.testBit_eq_false_of_lt.
Claim. For every natural number $t$, the $t$-th bit of $2^t - 1$ is false: $(2^t - 1).testBit(t) = false$.
background
The GrayCycleGeneral module constructs a bounded Gray cover for dimension d using the standard BRGC formula under the assumption d ≤ 64. The auxiliary definition allOnes t := 2^t - 1 supplies the integer whose lowest t bits are set. This lemma is called from the upstream allOnes definition to support the one-bit difference at the cycle wrap-around point.
proof idea
The tactic proof first establishes allOnes t < 2^t by rewriting the definition and invoking Nat.sub_lt on the positivity of 2^t and 1. It then applies the library lemma Nat.testBit_eq_false_of_lt to the inequality, yielding the required bit equality.
why it matters
The lemma supplies the final arithmetic step inside brgc_wrap_oneBitDiff, which proves the wrap-around adjacency for the BRGC path when d = t + 1. It therefore contributes to the bounded GrayCycle construction in the Patterns domain before the fully recursive, axiom-free development in GrayCycleBRGC.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.