oneBitDiff_snocBit_flip
plain-language theorem explainer
The result shows that appending false versus true as the final coordinate to any d-dimensional pattern yields two (d+1)-patterns differing in exactly one position. It is invoked inside the inductive step establishing one-bit adjacency for the BRGC Gray cycle path. The argument exhibits the differing index as the last coordinate and uses Fin.lastCases to obtain a contradiction on all earlier indices.
Claim. For every natural number $d$ and every map $p :$ Fin $d$ $→$ Bool, the two maps from Fin $(d+1)$ to Bool obtained by appending false and true as the highest-index coordinate differ in exactly one position.
background
In this module a Pattern $d$ is a map Fin $d$ $→$ Bool. OneBitDiff $p$ $q$ asserts that there exists a unique coordinate $k$ where $p$ and $q$ disagree. The constructor snocBit $p$ $b$ produces a map on Fin $(d+1)$ that returns $b$ on the last index and otherwise returns the value of $p$ on the corresponding earlier index, implemented via Fin.lastCases.
proof idea
The tactic proof opens with classical, refines the witness to Fin.last $d$, simplifies, then assumes an arbitrary differing index $j$ and performs induction on $j$ via Fin.lastCases. The last case holds by reflexivity. The cast case derives a contradiction because the first $d$ coordinates of both extensions equal those of $p$, violating the assumption that they differ at $j$.
why it matters
The lemma supplies the differing-bit fact needed when the appended bit flips inside the recursive BRGC construction. It is used directly by brgc_oneBit_step, which proves the one-bit adjacency property for the Gray cycle path brgcPath. The module realizes an axiom-free general-$D$ Gray cycle required by the Recognition framework for pattern recognition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.