Patterns Gray Code

Gray code as a recognition pattern

Gray code, named after Frank Gray who patented it in 1953, is a binary numeral system where two successive values differ in only one bit. The standard binary counting sequence can change many bits at once, for example from 0111 to 1000 changes all four bits. Gray code avoids that: the sequence for two bits is 00, 01, 11, 10, and each step flips exactly one bit. The most common form is the binary-reflected Gray code, built recursively by taking the previous list, then appending its reverse with a leading 1. This construction produces a Hamiltonian cycle on the d-dimensional hypercube: it visits all 2^d vertices exactly once, consecutive entries differ in exactly one bit, and the first and last entries also differ in exactly one bit, closing the cycle.

The conversion between ordinary binary and Gray code is a simple bitwise formula: gray(n) = n XOR (n >> 1). The inverse operation, recovering n from its Gray code, is done by repeatedly XORing with shifted versions of the code until the shifted value becomes zero. The framework's library implements both directions in a machine-checked collection of formal theorems, with the conversion functions defined for natural numbers and for fixed-width patterns.

In Recognition Science, a ledger is a discrete record of events, and a recognition is the act of matching a new event against that record. The framework models the set of possible states a ledger can hold as binary patterns of a fixed length. Gray code provides a natural ordering for those states: it lists every possible pattern exactly once, and moving from one state to the next changes only one bit. The module binaryReflectedGray defines this ordering as a function from an index to a pattern, and the library proves that this function is a bijection onto the set of all patterns, that consecutive patterns differ in exactly one bit, and that the first and last patterns also differ in exactly one bit, forming a cycle.

What this establishes in plain language is that the space of all possible recognition states can be traversed in a single continuous loop where each step is a minimal change. That property matters because it gives a way to enumerate states without ever making a large jump, which is useful for error detection, for incremental search, and for ordering the states of a system that changes one component at a time. The module does not claim that recognition itself must follow Gray code, only that Gray code offers a well-defined ordering that the framework can use when it needs to step through all possible patterns efficiently.

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

Recognition events must follow Gray code order. Gray code is the only ordering the framework uses. The framework proves that Gray code is optimal for any recognition task.

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: