Patterns Gray Code Binary Reflected Gray

The binary-reflected Gray code

A binary-reflected Gray code is a sequence of all 2^d binary patterns of length d, arranged so that consecutive patterns differ in exactly one bit. The classic construction, attributed to Frank Gray in 1953, builds the sequence recursively: the code for length 0 is just [0]; the code for length n+1 takes the code for length n, prepends a 0 to each pattern, then takes the reversed code, prepends a 1 to each pattern, and concatenates the two halves. For d=2 this yields 00, 01, 11, 10, a cycle that visits all four two-bit patterns while changing one bit per step.

The construction has a direct formula. For a natural number n, its Gray-code value is n XOR (n shifted right by one bit); the n-th entry of the d-bit code is the pattern of bits in that value. The inverse map, turning a Gray code back into an ordinary number, is the repeated XOR of the code with itself shifted by 1, 2, 4, and so on, until no bits remain. The code is a Hamiltonian cycle on the d-dimensional hypercube, meaning it visits every vertex exactly once and returns to its start, a property that makes it useful in rotary encoders, error correction, and digital circuit design where a single-bit change avoids glitches.

In Recognition Science, the machine-checked library of formal theorems defines this construction as a function from the finite set of indices 0 through 2^d - 1 to the set of d-bit patterns. The definition uses the standard formula and the recursive recipe; it is a formal object, not a theorem about recognition. The library also defines the inverse map from Gray code back to natural numbers, using a bounded loop that terminates by construction.

What the declaration does not do is tie Gray codes to the framework's recognition ledger, cost functions, or forcing chain. It is a standalone piece of classical combinatorics, formalized for use elsewhere. The definition itself makes no claim about recognition events, and nothing in the file asserts that Gray codes arise from the framework's axioms. The declaration is a building block, not a result about the framework.

The practical consequence is that a reader can rely on the formal definition as a precise, machine-checked version of the classical construction. The recursive recipe, the XOR formula, and the inverse map are all pinned down exactly, so any later framework theorem that uses Gray codes starts from a fixed, unambiguous object.

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

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

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

What this page does not claim

The declaration does not claim any connection between Gray codes and the recognition ledger or cost functions. No theorem in the file asserts that the Gray code construction is forced by the framework's axioms. The inverse map's termination is guaranteed by a fixed fuel bound of 64 shifts, not by a general proof for all natural numbers.

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: