Patterns Gray Code Axioms Gray To Nat Preserves Bound

The bound preservation theorem

The Gray code, invented by Frank Gray in 1953 (US Patent 2,632,058), is a way of ordering binary numbers so that consecutive values differ in exactly one bit. The standard construction is gray(n) = n XOR (n >> 1), and its inverse, which converts a Gray code back to an ordinary number, is the cumulative XOR of the code with its own shifted bits. The bound preservation theorem states a simple consequence of this construction: if a Gray code g is smaller than 2^d, meaning it fits in d bits, then its inverse grayInverse(g) is also smaller than 2^d. In other words, decoding a d-bit Gray code never produces a number that needs more than d bits to represent.

The theorem is formalized in the framework's machine-checked library of formal theorems as grayToNat_preserves_bound. It states: for all natural numbers g and d, if g < 2^d and d ≤ 64, then grayInverse g < 2^d. The condition d ≤ 64 reflects the implementation detail that the inverse function grayInverse uses a fixed loop of 64 iterations, which is enough to handle any 64-bit Gray code. The proof, as noted in the library's documentation, is elementary bitwise reasoning: XOR operations preserve bit width, so combining a d-bit number with its own shifts cannot produce a result wider than d bits.

This bound property is one of several classical Gray code results that the library declares as axioms pending full bitwise formalization. The library also declares that the inverse is correct on both sides: grayInverse (n XOR (n >> 1)) = n for n < 2^64, and the forward map inverts the inverse. It further declares that consecutive Gray codes differ in exactly one bit, which is the defining property of the code. These are all standard results with multiple published proofs, but in this library they are stated as axioms rather than derived theorems, because the formalization of bitwise induction for natural numbers is not yet complete.

What the theorem does not claim is broader than what it states. It does not claim that the inverse is correct for all natural numbers, only for those below 2^64. It does not claim that the Gray code map is a bijection on all natural numbers, only that within the 64-bit range the two directions invert each other. And it does not claim that the bound holds for arbitrary d without the d ≤ 64 restriction; the theorem explicitly requires that condition. The bound is a local property about bit width, not a global statement about the structure of all Gray codes.

/-- **Classical Result**: Gray code preserves bounds.

If g < 2^d, then grayToNat(g) < 2^d.

**Proof**: XOR operations preserve bit width

**References**: Elementary bit manipulation

**Status**: Simple bitwise reasoning
-/
theorem grayToNat_preserves_bound :
  ∀ g d : ℕ, g < 2^d → d ≤ 64 → grayInverse g < 2^d :=
  GrayCodeFacts.grayToNat_preserves_bound

/-- **Classical Result**: Gray code preserves bounds.

If g < 2^d, then grayToNat(g) < 2^d.

**Proof**: XOR operations preserve bit width

**References**: Elementary bit manipulation

**Status**: Simple bitwise reasoning
-/
theorem grayToNat_preserves_bound :
  ∀ g d : ℕ, g < 2^d → d ≤ 64 → grayInverse g < 2^d :=
  GrayCodeFacts.grayToNat_preserves_bound

/-- **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**: 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 theorem does not claim that the inverse is correct for all natural numbers, only for those below 2^64. The theorem does not claim that the Gray code map is a bijection on all natural numbers. The theorem does not claim that the bound holds for arbitrary d without the d ≤ 64 restriction.

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: