brgc_oneBit_step
plain-language theorem explainer
The recursive BRGC path satisfies the one-bit adjacency condition for every dimension d greater than zero. Pattern theorists and discrete mathematicians in the Recognition Science setting cite the result to obtain an axiom-free Gray cycle on the space of d-bit patterns. The proof proceeds by induction on dimension, with direct verification for d=1 and case analysis on left and right halves for the inductive step.
Claim. For every natural number $d>0$ and every index $i$ in the finite set of size $2^d$, the recursively defined BRGC path $P_d(i)$ and $P_d(i+1)$ (indices modulo $2^d$) differ in exactly one coordinate.
background
The module builds Gray cycles on the space of binary patterns of length d via the standard recursive BRGC rule: BRGC(0) is the singleton path at the zero pattern, and BRGC(d+1) concatenates the d-path prefixed by 0 with the reversed d-path prefixed by 1. The function brgcPath implements this recursion as a map from Fin(2^d) to Pattern d. OneBitDiff is the predicate asserting that two patterns differ in precisely one bit position. The theorem supplies the required adjacency property (including wrap-around) that turns brgcPath into a GrayCycle d.
proof idea
The proof is by cases on d. The d=1 case verifies the two steps of the cycle 0 to 1 to 0 directly via the snocBit flip lemma and symmetry. The inductive step at d+2 invokes the induction hypothesis for dimension d+1, splits the doubled path into left and right halves with Fin.append, and branches on whether the successor stays inside the left half, crosses the midpoint, or stays inside the right half, applying the appropriate snocBit same or flip lemma together with cast and twoPow_succ_eq_add lemmas to align indices.
why it matters
The lemma supplies the oneBit_step field that lets brgcGrayCycle package the recursive path into a GrayCycle d and lets brgcGrayCover obtain the corresponding GrayCover d (2^d). It is invoked by both the BRGC-specific and the general GrayCycleGeneral modules. Within the Recognition framework the result furnishes the discrete cycle structure for pattern recognition in arbitrary dimension, consistent with the eight-tick octave when d is specialized to 3. The result is fully proved and closes no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.