Patterns Gray Code Nat To Gray

The Gray code map

The binary-reflected Gray code, introduced by Frank Gray in 1953, is a sequence of binary numbers in which any two consecutive entries differ in exactly one bit. The standard formula to convert an ordinary binary number n into its Gray code is g = n XOR (n >> 1), where XOR is the bitwise exclusive-or and >> is a right shift by one position. For example, n = 3 (binary 011) becomes g = 011 XOR 001 = 010, which is 2. The inverse operation, recovering n from g, is performed by repeatedly XORing with shifted versions of g until the shifts run out of bits.

The construction has a clean recursive description. Start with the one-bit list [0, 1]. To extend a list of d-bit patterns to d+1 bits, take the existing list, prepend a 0 bit to each entry, then take the reversed list and prepend a 1 bit to each entry. This produces a list of all 2^d patterns of length d, and it has three defining properties: it visits every d-bit pattern exactly once, consecutive entries differ in one bit, and the first and last entries also differ in one bit, so the list wraps into a cycle. That cycle is a Hamiltonian cycle on the d-dimensional hypercube, a path that touches every vertex exactly once and returns to the start.

In the recognition framework, where a ledger records discrete events and their costs, the Gray code appears as a natural way to order patterns. The framework's machine-checked library of formal theorems defines natToGray as the function g = n XOR (n >> 1), and it defines binaryReflectedGray as the corresponding pattern of d bits for each index i in the finite set Fin (2^d). The inverse map grayToNat is also defined, using a bounded loop of 64 shifts to recover the original number. These definitions are exactly the classical Gray code, not a new invention.

What the framework's definitions do not do is derive the Gray code from first principles. The code is not forced by any cost function or recognition theorem; it is a chosen construction, a definitional choice made because the code's single-bit transitions fit the framework's interest in minimal-change sequences. The definitions also do not prove that the code is optimal in any sense, nor do they connect the Gray code to the golden ratio or the forcing chain that produces other constants. They simply provide a formal, machine-checked implementation of a standard combinatorial object.

The practical payoff is that the framework can reason about Gray code sequences without hand-waving about bit operations. A reader who wants to know whether a given list of patterns is a valid Gray code, or how to invert one, can check the formal definitions. The framework's contribution is precision, not novelty: it takes a 70-year-old construction and makes it part of a machine-checked library, so that any later theorem about patterns can rely on the code's properties without re-proving them from scratch.

/-- Convert a natural number to its Gray code representation
    The standard formula: gray(n) = n XOR (n >> 1) -/
def natToGray (n : ℕ) : ℕ := n ^^^ (n >>> 1)

/-- Binary-reflected Gray code as a function from Fin (2^d) to Pattern d
    We use the standard bit-extraction to convert Gray code to pattern -/
def binaryReflectedGray (d : ℕ) (i : Fin (2^d)) : Pattern d :=
  fun j => (natToGray i.val).testBit j.val

/-- Inverse Gray code: converts Gray code back to binary -/
def grayToNat (g : ℕ) : ℕ :=
  -- Inverse Gray code: repeatedly XOR with shifted versions
  -- g XOR (g >> 1) XOR (g >> 2) XOR ...
  -- For bounded values, this terminates
  let rec aux (shift : ℕ) (acc : ℕ) (fuel : ℕ) : ℕ :=
    match fuel with
    | 0 => acc
    | fuel' + 1 =>
      let shifted := g >>> shift
      if shifted = 0 then acc
      else aux (shift + 1) (acc ^^^ shifted) fuel'
  aux 0 0 64  -- 64 shifts is enough for any practical number

-- Properties and classical results are provided via
-- `IndisputableMonolith.Patterns.GrayCodeAxioms.GrayCodeFacts`.
-- This module remains axiom-free and parametric over those facts.

What this page does not claim

The Gray code is not derived from the recognition cost function or any forcing theorem. The framework does not prove that the Gray code is optimal for any application. No connection is made between the Gray code and the golden ratio or the 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/GrayCode.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: