brgcPath
plain-language theorem explainer
The binary reflected Gray code supplies an explicit path through all 2^d binary patterns of length d, with each step differing by exactly one bit. Researchers working on Gray code constructions in the Recognition Science patterns module would cite this definition when packaging a GrayCover or GrayCycle for arbitrary dimension. The definition is a direct one-line wrapper that applies the binaryReflectedGray function to the input index.
Claim. The BRGC path is the function sending each index $i$ in the finite set of size $2^d$ to the $d$-bit pattern obtained from the binary reflected Gray code encoding of $i$, where the set of $d$-bit patterns is equipped with the one-bit difference relation.
background
The module Patterns.GrayCycleGeneral develops Gray cycles for general dimension $d$ via the bounded BRGC construction. Pattern $d$ denotes the type of all binary strings of length $d$, and the BRGC path is defined using the formula gray(n) = n XOR (n >>> 1). The construction requires $d ≤ 64$ and relies on GrayCodeAxioms for adjacency properties. This is the Workstream A generalization, contrasting with the axiom-free recursive construction in GrayCycleBRGC. Upstream dependencies include foundational definitions such as one from IntegersFromLogic and step from CellularAutomata, providing the discrete structures and iteration mechanisms underlying the patterns. The module documentation states that the construction is definitional and intentionally bounded, with the canonical axiom-free version routed to GrayCycleBRGC.
proof idea
The definition is a one-line wrapper that applies the binaryReflectedGray function directly to the input index i of type Fin (2 ^ d).
why it matters
This definition provides the core path function for constructing brgcGrayCover and brgcGrayCycle, which package it with injectivity and one-bit step properties. It supports the general-d case in the Recognition Science patterns framework, enabling Gray cycles under bounded assumptions while the D=3 case remains fully axiom-free in Patterns.GrayCycle. It contributes to the combinatorial foundations that interface with discrete pattern structures in the broader theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.