gray_code_one_bit_property
plain-language theorem explainer
The theorem asserts that for natural numbers d and n with n+1 less than 2 to the d, the binary-reflected Gray encodings of n and n+1 differ in exactly one bit position. Combinatorialists and hardware designers working on reflected codes or single-transition sequences cite this as the central property of the binary-reflected Gray code. The proof is a one-line wrapper that pulls the corresponding field from the GrayCodeFacts hypothesis envelope.
Claim. For all natural numbers $d$ and $n$ with $n+1 < 2^d$, there exists a unique natural number $k < d$ such that the $k$-th bit of $n$ XOR $(n$ right-shifted by 1$)$ differs from the $k$-th bit of $(n+1)$ XOR $((n+1)$ right-shifted by 1$)$.
background
The module Patterns.GrayCodeAxioms records classical Gray-code facts as axioms pending full bitwise formalization. The binary-reflected Gray code is constructed by gray(n) = n XOR (n right-shifted by 1). GrayCodeFacts is the hypothesis envelope that packages the inversion lemmas and the one-bit difference property.
proof idea
The proof is a one-line wrapper that applies the gray_code_one_bit_property field of the GrayCodeFacts class.
why it matters
This result populates the GrayCodeFacts envelope and is used by brgc_oneBit_step to guarantee one-bit transitions along Gray-code paths. It encodes the defining property of binary-reflected Gray codes, as stated in the module references to Savage (1997) Theorem 2.1 and Knuth (2011) Theorem 7.2.1.1.A. Within the Recognition framework it supplies a verified combinatorial primitive for pattern constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.