Patterns Gray Code Gray To Nat

The inverse mapping

The binary-reflected Gray code is a way of ordering the binary representations of the numbers from 0 to 2^d − 1 so that consecutive entries differ in exactly one bit. This ordering matters in hardware and communications, where flipping several bits at once can cause errors. The standard encoding of a natural number n into Gray code is the bitwise operation g = n XOR (n >> 1). The declaration grayToNat provides the inverse: given a Gray-coded value g, it recovers the original natural number n.

The inverse works by repeatedly XORing g with itself shifted right by successive amounts. For a value that fits in 64 bits, the declaration runs this operation for shifts from 1 up to 64, which is enough to recover any number in that range. The definition is constructive: it gives a concrete algorithm rather than merely asserting that an inverse exists. This matters because the forward encoding n XOR (n >> 1) is its own inverse in a limited sense, but the general recovery needs the full shift-and-XOR loop to cancel every overlapping bit.

In Recognition Science, this declaration belongs to the framework's treatment of patterns as discrete structures. The framework models recognition, a forced cost of distinguishing one state from another, as the primitive from which physical constants and dimensions are derived. Within that account, Gray code appears as a natural way to order the vertices of a hypercube so that adjacent vertices differ by one bit, which is exactly the structure of a Hamiltonian cycle on the d-dimensional cube. The declaration grayToNat is the bookkeeping that lets the framework move between a Gray-coded pattern and the natural number it indexes.

What grayToNat does not claim is more limited than the surrounding framework. The declaration does not prove that every natural number has a unique Gray code, nor does it establish the Hamiltonian cycle property of the binary-reflected construction. Those are separate theorems about the encoding as a whole. The declaration also does not connect Gray code to the forcing chain that derives physical constants; it is a standalone utility for pattern indexing, not a step in that derivation.

/-- 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.

/-- 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.

/-- 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 declaration does not prove uniqueness of Gray codes for all natural numbers. The declaration does not establish the Hamiltonian cycle property of the binary-reflected construction. The declaration does not connect Gray code to the derivation of physical constants.

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: