brgcPath
plain-language theorem explainer
brgcPath recursively constructs the binary-reflected Gray code as a map from Fin (2^d) to d-bit patterns. Researchers building axiom-free Gray cycles or covers in finite Boolean spaces cite it for the standard recursive implementation. The definition proceeds by case split on dimension, using Fin.append to join the direct subpath with appended false and the reversed subpath with appended true.
Claim. The function $brgcPath(d) : Fin(2^d) → (Fin d → Bool)$ is defined by $brgcPath(0, i)$ as the constant false map on the single 0-dimensional pattern, and for successor dimension $d+1$ by splitting the index range into two halves of size $2^d$, mapping the first half via snocBit applied to the lower path with false appended and the second half via snocBit applied to the reversed lower path with true appended.
background
In the module, Pattern d is the type (Fin d → Bool) of d-bit strings. snocBit p b appends bit b as the final coordinate of pattern p. The supporting lemma twoPow_succ_eq_add states that 2^(d+1) equals 2^d + 2^d, allowing the index Fin range to be partitioned for the recursive step. The module documentation states that this supplies an axiom-free general-D Gray cycle construction via the recursion BRGC(0) = [0] and BRGC(d+1) = [0·BRGC(d), 1·(BRGC(d)) reversed], independent of any bitwise gray-code formula.
proof idea
The definition is given by pattern matching on the dimension parameter. The zero case returns the constant false function. The successor case computes T := 2^d, casts the input index via the equality 2^(d+1) = T + T, defines left and right branches by applying snocBit to the recursive call and its Fin.rev, then selects the appropriate branch with Fin.append.
why it matters
This definition supplies the concrete path used by brgcGrayCycle and brgcGrayCover in the same module, and is imported into GrayCycleGeneral for the bounded case. It directly realizes the recursive BRGC construction quoted in the module documentation, enabling the subsequent proofs of injectivity and one-bit adjacency that package the GrayCycle and GrayCover structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.