Patterns Gray Code Axioms

Gray code axioms

A Gray code, also called a reflected binary code, is an ordering of the binary representations of numbers so that any two consecutive numbers differ in exactly one bit position. Frank Gray patented the standard construction in 1953 (US Patent 2,632,058) for pulse code communication. The usual formula is gray(n) = n XOR (n >> 1), where XOR is the bitwise exclusive-or and >> shifts bits right. The inverse operation, recovering the original number from a Gray code, is a cumulative XOR: binary(g) = g XOR (g>>1) XOR (g>>2) XOR .... These codes appear in rotary encoders, error correction, and computer graphics because a single-bit change prevents ambiguous readings during transitions.

The defining property is that consecutive Gray codes differ in exactly one bit. For the binary-reflected construction, this follows because gray(n) XOR gray(n+1) simplifies to a single power of two, the bit at the position of the least significant zero in n. This property is what makes the code useful in physical systems: if a mechanical encoder misreads one bit during a transition, the error is at most one step. The inverse and forward maps are exact inverses of each other, so no information is lost in the conversion.

In Recognition Science, the Gray code appears as a way to index patterns on a discrete ledger, a record of recognition events. The module Patterns.GrayCodeAxioms declares standard Gray code properties as axioms, pending a full bitwise formalization. It states that for numbers below 2^64, the inverse Gray code operation correctly inverts the forward transformation, and that converting a d-bit pattern to a number always yields a value below 2^d. These facts are classical results in discrete mathematics, with published proofs in Knuth's Art of Computer Programming and Savage's survey of combinatorial Gray codes.

The module also records the one-bit property as a theorem: for any n and d with n+1 < 2^d, there exists a unique bit position k < d where gray(n) and gray(n+1) differ. This is the defining property of a Gray code, and here it is stated with an explicit uniqueness condition. The axioms are not proved inside the framework; they are declared as assumptions to be discharged later when bitwise induction infrastructure is available. The practical consequence is that the framework can already reason about pattern indexing and bounds, while the deeper bit-level proofs remain a formalization target.

/-- **Classical Result**: Gray code inverse is a left inverse.

The inverse Gray code operation (cumulative XOR) correctly inverts the forward
Gray code transformation.

**Proof**: Induction on bit positions with XOR algebra

**References**:
- Knuth (2011), Exercise 7.2.1.1.4
- Savage (1997), Section 2.1

**Formalization Blocker**: Requires bitwise induction infrastructure for Nat

**Status**: Standard result in discrete mathematics
-/
theorem grayToNat_inverts_natToGray :
  ∀ n : ℕ, n < 2^64 → grayInverse (n ^^^ (n >>> 1)) = n :=
  GrayCodeFacts.grayToNat_inverts_natToGray

/-- **Classical Result**: Pattern to number conversion bound.

Converting a d-bit pattern to a number gives a value < 2^d.

**Proof**: Sum of 2^i for i < d equals 2^d - 1 < 2^d

**References**: Elementary combinatorics

**Status**: Straightforward calculation
-/
theorem pattern_to_nat_bound :
  ∀ (d : ℕ) (p : Pattern d),
    (∑ k : Fin d, if p k then 2^(k.val) else 0) < 2^d :=
  GrayCodeFacts.pattern_to_nat_bound

/-- **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 Gray code properties are proved inside the framework; they are declared as axioms pending formalization. The Gray code is derived from the recognition cost function or the forcing chain. The module establishes any new mathematical result about Gray codes beyond classical published facts.

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: