brgcGrayCover
plain-language theorem explainer
brgcGrayCover packages the recursive BRGC path into a GrayCover structure for any dimension d greater than zero. It supplies a surjective path of length 2^d on the set of all d-bit strings together with one-bit adjacency at every step. Researchers needing explicit Gray cycles for pattern measurement or finite-state coverings cite this construction. The definition assembles the path from brgcPath, derives surjectivity from injectivity plus matching cardinalities, and obtains adjacency directly from the one-bit step lemma.
Claim. For every natural number $d > 0$, the map $p = $ brgcPath$(d) :$ Fin$(2^d) $to$ Pattern$(d)$ yields a Gray cover of period $2^d$. The path is surjective onto all $d$-bit strings and satisfies the one-bit difference condition between $p(i)$ and $p(i+1)$ for every $i$.
background
Pattern d is the type Fin d to Bool, the set of all $2^d$ binary strings of length d. GrayCover d T is the structure whose fields are a path function Fin T to Pattern d, a surjectivity proof, and a one-bit adjacency proof for consecutive positions (including wrap-around). card_pattern states that the cardinality of Pattern d equals $2^d$ exactly. brgcPath is the recursive construction BRGC(0) = [0], BRGC(d+1) = [0 concatenated with BRGC(d), 1 concatenated with the reverse of BRGC(d)]. brgcPath_injective and brgc_oneBit_step supply the supporting lemmas on injectivity and adjacency.
proof idea
The definition is a one-line wrapper. It sets the path field to brgcPath d. Surjectivity is proved by invoking brgcPath_injective to obtain injectivity, applying card_pattern to match cardinalities, then using Fintype.bijective_iff_injective_and_card to conclude bijectivity and hence surjectivity. The oneBit_step field is supplied directly by the theorem brgc_oneBit_step d hdpos.
why it matters
This definition supplies the concrete GrayCover instance required by the general existence theorem exists_grayCover in GrayCycleGeneral. That theorem asserts a Gray cover of period $2^d$ exists for every d > 0; the present construction discharges the witness. It realizes the axiom-free Gray cycle construction described in the module, independent of bitwise formulas, and feeds downstream results that package the same object for dimensions up to 64.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.