oneBitDiff_snocBit_flip
plain-language theorem explainer
The declaration shows that appending false versus true as the final coordinate to any d-dimensional pattern yields two (d+1)-dimensional patterns differing in exactly one position. Researchers constructing recursive Gray cycles cite it to verify adjacency under the BRGC recursion. The proof exhibits the last coordinate as the unique witness and uses Fin.lastCases induction to obtain an immediate contradiction on all prior coordinates.
Claim. For every natural number $d$ and every map $p : Fin d → Bool$, the two maps obtained by appending false and true as the final coordinate differ in exactly one position.
background
In this module patterns are maps from Fin d to Bool. The snocBit operation extends such a map by appending a new final coordinate b, defined via Fin.lastCases so that the new coordinate is b and the prefix recovers the original p. OneBitDiff asserts that two patterns differ in exactly one coordinate, i.e., there exists a unique k in Fin (d+1) at which they disagree (Hamming distance 1).
proof idea
The tactic proof opens with classical reasoning and refines the existential witness to Fin.last d. After simp it performs induction on the test coordinate j via Fin.lastCases. The last case is reflexivity. The cast case derives False because the two snocBit patterns agree on every original coordinate, contradicting the assumption hj.
why it matters
This lemma is invoked by brgc_oneBit_step to establish consecutive one-bit steps along the BRGC path. It supplies the adjacency step inside the recursive construction BRGC(d+1) = [0·BRGC(d), 1·(BRGC(d))ʳ] that yields an axiom-free GrayCycle for arbitrary dimension. The result therefore supports the pattern layer used throughout the Recognition forcing chain and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.