brgc_oneBit_step
The lemma proves that the binary-reflected Gray code path for d bits (0 < d ≤ 64) yields consecutive patterns differing in exactly one bit, including wrap-around from last to first. Pattern theorists constructing Hamiltonian cycles on hypercubes cite this step when packaging explicit Gray cycles. The proof splits on whether the index wraps modulo 2^d, invoking an external one-bit property for interior steps and reducing the boundary to a dedicated wrap lemma.
claimFor every natural number $d$ with $0 < d ≤ 64$ and every index $i$ in the set of size $2^d$, the binary-reflected Gray code of $i$ and the binary-reflected Gray code of $i+1$ (modulo $2^d$) differ in exactly one bit position.
background
The module develops Gray cycles for general dimension $d$ via the binary-reflected formula gray(n) = n XOR (n right-shift 1), under the explicit bound $d ≤ 64$ that routes successor adjacency through bitwise axioms. OneBitDiff is the predicate asserting two patterns differ in precisely one coordinate. The local setting is the bounded development, which contrasts with the recursive axiom-free version in the sibling module. The proof draws on the one-bit property for Gray codes and the wrap-around adjacency lemma.
proof idea
The tactic proof opens with intro i and classical, then applies by_cases on whether i.val + 1 < 2^d. The non-wrapping branch invokes gray_code_one_bit_property to extract the unique differing bit k, verifies the difference via Fin.val_add_one_of_lt', and confirms uniqueness by matching against the axiom-supplied witness. The wrapping branch proves i equals the last index via Nat.le_antisymm, shows the successor is zero, and reduces via simpa to the wrap lemma.
why it matters in Recognition Science
This lemma supplies the oneBit_step field required to form the GrayCycle structure, which directly yields the packaged brgcGrayCycle and brgcGrayCover objects. Those objects feed the general-d cycle cover used in pattern recognition arguments. In the Recognition framework it supports the D=3 spatial construction and explicit adjacent paths on the phi-ladder. It touches the open question of lifting the d ≤ 64 bound without axioms.
scope and limits
- Does not establish the result for dimensions exceeding 64.
- Does not remove dependence on the GrayCodeAxioms interface.
- Does not address non-binary-reflected Gray code constructions.
- Does not prove injectivity of the path (handled by a separate lemma).
formal statement (Lean)
233lemma brgc_oneBit_step {d : Nat} (hdpos : 0 < d) (hd : d ≤ 64) :
234 ∀ i : Fin (2 ^ d), OneBitDiff (brgcPath d i) (brgcPath d (i + 1)) := by
proof body
Tactic-mode proof.
235 intro i
236 classical
237 -- split on whether `i.val + 1 < 2^d` (no wrap) or wrap case
238 by_cases hstep : i.val + 1 < 2 ^ d
239 · -- Use the Gray-code one-bit property at the Nat level.
240 rcases GrayCodeAxioms.gray_code_one_bit_property (d := d) (n := i.val) hstep with
241 ⟨k, hk, hkuniq⟩
242 have hklt : k < d := hk.1
243 let kk : Fin d := ⟨k, hklt⟩
244 refine ⟨kk, ?diff, ?uniq⟩
245 · -- Show the bit differs at coordinate kk.
246 haveI : NeZero (2 ^ d) := ⟨pow_ne_zero d (by decide : (2 : Nat) ≠ 0)⟩
247 have hval : (i + 1).val = i.val + 1 :=
248 Fin.val_add_one_of_lt' (n := 2 ^ d) (i := i) hstep
249 dsimp [brgcPath, binaryReflectedGray, natToGray, kk]
250 simpa [hval] using hk.2
251 · intro j hj
252 -- Uniqueness: any differing coordinate must be kk.
253 haveI : NeZero (2 ^ d) := ⟨pow_ne_zero d (by decide : (2 : Nat) ≠ 0)⟩
254 have hval : (i + 1).val = i.val + 1 :=
255 Fin.val_add_one_of_lt' (n := 2 ^ d) (i := i) hstep
256 have hjnat :
257 ((i.val ^^^ (i.val >>> 1)).testBit j.val) ≠
258 (((i.val + 1) ^^^ ((i.val + 1) >>> 1)).testBit j.val) := by
259 dsimp [brgcPath, binaryReflectedGray, natToGray] at hj
260 simpa [hval] using hj
261 have : (j.val : Nat) = k := by
262 exact hkuniq j.val ⟨j.isLt, hjnat⟩
263 apply Fin.ext
264 simpa [kk] using this
265 · -- Wrap case: i is the last index and (i+1)=0 in `Fin (2^d)`.
266 -- In the wrap branch, `i` must be the last element: `i.val = 2^d - 1`.
267 have hi_eq : i.val = 2 ^ d - 1 := by
268 have hle : i.val ≤ 2 ^ d - 1 := Nat.le_pred_of_lt i.isLt
269 have hge : 2 ^ d - 1 ≤ i.val := by
270 -- not (i+1 < 2^d) ⇒ 2^d ≤ i+1 ⇒ 2^d - 1 ≤ i
271 have : 2 ^ d ≤ i.val + 1 := Nat.le_of_not_gt hstep
272 have hpos : 0 < 2 ^ d := pow_pos (by decide : 0 < (2 : Nat)) d
273 have : Nat.succ (2 ^ d - 1) ≤ Nat.succ i.val := by
274 simpa [Nat.succ_eq_add_one, Nat.succ_pred_eq_of_pos hpos] using this
275 exact Nat.succ_le_succ_iff.mp this
276 exact Nat.le_antisymm hle hge
277 let iLast : Fin (2 ^ d) :=
278 ⟨2 ^ d - 1, by
279 exact Nat.sub_lt (pow_pos (by decide : 0 < (2 : Nat)) d) (by decide)⟩
280 have hi_def : i = iLast := by
281 apply Fin.ext
282 simp [iLast, hi_eq]
283 have hsucc0_last : iLast + 1 = 0 := by
284 apply Fin.ext
285 -- compute val_add modulo 2^d at the last index
286 have hle : 1 ≤ 2 ^ d := Nat.one_le_pow d 2 (by decide : 0 < (2 : Nat))
287 -- (2^d - 1 + 1) % 2^d = 0
288 simp [Fin.val_add, iLast, Nat.sub_add_cancel hle]
289 -- reduce to the wrap-around axiom statement (last index → 0)
290 simpa [hi_def, hsucc0_last] using (brgc_wrap_oneBitDiff (d := d) hdpos)
291
292/-! ## General GrayCycle/GrayCover existence under explicit assumptions -/
293
294/-- A packaged Gray cycle for general `d` under the bounded BRGC assumptions. -/