gray_code_one_bit_property
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not define or construct the Gray encoding function.
- Does not treat cases where n+1 is at least 2^d.
- Does not cover non-reflected Gray codes.
- Does not compute the explicit position k.
formal statement (Lean)
146theorem gray_code_one_bit_property :
147 ∀ (d n : ℕ), n + 1 < 2^d →
148 ∃! k : ℕ, k < d ∧
149 (n ^^^ (n >>> 1)).testBit k ≠ ((n+1) ^^^ ((n+1) >>> 1)).testBit k :=
proof body
Term-mode proof.
150 GrayCodeFacts.gray_code_one_bit_property
151
152end GrayCodeAxioms
153end Patterns
154end IndisputableMonolith