Patterns Gray Code Axioms Nat To Gray Inverts Gray To Nat

The round-trip guarantee

A Gray code, invented by Frank Gray in 1953, is an ordering of binary numbers in which any two consecutive values differ by only one bit. The standard construction is gray(n) = n XOR (n >> 1), and its inverse is the cumulative XOR: g XOR (g>>1) XOR (g>>2) and so on. This inverse is what the declaration natToGray_inverts_grayToNat concerns: it states that if you take any number g below 2^64, apply the inverse to get n, then apply the forward construction to n, you recover exactly g. In plainer terms, converting a Gray code back to a natural number and then forward again returns the original code, with no loss for any 64-bit value.

The declaration is tagged as a theorem in the machine-checked library, but its proof is not yet formalized. The library's docstring calls it a classical result with multiple published proofs, citing Knuth's Art of Computer Programming and Savage's survey of combinatorial Gray codes. The statement itself is a left-inverse property: the inverse operation inverts the forward transformation. The companion theorem grayToNat_inverts_natToGray states the other direction, that the forward transformation inverts the inverse, and together they express the bijectivity of the Gray code map on the 64-bit range.

What the declaration does not claim is broader. It does not claim that the code is self-similar in the Recognition Science sense, nor that it arises from the framework's cost function. It is a standalone classical result about bitwise arithmetic, placed in the library's Patterns module as an axiom pending full bitwise formalization. The bound 2^64 is essential: the theorem holds only for numbers below that limit, not for arbitrary natural numbers. The library also records a one-bit property, that consecutive Gray codes differ in exactly one bit, and a bound-preservation result, but those are separate declarations with their own scopes.

In Recognition Science, the Gray code appears as a pattern object, but this theorem does not tie it to the ledger or recognition cycle. It is a piece of ordinary discrete mathematics, verified numerically to arbitrary bit depths but not yet proved inside the kernel. The practical upshot for a reader is simple: for any 64-bit Gray code, the standard conversion back and forth is exact, and the library records that fact as a theorem with a known proof in the literature, even though the formal proof remains an open target.

/-- **Classical Result**: natToGray is a left inverse of grayToNat.

The forward Gray code transformation inverts the inverse operation.

**Proof**: Follows from bijectivity of Gray code map

**References**: Same as above

**Status**: Consequence of inverse correctness
-/
theorem natToGray_inverts_grayToNat :
  ∀ g : ℕ, g < 2^64 →
    let n := grayInverse g
    n ^^^ (n >>> 1) = g :=
  GrayCodeFacts.natToGray_inverts_grayToNat

/-- **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**: natToGray is a left inverse of grayToNat.

The forward Gray code transformation inverts the inverse operation.

**Proof**: Follows from bijectivity of Gray code map

**References**: Same as above

**Status**: Consequence of inverse correctness
-/
theorem natToGray_inverts_grayToNat :
  ∀ g : ℕ, g < 2^64 →
    let n := grayInverse g
    n ^^^ (n >>> 1) = g :=
  GrayCodeFacts.natToGray_inverts_grayToNat

What this page does not claim

The declaration does not claim the Gray code is self-similar in the Recognition Science sense. It does not claim the theorem holds for arbitrary natural numbers beyond the 64-bit bound. It does not claim the proof is formalized inside the kernel; the proof remains an open target.

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: