Patterns Gray Code Axioms Gray Code One Bit Property

The one-bit property

A Gray code, named after Frank Gray who patented it in 1953, is an ordering of the binary representations of the numbers from 0 to 2^d − 1 such that any two consecutive numbers differ in exactly one bit position. The standard construction, called the binary-reflected Gray code, computes the code for a natural number n as n XOR (n shifted right by one bit). Its defining property is that the codes for n and n+1 differ in exactly one bit, which makes the sequence useful in digital systems where a single-bit change avoids transient errors, and in error correction and computer graphics.

The machine-checked library of formal theorems in Recognition Science records this property as a declaration named gray_code_one_bit_property. In plain language, the declaration states that for any bit width d and any number n such that n+1 is still within the d-bit range, there exists a unique bit position k below d where the Gray code of n and the Gray code of n+1 differ. The proof is classical: the XOR of the two consecutive Gray codes simplifies to a single power of two, the bit at the position of the least significant zero in n. The library declares this as an axiom pending full bitwise formalization, so the declaration is a stated hypothesis envelope rather than a fully machine-checked derivation from first principles.

What the declaration does not claim is just as important. It does not claim that the one-bit property holds for all natural numbers without a bound; the declaration explicitly requires n+1 to be less than 2^d, so it covers only the finite d-bit range. It also does not claim that the Gray code is the only ordering with this property, nor does it establish any connection between Gray codes and the broader Recognition Science framework's cost functions or forcing chain. The library itself labels these results as classical and pending formalization, so the declaration is a record of a known combinatorial fact, not a new derivation.

/-- **Classical Result**: Consecutive Gray codes differ in one bit.

For any n < 2^d - 1, gray(n) and gray(n+1) differ in exactly one bit position.

**Proof**:
- gray(n) XOR gray(n+1) = [n XOR (n>>1)] XOR [(n+1) XOR ((n+1)>>1)]
- This simplifies to a single power of 2 (bit at position of least significant 0 in n)

**References**:
- Savage (1997), Theorem 2.1
- Knuth (2011), Theorem 7.2.1.1.A

**Status**: Defining property of Gray codes
-/
theorem gray_code_one_bit_property :
  ∀ (d n : ℕ), n + 1 < 2^d →
    ∃! k : ℕ, k < d ∧
      (n ^^^ (n >>> 1)).testBit k ≠ ((n+1) ^^^ ((n+1) >>> 1)).testBit k :=
  GrayCodeFacts.gray_code_one_bit_property

What this page does not claim

The declaration does not claim the one-bit property holds for all natural numbers without a finite bit-width bound. The declaration does not prove that the Gray code is the only ordering with the one-bit property. The declaration does not connect Gray codes to the Recognition Science cost functions or forcing chain.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Patterns/GrayCodeAxioms.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: