oneBitDiff_snocBit_flip
plain-language theorem explainer
For any pattern p of dimension d the two extensions formed by appending false versus true as the final coordinate differ in exactly one position. This internal lemma closes the inductive step when building one-bit-adjacent paths via the BRGC recursion. The proof exhibits the differing index as Fin.last d and derives a contradiction on all earlier indices by direct comparison of the original patterns.
Claim. Let $p$ be a map from Fin $d$ to Bool. The two maps of type Fin $(d+1)$ to Bool obtained by appending false and true respectively differ in exactly one coordinate: there exists a unique $k$ in Fin $(d+1)$ such that the two maps disagree at $k$.
background
Pattern $d$ is the type Fin $d$ to Bool. OneBitDiff $p$ $q$ asserts that $p$ and $q$ differ in exactly one coordinate, formalized as an exists-unique quantifier over Fin $d$. snocBit $p$ $b$ produces the pattern of dimension $d+1$ that returns $b$ on the last index and otherwise copies $p$ on the preceding indices, using Fin.lastCases to perform the case split. The module constructs Gray cycles for arbitrary dimension by the recursive BRGC rule BRGC$(d+1)$ = [0·BRGC($d$), 1·(BRGC($d$)) reversed], proving injectivity and one-bit adjacency without axioms or the bitwise gray-code formula.
proof idea
The tactic proof opens with classical, then refines the exists-unique witness to Fin.last $d$. The first obligation is discharged by simp. The second obligation proceeds by induction on the test index $j$ via Fin.lastCases: the last case is immediate by reflexivity; the cast case produces a contradiction because the two snocBit patterns agree on all original coordinates, so the supplied inequality $hj$ is impossible.
why it matters
The lemma is invoked inside brgc_oneBit_step, which in turn supplies the adjacency property required to package brgcPath into a GrayCycle $d$. It therefore participates in the axiom-free construction of Gray cycles for general $D$ that the module advertises. No open scaffolding is closed here; the result is fully proved and internal to the recursion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.