oneBitDiff_snocBit_same
This lemma shows that appending an identical bit b to each of two patterns preserves their single-bit difference. It is invoked in the inductive construction of the binary-reflected Gray code path to maintain adjacency at each recursion level. The proof extracts the original differing index, lifts it via castSucc, and dispatches the new final coordinate by contradiction while reducing earlier coordinates to the input uniqueness.
claimLet $p, q$ be patterns of length $d$. If $p$ and $q$ differ in exactly one coordinate, then for any bit $b$, the patterns formed by appending $b$ to both $p$ and $q$ differ in exactly one coordinate.
background
A Pattern $d$ is a finite window of length $d$, realized as a function from Fin $d$ to Bool. OneBitDiff $p$ $q$ asserts that $p$ and $q$ differ at precisely one index $k$, together with a uniqueness statement that no other index differs. The snocBit operation appends a fixed Boolean value to the end of a pattern, producing a pattern of length $d+1$. This lemma sits inside the axiom-free recursive BRGC construction: brgcPath builds the path for dimension $d+1$ by appending false to the left half and true to the reflected right half of the dimension-$d$ path.
proof idea
The tactic proof introduces the hypothesis and rcases it to obtain the differing index $k$ and its uniqueness. It refines the goal to the castSucc index together with two subgoals. The first subgoal is discharged by simpa. The second subgoal proceeds by induction on the candidate index $j$ via Fin.lastCases: the last case yields an immediate contradiction because the appended bits are identical, while the cast case reduces the difference to the original patterns and invokes uniqueness to conclude equality of indices.
why it matters in Recognition Science
The result is applied directly in brgc_oneBit_step to establish one-bit adjacency along consecutive elements of the BRGC path for every $d>0$. It thereby completes the verification that the recursive construction yields a Gray cycle (injective path with one-bit steps and wrap-around). In the Recognition Science setting this supplies the combinatorial substrate for Pattern-based measurement and the simplicial ledger used in the forcing chain (T0-T8) and the Recognition Composition Law.
scope and limits
- Does not prove wrap-around adjacency of the full cycle.
- Does not establish injectivity of brgcPath.
- Does not extend to alphabets larger than two symbols.
- Does not quantify the Hamming distance beyond the one-bit case.
formal statement (Lean)
123private theorem oneBitDiff_snocBit_same {d : Nat} {p q : Pattern d} (b : Bool) :
124 OneBitDiff p q → OneBitDiff (snocBit p b) (snocBit q b) := by
proof body
Tactic-mode proof.
125 intro h
126 classical
127 rcases h with ⟨k, hk, hkuniq⟩
128 refine ⟨k.castSucc, ?_, ?_⟩
129 · simpa using hk
130 · intro j hj
131 -- any differing coordinate cannot be the new last coordinate (since it is fixed to `b`)
132 induction j using Fin.lastCases with
133 | last =>
134 have : False := by
135 simpa [snocBit] using hj
136 exact this.elim
137 | cast j =>
138 have hj' : p j ≠ q j := by
139 simpa [snocBit] using hj
140 have : j = k := hkuniq j hj'
141 simpa [this]
142