natToGray
plain-language theorem explainer
The natToGray definition supplies the standard bitwise map sending each natural number n to its binary-reflected Gray code via XOR with a right shift. Pattern theorists and hypercube-cycle researchers in Recognition Science cite it as the primitive conversion step that feeds all subsequent BRGC constructions. The definition is a direct one-line implementation of the classical formula with no additional lemmas.
Claim. The function that converts a natural number $n$ to its binary-reflected Gray code is given by $nopluslfloor n/2rfloor$, where $oplus$ denotes bitwise XOR.
background
The module Patterns.GrayCode implements the binary-reflected Gray code (BRGC) that produces a Hamiltonian cycle on the d-dimensional hypercube. Pattern is defined in sibling modules as Fin d to Bool (a finite window of length d) and appears in Measurement, Streams, and Streams.Blocks as the same type. Upstream results supply the general Pattern alias and the PrimitiveDistinction axioms that underwrite the structural conditions for such encodings.
proof idea
One-line definition that directly encodes the classical formula gray(n) = n XOR (n >>> 1).
why it matters
natToGray is the core conversion used by binaryReflectedGray to produce Pattern d values and by the GrayCycleGeneral lemmas that prove one-bit adjacency, injectivity of brgcPath, and the wrap-around edge. It therefore supplies the concrete map required for the BRGC Hamiltonian-cycle construction described in the module doc-comment. The result sits inside the Patterns domain that Recognition Science employs for discrete encodings before lifting to continuum bridges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.