natToGray
The natToGray definition supplies the standard binary-reflected Gray code encoding of natural numbers via bitwise XOR with a right shift. Researchers working on hypercube Hamiltonian paths or pattern generation in discrete structures would cite this as the core conversion step. The implementation is a direct one-line definition matching the classical formula.
claimThe map $g : ℕ → ℕ$ given by $g(n) := n ⊕ (n ≫ 1)$, where ⊕ denotes bitwise XOR and ≫ denotes right shift, converts a natural number to its binary-reflected Gray code representation.
background
The module Patterns.GrayCode implements the binary-reflected Gray code (BRGC) that generates a Hamiltonian cycle on the d-dimensional hypercube Q_d. A Pattern d is defined as Fin d → Bool, representing d-bit strings; upstream modules such as Streams and Measurement define Pattern (n : Nat) as Fin n → Bool with an associated Z functional counting ones in the window. The PrimitiveDistinction.from theorem reduces seven independent axioms to four structural conditions plus three definitional facts, while ContinuumBridge.as identifies the Laplacian action with simplicial ledger measures via (1/2) Σ w_ij (ε_i − ε_j)² = (1/κ) Σ δ_h A_h.
proof idea
This is a direct definition implementing the classical formula gray(n) = n XOR (n >>> 1). No lemmas are applied; it serves as the primitive conversion used by binaryReflectedGray to extract bits into Pattern d.
why it matters in Recognition Science
This definition is the foundation for binaryReflectedGray, which in turn supports brgcPath_injective and brgc_oneBit_step in GrayCycleGeneral, establishing that the BRGC path is injective and that consecutive elements differ by one bit. It fills the role of the standard encoding in the construction of Hamiltonian cycles on hypercubes, as described in the module documentation. It enables the cycle properties used in pattern recognition without touching open questions in the forcing chain.
scope and limits
- Does not establish any invertibility or cycle properties of the encoding.
- Does not restrict the input domain or bound the bit width.
- Does not connect to Recognition Science constants, J-cost, or the phi-ladder.
- Does not handle non-natural inputs or alternative Gray code variants.
Lean usage
def grayExample (d : Nat) (i : Fin (2 ^ d)) : Pattern d := binaryReflectedGray d iformal statement (Lean)
30def natToGray (n : ℕ) : ℕ := n ^^^ (n >>> 1)
proof body
Definition body.
31
32/-- Binary-reflected Gray code as a function from Fin (2^d) to Pattern d
33 We use the standard bit-extraction to convert Gray code to pattern -/