brgc_oneBit_step
plain-language theorem explainer
The lemma establishes that the binary-reflected Gray code path on d bits yields consecutive patterns differing in exactly one coordinate, for every d with 1 ≤ d ≤ 64 and including the wrap-around from the final index back to zero. Pattern theorists constructing explicit Gray cycles on hypercube vertices would cite the result to certify adjacency in the BRGC construction. The argument splits on whether the index wraps, reduces the interior steps to the Gray-code one-bit axiom, and handles the wrap by reduction to a dedicated wrap lemma.
Claim. For every natural number $d$ satisfying $0 < d ≤ 64$, and for every index $i$ in the finite set of cardinality $2^d$, the binary-reflected Gray code path at $i$ and at the successor index $i+1$ (taken modulo $2^d$) differ in exactly one bit position.
background
The module Patterns.GrayCycleGeneral supplies GrayCycle and GrayCover objects for arbitrary dimension d via the bounded BRGC formula gray(n) = n XOR (n >>> 1), under the explicit hypothesis d ≤ 64. A GrayCycle d is an injective map from Fin(2^d) to the space of d-bit patterns such that every consecutive pair, including the wrap from last to first, differs in precisely one bit. The local setting routes the one-bit property through the GrayCodeAxioms interface rather than proving it internally. This lemma populates the oneBit_step field demanded by the GrayCycle structure definition.
proof idea
The proof introduces the index i and performs classical case split on whether i.val + 1 < 2^d. In the non-wrapping branch it invokes GrayCodeAxioms.gray_code_one_bit_property to extract the unique differing bit k, builds the corresponding Fin d, and verifies both the bit flip and uniqueness by direct expansion of the testBit expressions after substitution of the successor value. In the wrapping branch it proves i equals the last index via antisymmetry of ≤, then reduces the claim to brgc_wrap_oneBitDiff by Fin extensionality.
why it matters
The lemma discharges the oneBit_step obligation inside brgcGrayCycle and brgcGrayCover in the same module, which package the bounded GrayCycle instances. Those definitions are in turn referenced by the recursive BRGC construction in GrayCycleBRGC to obtain the axiom-free general-d GrayCycle. Within the Recognition framework the result supports the Patterns layer that encodes adjacency on finite sets, supplying the concrete one-bit steps needed before specialization to d = 3 or integration with higher structures such as the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.