gray_code_one_bit_property
plain-language theorem explainer
Consecutive binary-reflected Gray codes differ in exactly one bit position. Discrete mathematicians and hardware designers cite the result for its use in state encoding, error correction, and combinatorial search. The proof is a one-line wrapper that invokes the GrayCodeFacts hypothesis envelope.
Claim. For all natural numbers $d$ and $n$ satisfying $n+1 < 2^d$, there exists a unique $k < d$ such that the $k$-th bit of $n$ XOR $(n$ right-shift $1)$ differs from the $k$-th bit of $(n+1)$ XOR $((n+1)$ right-shift $1)$.
background
The module declares classical Gray code properties as axioms pending full bitwise formalization. The binary-reflected Gray code is defined by gray(n) = n XOR (n >> 1), with the inverse obtained by successive XORs of right-shifts. GrayCodeFacts serves as the hypothesis envelope containing this and related inversion lemmas such as grayToNat_inverts_natToGray.
proof idea
One-line wrapper that applies GrayCodeFacts.gray_code_one_bit_property.
why it matters
The declaration populates the GrayCodeFacts class and is invoked by brgc_oneBit_step to establish OneBitDiff along brgcPath. It encodes the classical result from Savage (1997) Theorem 2.1 and Knuth (2011) Theorem 7.2.1.1.A, supplying the defining one-bit transition property while the module awaits complete formalization of bitwise operations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.