brgc_wrap_oneBitDiff
plain-language theorem explainer
The result shows that the binary-reflected Gray code path for positive dimension d maps the all-ones index 2^d - 1 and the zero index to codewords differing in exactly one bit position. Pattern theorists building cyclic Gray covers for general d would cite it to close the wrap-around adjacency. The tactic proof rewrites d as t + 1, selects the highest bit as witness, verifies the difference via testBit and shift lemmas on all-ones numbers, then rules out all other positions by Fin.lastCases induction showing both sides are false.
Claim. For every positive integer $d$, the binary-reflected Gray code word for $2^d - 1$ and the word for $0$ differ in exactly one coordinate.
background
The declaration lives in Patterns.GrayCycleGeneral, the bounded bitwise development of Gray cycles for arbitrary dimension d. It uses the standard BRGC formula gray(n) = n XOR (n >>> 1) and packages the resulting objects as GrayCover d (2^d) and GrayCycle d, with successor adjacency routed through GrayCodeAxioms when d ≤ 64. Core notions are brgcPath, which sends an index to its reflected Gray word, and OneBitDiff, which asserts that two such words differ at precisely one bit position. Sibling lemmas such as allOnes_succ_eq_bit and allOnes_testBit_lt supply the bit-level arithmetic on the all-ones number that the proof invokes.
proof idea
The tactic proof begins by rewriting d as t + 1 via Nat.exists_eq_succ_of_ne_zero. It defines iLast as the Fin index 2^{t+1} - 1 and constructs a OneBitDiff witness by choosing the last bit position Fin.last t. The difference at that position is shown by computing testBit t on natToGray of allOnes(t+1) (true) versus 0 (false), using shift-right identities and allOnes_testBit lemmas. For every other index the proof applies Fin.lastCases induction, establishes that both paths evaluate to false at castSucc positions, and derives a contradiction from the assumed difference.
why it matters
The lemma supplies the wrap-around case required by the downstream brgc_oneBit_step, which together establish the full one-bit adjacency property for the BRGC path. It advances the general-dimension GrayCycle construction in the Patterns workstream, supporting the framework's D = 3 spatial dimension by furnishing cycle covers that remain axiom-free in the core recursive development. The result closes the cyclic aspect of the path, enabling grayCycle objects that realize recognition patterns on discrete spaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.