brgcGrayCycle
plain-language theorem explainer
This definition packages a Gray cycle of dimension d (0 < d ≤ 64) by assembling the BRGC path with its injectivity and one-bit transition lemmas. Pattern researchers in the Recognition framework cite it when an explicit adjacent cycle is required under the bounded bitwise assumptions. The construction is a direct record assembly that delegates the structural properties to brgcPath_injective and brgc_oneBit_step.
Claim. For each natural number $d$ with $0 < d ≤ 64$, the binary-reflected Gray code supplies a Gray cycle of dimension $d$: an injective map from Fin$(2^d)$ to $d$-dimensional patterns such that consecutive elements (including the wrap-around) differ in exactly one bit.
background
The module develops Gray cycles for general dimension via the bounded BRGC method. A GrayCycle $d$ is the structure consisting of a path function Fin$(2^d) →$ Pattern $d$, an injectivity proof, and a one-bit step proof (including wrap-around). The local setting is the Workstream A generalization that uses the bitwise formula gray$(n) = n$ XOR $(n >>> 1)$ but routes adjacency through GrayCodeAxioms, requiring the $d ≤ 64$ bound.
proof idea
The definition is a one-line record constructor. It populates the path field with brgcPath $d$, the inj field with brgcPath_injective $(d := d)$ hdpos hd, and the oneBit_step field with brgc_oneBit_step $(d := d)$ hdpos hd.
why it matters
This supplies the explicit bounded Gray cycle required by exists_grayCycle_of_le64. It fills the role of a packaged witness under the bitwise axioms while the unconditional general existence is delegated to the recursive construction in GrayCycleBRGC. In the Recognition framework it supports pattern constructions up to the 64-bit limit, consistent with the eight-tick octave and small-$d$ cases such as D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.