brgc_oneBit_step
plain-language theorem explainer
The lemma proves that the binary-reflected Gray code path for d bits (0 < d ≤ 64) yields consecutive patterns differing in exactly one bit, including wrap-around from last to first. Pattern theorists constructing Hamiltonian cycles on hypercubes cite this step when packaging explicit Gray cycles. The proof splits on whether the index wraps modulo 2^d, invoking an external one-bit property for interior steps and reducing the boundary to a dedicated wrap lemma.
Claim. For every natural number $d$ with $0 < d ≤ 64$ and every index $i$ in the set of size $2^d$, the binary-reflected Gray code of $i$ and the binary-reflected Gray code of $i+1$ (modulo $2^d$) differ in exactly one bit position.
background
The module develops Gray cycles for general dimension $d$ via the binary-reflected formula gray(n) = n XOR (n right-shift 1), under the explicit bound $d ≤ 64$ that routes successor adjacency through bitwise axioms. OneBitDiff is the predicate asserting two patterns differ in precisely one coordinate. The local setting is the bounded development, which contrasts with the recursive axiom-free version in the sibling module. The proof draws on the one-bit property for Gray codes and the wrap-around adjacency lemma.
proof idea
The tactic proof opens with intro i and classical, then applies by_cases on whether i.val + 1 < 2^d. The non-wrapping branch invokes gray_code_one_bit_property to extract the unique differing bit k, verifies the difference via Fin.val_add_one_of_lt', and confirms uniqueness by matching against the axiom-supplied witness. The wrapping branch proves i equals the last index via Nat.le_antisymm, shows the successor is zero, and reduces via simpa to the wrap lemma.
why it matters
This lemma supplies the oneBit_step field required to form the GrayCycle structure, which directly yields the packaged brgcGrayCycle and brgcGrayCover objects. Those objects feed the general-d cycle cover used in pattern recognition arguments. In the Recognition framework it supports the D=3 spatial construction and explicit adjacent paths on the phi-ladder. It touches the open question of lifting the d ≤ 64 bound without axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.