binaryReflectedGray
The binary-reflected Gray code supplies the explicit map from each index i in Fin(2^d) to a d-bit pattern whose bits are taken from the integer Gray code of i. Researchers constructing Hamiltonian cycles on the hypercube or proving one-bit adjacency in the pattern layer cite this definition. It is realized by a direct bit-extraction wrapper around the natToGray conversion.
claimThe binary-reflected Gray code is the map $BRGC_d : Fin(2^d) → (Fin d → Bool)$ defined by $BRGC_d(i)(j)$ equals the $j$-th bit of $gray(i)$, where $gray(n) = n ⊕ (n ≫ 1)$.
background
In the Patterns.GrayCode module the binary-reflected Gray code realizes the standard recursive construction of a Hamiltonian path on the d-dimensional hypercube. Pattern d denotes the type of functions from Fin d to Bool, equivalently finite binary strings of length d. The auxiliary natToGray converts a natural number n to its Gray-code integer via the formula n XOR (n right-shifted by 1). Upstream, the Pattern abbreviation from Measurement and Streams supplies the window type used throughout the pattern layer.
proof idea
This definition is a one-line wrapper that applies natToGray to the underlying natural number of the Fin index and then extracts the j-th bit via testBit for each coordinate j.
why it matters in Recognition Science
The definition is the core building block for the BRGC path in GrayCycleGeneral, which in turn supports the injectivity theorem brgcPath_injective and the one-bit difference lemmas brgc_oneBit_step and brgc_wrap_oneBitDiff. It fills the concrete realization of the Hamiltonian cycle on the hypercube Q_d required by the pattern axioms. The construction directly implements the recursive BRGC rule given in the module documentation.
scope and limits
- Does not establish the one-bit adjacency property; that is proved in downstream lemmas.
- Does not verify that the map is bijective or surjective.
- Does not extend to d greater than 64.
- Does not handle the zero-dimensional case.
formal statement (Lean)
34def binaryReflectedGray (d : ℕ) (i : Fin (2^d)) : Pattern d :=
proof body
Definition body.
35 fun j => (natToGray i.val).testBit j.val
36
37/-- Inverse Gray code: converts Gray code back to binary -/