lemma
proved
tactic proof
brgc_oneBit_step
show as:
view Lean formalization →
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. -/