natToGray_testBit_false_of_ge
plain-language theorem explainer
The lemma shows that the k-th bit of the binary-reflected Gray code of any n below 2^d is false whenever k is at least d. Pattern theorists constructing injective BRGC paths for arbitrary dimension cite it to control high-order bits during injectivity arguments. The argument lifts the given bound to n < 2^k, applies the library fact that numbers below a power of two have vanishing high bits, and combines the two vanishing bits through the XOR definition of natToGray.
Claim. If $n < 2^d$ and $d ≤ k$, then the $k$-th bit of the binary-reflected Gray code of $n$ is false, where the Gray code is defined by $n ⊕ (n ≫ 1)$.
background
This lemma sits inside the GrayCycleGeneral module, which builds a Gray cover for general dimension d from the bounded BRGC formula gray(n) = n XOR (n >>> 1) and exposes it as a map Fin(2^d) → Pattern d. The supporting definition natToGray implements exactly that bitwise operation. The module works under the GrayCodeFacts hypothesis class, which supplies the classical inversion properties needed for d ≤ 64.
proof idea
The tactic proof first obtains n < 2^k from the given n < 2^d and d ≤ k by monotonicity of exponentiation. It then invokes Nat.testBit_eq_false_of_lt twice: once on n and once on n >>> 1 (whose size bound follows from the division inequality n >>> 1 ≤ n). The final simp step folds these two facts into the XOR expression that defines natToGray.
why it matters
The result is an internal step in the proof of brgcPath_injective, which establishes that the BRGC path map is injective for 0 < d ≤ 64. It therefore supports the bounded bitwise construction of Gray cycles in this module, which the module documentation contrasts with the fully axiom-free recursive development in GrayCycleBRGC. Within the Recognition framework it contributes to the pattern machinery that ultimately feeds the D = 3 case and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.