brgcGrayCycle
plain-language theorem explainer
The definition packages the recursive binary-reflected Gray code into a GrayCycle structure for any dimension d > 0. Combinatorialists studying Hamiltonian cycles on hypercubes cite this explicit construction. It assembles the path map, its injectivity, and the one-bit adjacency property by direct field assignment from the supporting lemmas.
Claim. For each natural number $d > 0$, the recursive BRGC yields a cycle map $Fin(2^d) → Pattern d$ that is injective and satisfies OneBitDiff between consecutive images (including wrap-around).
background
GrayCycle d is the structure whose fields are a path : Fin(2^d) → Pattern d, an injectivity proof, and a oneBit_step lemma asserting OneBitDiff on consecutive phases. Pattern d is the type of d-bit strings (functions Fin d → Bool). OneBitDiff p q means p and q differ in exactly one coordinate. brgcPath supplies the recursive definition: the base case at d = 0 is the unique empty pattern, while the successor appends a false bit to the prior cycle on the left half and a true bit to the reversed prior cycle on the right half.
proof idea
One-line wrapper that applies brgcPath to the path field, brgcPath_injective d to the inj field, and brgc_oneBit_step (d := d) hdpos to the oneBit_step field.
why it matters
This definition supplies the concrete witness used by exists_grayCycle in GrayCycleGeneral, which asserts existence of a Gray cycle for every d > 0. It completes the axiom-free BRGC construction described in the module, independent of bitwise formulas, and feeds the general pattern results downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.