binaryReflectedGray
plain-language theorem explainer
Binary-reflected Gray code converts each index i from 0 to 2^d minus 1 into a d-bit pattern by extracting bits from the Gray code of i. Researchers on hypercube Hamiltonians and single-bit adjacent sequences cite this construction. The definition is a direct one-line wrapper applying the natural-number Gray code conversion followed by bit extraction.
Claim. The map sending each index $i$ in the set of size $2^d$ to the pattern $p$ in the set of functions from a $d$-element index set to Boolean values, where the $j$-th component of $p$ equals the $j$-th bit of the Gray code of the value of $i$, and the Gray code of a natural number $n$ is obtained by the bitwise XOR of $n$ with its right shift by one.
background
The module introduces the binary-reflected Gray code as the standard recursive construction that produces a Hamiltonian cycle on the $d$-dimensional hypercube. Pattern $d$ is defined as the set of functions from Fin $d$ to Bool, equivalently finite binary strings of length $d$; the same abbreviation appears in Measurement and Streams as finite windows of length $n$. The sibling definition natToGray supplies the integer conversion $n$ XOR $(n$ right-shift $1)$, which is the core of the bit-extraction step here.
proof idea
One-line wrapper that applies natToGray to the index value and then extracts the required bit via testBit.
why it matters
This definition supplies the explicit function used by brgcPath, which in turn supports the injectivity theorem brgcPath_injective and the one-bit difference results brgc_oneBit_step and brgc_wrap_oneBitDiff. It realizes the construction step described in the module documentation for generating cycles that visit all $2^d$ vertices with consecutive entries differing in one bit. The placement connects the arithmetic substrate (back embedding) to pattern-level cycle properties in the Gray code axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.