IndisputableMonolith.Patterns.GrayCycleBRGC
IndisputableMonolith/Patterns/GrayCycleBRGC.lean · 448 lines · 14 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Patterns
3import IndisputableMonolith.Patterns.GrayCycle
4
5/-!
6# GrayCycle (general D) via BRGC recursion (axiom-free)
7
8This module provides an **axiom-free** general-\(D\) Gray cycle construction using the
9standard *recursive* BRGC definition:
10
11- BRGC(0) = [0]
12- BRGC(d+1) = [0·BRGC(d), 1·(BRGC(d))ʳ]
13
14We implement this as a `Fin (2^d) → Pattern d` path, and prove:
15- injectivity (no repeats),
16- one-bit adjacency (including wrap-around) for all `d > 0`,
17- packaged `GrayCycle d` / `GrayCover d (2^d)`.
18
19This construction is independent of `Patterns/GrayCodeAxioms.lean` and does **not**
20use the bitwise formula `gray(n) = n XOR (n >> 1)`.
21-/
22
23namespace IndisputableMonolith
24namespace Patterns
25
26open Classical
27
28namespace GrayCycleBRGC
29
30/-! ## Utilities: extend a pattern with a trailing bit -/
31
32/-- Append a fresh *last* coordinate `b` to a pattern `p : Pattern d`, yielding a pattern in
33dimension `d+1`. -/
34def snocBit {d : Nat} (p : Pattern d) (b : Bool) : Pattern (d + 1) :=
35 fun j => Fin.lastCases b (fun k => p k) j
36
37@[simp] lemma snocBit_castSucc {d : Nat} (p : Pattern d) (b : Bool) (k : Fin d) :
38 snocBit p b k.castSucc = p k := by
39 simp [snocBit]
40
41@[simp] lemma snocBit_last {d : Nat} (p : Pattern d) (b : Bool) :
42 snocBit p b (Fin.last d) = b := by
43 simp [snocBit]
44
45/-! ## The recursive BRGC path -/
46
47private lemma twoPow_succ_eq_add (d : Nat) : 2 ^ (d + 1) = 2 ^ d + 2 ^ d := by
48 -- `2^(d+1) = 2^d * 2 = 2 * 2^d = 2^d + 2^d`
49 simpa [pow_succ, Nat.mul_comm, Nat.two_mul]
50
51/-- The recursive BRGC path as a `Fin (2^d) → Pattern d`. -/
52def brgcPath : (d : Nat) → Fin (2 ^ d) → Pattern d
53 | 0, _ =>
54 -- unique 0-bit pattern
55 fun _ => False
56 | (d + 1), i =>
57 let T : Nat := 2 ^ d
58 let hTT : 2 ^ (d + 1) = T + T := by
59 simpa [T, twoPow_succ_eq_add d]
60 let i' : Fin (T + T) := i.cast hTT
61 let left : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d k) false
62 let right : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d (Fin.rev k)) true
63 Fin.append left right i'
64
65/-! ## Injectivity (no repeats) -/
66
67private lemma cast_add_one {n m : Nat} [NeZero n] [NeZero m] (h : n = m) (i : Fin n) :
68 (i + 1).cast h = (i.cast h) + 1 := by
69 subst h
70 simp
71
72theorem brgcPath_injective : ∀ d : Nat, Function.Injective (brgcPath d)
73 | 0 => by
74 intro i j _
75 -- `Fin 1` is a subsingleton (only `0`)
76 simpa [Fin.eq_zero i, Fin.eq_zero j]
77 | (d + 1) => by
78 intro i j hij
79 -- unfold the `d+1` definition and reduce to injectivity of the appended halves
80 classical
81 let T : Nat := 2 ^ d
82 have hTT : 2 ^ (d + 1) = T + T := by
83 simpa [T, twoPow_succ_eq_add d]
84 let left : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d k) false
85 let right : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d (Fin.rev k)) true
86 have hij' :
87 Fin.append left right (i.cast hTT) = Fin.append left right (j.cast hTT) := by
88 simpa [brgcPath, T, hTT, left, right] using hij
89
90 have hleft_inj : Function.Injective left := by
91 intro a b hab
92 have hab' : brgcPath d a = brgcPath d b := by
93 funext k
94 have := congrArg (fun p : Pattern (d + 1) => p k.castSucc) hab
95 simpa [left, snocBit] using this
96 exact (brgcPath_injective d) hab'
97
98 have hright_inj : Function.Injective right := by
99 intro a b hab
100 have hab' : brgcPath d (Fin.rev a) = brgcPath d (Fin.rev b) := by
101 funext k
102 have := congrArg (fun p : Pattern (d + 1) => p k.castSucc) hab
103 simpa [right, snocBit] using this
104 have : Fin.rev a = Fin.rev b := (brgcPath_injective d) hab'
105 exact Fin.rev_injective this
106
107 have hdis : ∀ a b : Fin T, left a ≠ right b := by
108 intro a b hab
109 have := congrArg (fun p : Pattern (d + 1) => p (Fin.last d)) hab
110 -- last coordinate is the appended bit: false on left, true on right
111 simpa [left, right] using this
112
113 have happ_inj : Function.Injective (Fin.append left right) :=
114 (Fin.append_injective_iff (xs := left) (ys := right)).2 ⟨hleft_inj, hright_inj, hdis⟩
115
116 have hcast : i.cast hTT = j.cast hTT := happ_inj hij'
117 -- cast back along the inverse equality
118 have := congrArg (Fin.cast hTT.symm) hcast
119 simpa [hTT] using this
120
121/-! ## One-bit adjacency -/
122
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
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
143private theorem oneBitDiff_snocBit_flip {d : Nat} (p : Pattern d) :
144 OneBitDiff (snocBit p false) (snocBit p true) := by
145 classical
146 refine ⟨Fin.last d, ?_, ?_⟩
147 · simp
148 · intro j hj
149 induction j using Fin.lastCases with
150 | last => rfl
151 | cast j =>
152 have : False := by
153 -- on old coordinates the patterns are equal
154 simpa [snocBit] using hj
155 exact this.elim
156
157/-! ### Relating `natAdd` vs `addNat` when the sizes match -/
158
159private lemma natAdd_eq_addNat {T : Nat} (k : Fin T) :
160 (Fin.natAdd T k : Fin (T + T)) = k.addNat T := by
161 apply Fin.ext
162 -- both sides represent the same natural number `T + k`
163 simp [Fin.natAdd, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
164
165private lemma rev_add_one_eq {n : Nat} [NeZero n] {i : Fin n} (hi : i.val + 1 < n) :
166 Fin.rev (i + 1) + 1 = Fin.rev i := by
167 classical
168 apply Fin.ext
169 have hival : (i + 1).val = i.val + 1 :=
170 Fin.val_add_one_of_lt' (n := n) (i := i) hi
171 have hle1 : i.val + 1 ≤ n := Nat.le_of_lt hi
172 have hle2 : i.val + 2 ≤ n := Nat.succ_le_of_lt hi
173 have hnat : (n - (i.val + 2)) + 1 = n - (i.val + 1) := by
174 have h :
175 ((n - (i.val + 2)) + 1) + (i.val + 1) = (n - (i.val + 1)) + (i.val + 1) := by
176 calc
177 ((n - (i.val + 2)) + 1) + (i.val + 1)
178 = (n - (i.val + 2)) + (1 + (i.val + 1)) := by
179 simp [Nat.add_assoc]
180 _ = (n - (i.val + 2)) + (i.val + 2) := by
181 simp [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
182 _ = n := Nat.sub_add_cancel hle2
183 _ = (n - (i.val + 1)) + (i.val + 1) := (Nat.sub_add_cancel hle1).symm
184 exact Nat.add_right_cancel h
185 have hrev_succ : (Fin.rev (i + 1)).val = n - (i.val + 2) := by
186 simp [Fin.val_rev, hival, Nat.add_assoc]
187 have hnpos : 0 < n := Nat.pos_of_ne_zero (NeZero.ne n)
188 have hpos1 : 0 < i.val + 1 := Nat.succ_pos _
189 have hlt : n - (i.val + 1) < n := Nat.sub_lt hnpos hpos1
190 have hrev_add_lt : (Fin.rev (i + 1)).val + 1 < n := by
191 calc
192 (Fin.rev (i + 1)).val + 1
193 = n - (i.val + 1) := by
194 calc
195 (Fin.rev (i + 1)).val + 1 = (n - (i.val + 2)) + 1 := by
196 simpa [hrev_succ]
197 _ = n - (i.val + 1) := hnat
198 _ < n := hlt
199 have hL : (Fin.rev (i + 1) + 1).val = (Fin.rev (i + 1)).val + 1 :=
200 Fin.val_add_one_of_lt' (n := n) (i := Fin.rev (i + 1)) hrev_add_lt
201 have hR : (Fin.rev i).val = n - (i.val + 1) := by
202 simp [Fin.val_rev]
203 calc
204 (Fin.rev (i + 1) + 1).val = (Fin.rev (i + 1)).val + 1 := hL
205 _ = (n - (i.val + 2)) + 1 := by simpa [hrev_succ]
206 _ = n - (i.val + 1) := hnat
207 _ = (Fin.rev i).val := by simpa [hR]
208
209theorem brgc_oneBit_step : ∀ {d : Nat}, 0 < d →
210 ∀ i : Fin (2 ^ d), OneBitDiff (brgcPath d i) (brgcPath d (i + 1))
211 | 0, hdpos => (Nat.not_lt_zero _ hdpos).elim
212 | 1, _ => by
213 intro i
214 -- dimension 1: the cycle is `0 → 1 → 0`, so the only bit flips each step
215 fin_cases i
216 · -- 0 → 1
217 have : OneBitDiff (snocBit (brgcPath 0 0) false) (snocBit (brgcPath 0 0) true) :=
218 oneBitDiff_snocBit_flip (p := brgcPath 0 0)
219 simpa [brgcPath] using this
220 · -- 1 → 0 (wrap), use symmetry
221 have h : OneBitDiff (snocBit (brgcPath 0 0) false) (snocBit (brgcPath 0 0) true) :=
222 oneBitDiff_snocBit_flip (p := brgcPath 0 0)
223 have : OneBitDiff (snocBit (brgcPath 0 0) true) (snocBit (brgcPath 0 0) false) :=
224 OneBitDiff_symm h
225 simpa [brgcPath] using this
226 | (d + 2), _ => by
227 -- Inductive step: assume one-bit stepping for dimension `d+1`, prove for `d+2`.
228 have ih :
229 ∀ i : Fin (2 ^ (d + 1)), OneBitDiff (brgcPath (d + 1) i) (brgcPath (d + 1) (i + 1)) :=
230 brgc_oneBit_step (d := d + 1) (Nat.succ_pos _)
231 intro i
232 classical
233 let T : Nat := 2 ^ (d + 1)
234 have hTT : 2 ^ (d + 2) = T + T := by
235 simpa [T] using twoPow_succ_eq_add (d := d + 1)
236 let left : Fin T → Pattern (d + 2) := fun k => snocBit (brgcPath (d + 1) k) false
237 let right : Fin T → Pattern (d + 2) := fun k => snocBit (brgcPath (d + 1) (Fin.rev k)) true
238 let i' : Fin (T + T) := i.cast hTT
239
240 have hTpos : 0 < T := pow_pos (by decide : 0 < (2 : Nat)) (d + 1)
241 letI : NeZero T := ⟨Nat.ne_zero_of_lt hTpos⟩
242 letI : NeZero (T + T) := ⟨Nat.ne_zero_of_lt (Nat.add_pos_left hTpos T)⟩
243
244 have hcast_succ : (i + 1).cast hTT = i' + 1 := by
245 -- `cast` commutes with `+1` along definitional equalities
246 simpa [i'] using (cast_add_one (n := 2 ^ (d + 2)) (m := T + T) (h := hTT) i)
247
248 -- Reduce to the `Fin (T+T)` index space.
249 have hTTgoal : OneBitDiff (Fin.append left right i') (Fin.append left right (i' + 1)) := by
250 -- case split on whether `i'` lies in the left or right half, and whether we cross a boundary
251 induction i' using Fin.addCases with
252 | left k =>
253 -- i' = castAdd T k
254 by_cases hk : k.val + 1 < T
255 · -- successor stays in the left half
256 have hk_big : (Fin.castAdd T k : Fin (T + T)).val + 1 < T + T := by
257 -- k.val + 1 < T ≤ T+T
258 exact lt_of_lt_of_le hk (Nat.le_add_right T T)
259 have hnext : (Fin.castAdd T k : Fin (T + T)) + 1 = Fin.castAdd T (k + 1) := by
260 apply Fin.ext
261 have hk1 : (k + 1).val = k.val + 1 :=
262 Fin.val_add_one_of_lt' (n := T) (i := k) hk
263 have hk'1 : ((Fin.castAdd T k : Fin (T + T)) + 1).val =
264 (Fin.castAdd T k : Fin (T + T)).val + 1 :=
265 Fin.val_add_one_of_lt' (n := T + T) (i := Fin.castAdd T k) hk_big
266 simpa [hk1] using hk'1
267 -- adjacency comes from IH in dimension d+1, lifted through `snocBit`
268 have hstep : OneBitDiff (brgcPath (d + 1) k) (brgcPath (d + 1) (k + 1)) := ih k
269 have hstep' : OneBitDiff (left k) (left (k + 1)) :=
270 oneBitDiff_snocBit_same false hstep
271 -- rewrite the `append` evaluations
272 simpa [Fin.append_left, hnext, left, right] using hstep'
273 · -- boundary: last element of left half steps into the first element of right half
274 have hkval : k.val = T - 1 := by
275 have hle : k.val + 1 ≤ T := Nat.succ_le_of_lt k.isLt
276 have hge : T ≤ k.val + 1 := Nat.le_of_not_gt hk
277 have : k.val + 1 = T := Nat.le_antisymm hle hge
278 exact Nat.eq_sub_of_add_eq this
279 have hnext : (Fin.castAdd T k : Fin (T + T)) + 1 = Fin.natAdd T 0 := by
280 apply Fin.ext
281 -- both have value `T`
282 have hT1 : 1 ≤ T := Nat.succ_le_of_lt hTpos
283 have hkplus : (Fin.castAdd T k : Fin (T + T)).val + 1 = T := by
284 -- `(castAdd T k).val = k.val = T-1`
285 simpa [hkval, Nat.sub_add_cancel hT1]
286 have hk_big : (Fin.castAdd T k : Fin (T + T)).val + 1 < T + T := by
287 -- `T < T+T` since `T>0`
288 have hT1 : 1 ≤ T := Nat.succ_le_of_lt hTpos
289 have hTlt : T < T + T := by
290 have hle : T + 1 ≤ T + T := Nat.add_le_add_left hT1 T
291 exact lt_of_lt_of_le (Nat.lt_succ_self T) hle
292 -- rewrite the LHS using `hkplus : (castAdd ...).val + 1 = T`
293 exact hkplus.symm ▸ hTlt
294 have hk'1 : ((Fin.castAdd T k : Fin (T + T)) + 1).val =
295 (Fin.castAdd T k : Fin (T + T)).val + 1 :=
296 Fin.val_add_one_of_lt' (n := T + T) (i := Fin.castAdd T k) hk_big
297 have hval : ((Fin.castAdd T k : Fin (T + T)) + 1).val = T := by
298 exact hk'1.trans hkplus
299 -- `natAdd T 0` has val `T`
300 simpa [hval]
301 -- show underlying index on the right is also `k` (since `rev 0` is last)
302 have hrev0 : Fin.rev (0 : Fin T) = k := by
303 apply Fin.ext
304 -- `rev 0` has value `T-1`
305 simpa [hkval] using (Fin.val_rev_zero (n := T))
306 have hstep' : OneBitDiff (left k) (right 0) := by
307 -- same underlying pattern, last bit flips
308 simpa [left, right, hrev0] using (oneBitDiff_snocBit_flip (p := brgcPath (d + 1) k))
309 -- rewrite `append` at the boundary indices explicitly (avoid `natAdd`/`addNat` mismatch issues)
310 have happL : Fin.append left right (Fin.castAdd T k) = left k := by
311 simpa using (Fin.append_left (u := left) (v := right) k)
312 have happNext : Fin.append left right ((Fin.castAdd T k : Fin (T + T)) + 1) = right 0 := by
313 have : Fin.append left right (Fin.natAdd T (0 : Fin T)) = right 0 := by
314 simpa using (Fin.append_right (u := left) (v := right) (i := (0 : Fin T)))
315 simpa [hnext] using this
316 have hstep0 : OneBitDiff (Fin.append left right (Fin.castAdd T k)) (right 0) := by
317 simpa [happL] using hstep'
318 -- replace `right 0` with the `append` at the successor index
319 simpa [happNext.symm] using hstep0
320 | right k =>
321 -- i' = natAdd T k
322 by_cases hk : k.val + 1 < T
323 · -- successor stays in the right half
324 have hk_big : (Fin.natAdd T k : Fin (T + T)).val + 1 < T + T := by
325 -- (T + k.val) + 1 < T + T since k.val + 1 < T
326 have : T + (k.val + 1) < T + T := Nat.add_lt_add_left hk T
327 simpa [Fin.natAdd, Nat.add_assoc] using this
328 have hnext : (Fin.natAdd T k : Fin (T + T)) + 1 = Fin.natAdd T (k + 1) := by
329 apply Fin.ext
330 have hk1 : (k + 1).val = k.val + 1 :=
331 Fin.val_add_one_of_lt' (n := T) (i := k) hk
332 have hk'1 : ((Fin.natAdd T k : Fin (T + T)) + 1).val =
333 (Fin.natAdd T k : Fin (T + T)).val + 1 :=
334 Fin.val_add_one_of_lt' (n := T + T) (i := Fin.natAdd T k) hk_big
335 simpa [hk1, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] using hk'1
336 -- adjacency comes from IH in dimension d+1, but the right half is reversed
337 have hrevStep : OneBitDiff
338 (brgcPath (d + 1) (Fin.rev (k + 1))) (brgcPath (d + 1) ((Fin.rev (k + 1)) + 1)) := ih (Fin.rev (k + 1))
339 have hrevRel : (Fin.rev (k + 1) : Fin T) + 1 = Fin.rev k := by
340 -- rev(k+1) + 1 = rev(k) when k.val+1 < T
341 -- use the helper lemma on `Fin T`
342 simpa [Nat.add_assoc] using (rev_add_one_eq (n := T) (i := k) hk)
343 have hstep0 : OneBitDiff (brgcPath (d + 1) (Fin.rev (k + 1))) (brgcPath (d + 1) (Fin.rev k)) := by
344 simpa [hrevRel] using hrevStep
345 have hstep1 : OneBitDiff (brgcPath (d + 1) (Fin.rev k)) (brgcPath (d + 1) (Fin.rev (k + 1))) :=
346 OneBitDiff_symm hstep0
347 have hstep' : OneBitDiff (right k) (right (k + 1)) :=
348 oneBitDiff_snocBit_same true hstep1
349 -- rewrite `append` on the right half via a successor-index evaluation
350 have happK : Fin.append left right (Fin.natAdd T k) = right k := by
351 simpa using (Fin.append_right (u := left) (v := right) (i := k))
352 -- switch to the `addNat` presentation used by the simplifier in this file
353 have hnextAdd : (k.addNat T : Fin (T + T)) + 1 = (k + 1).addNat T := by
354 -- rewrite both `natAdd` endpoints into `addNat`
355 simpa [natAdd_eq_addNat (T := T) (k := k), natAdd_eq_addNat (T := T) (k := (k + 1))] using hnext
356 have happK' : Fin.append left right (k.addNat T) = right k := by
357 have : Fin.append left right (Fin.natAdd T k) = right k := by
358 simpa using (Fin.append_right (u := left) (v := right) (i := k))
359 simpa [natAdd_eq_addNat (T := T) (k := k)] using this
360 have happNext : Fin.append left right (k.addNat T + 1) = right (k + 1) := by
361 have : Fin.append left right (Fin.natAdd T (k + 1)) = right (k + 1) := by
362 simpa using (Fin.append_right (u := left) (v := right) (i := (k + 1)))
363 have : Fin.append left right ((k + 1).addNat T) = right (k + 1) := by
364 simpa [natAdd_eq_addNat (T := T) (k := (k + 1))] using this
365 simpa [hnextAdd.symm] using this
366 have hstep0 : OneBitDiff (Fin.append left right (k.addNat T)) (right (k + 1)) := by
367 simpa [happK'] using hstep'
368 simpa [happNext.symm] using hstep0
369 · -- boundary: last element of right half wraps back to the first element of left half
370 have hkval : k.val = T - 1 := by
371 have hle : k.val + 1 ≤ T := Nat.succ_le_of_lt k.isLt
372 have hge : T ≤ k.val + 1 := Nat.le_of_not_gt hk
373 have : k.val + 1 = T := Nat.le_antisymm hle hge
374 exact Nat.eq_sub_of_add_eq this
375 have hnext : (Fin.natAdd T k : Fin (T + T)) + 1 = Fin.castAdd T 0 := by
376 apply Fin.ext
377 -- last element in `Fin (T+T)` wraps to `0`
378 have hT1 : 1 ≤ T := Nat.succ_le_of_lt hTpos
379 have hsum : k.val + T + 1 = T + T := by
380 calc
381 k.val + T + 1 = (T - 1) + T + 1 := by simp [hkval]
382 _ = (T - 1) + 1 + T := by
383 simp [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
384 _ = T + T := by
385 simp [Nat.sub_add_cancel hT1, Nat.add_assoc]
386 -- `((natAdd T k) + 1).val = ((k.val + T) + 1) % (T+T) = 0`
387 -- (the RHS `castAdd T 0` has value 0)
388 have : ((k.val + T + 1) % (T + T)) = 0 := by
389 simpa [hsum, Nat.mod_self]
390 simpa [Fin.val_add] using this
391 have hrev_last : Fin.rev k = (0 : Fin T) := by
392 apply Fin.ext
393 -- rev(last) has value 0
394 have hT1 : 1 ≤ T := Nat.succ_le_of_lt hTpos
395 have : (T - 1 + 1) = T := Nat.sub_add_cancel hT1
396 simp [Fin.val_rev, hkval, this]
397 have hstep' : OneBitDiff (right k) (left 0) := by
398 -- last bit flips from `true` to `false`
399 have hflip : OneBitDiff (snocBit (brgcPath (d + 1) 0) false) (snocBit (brgcPath (d + 1) 0) true) :=
400 oneBitDiff_snocBit_flip (p := brgcPath (d + 1) 0)
401 have hflip' : OneBitDiff (snocBit (brgcPath (d + 1) 0) true) (snocBit (brgcPath (d + 1) 0) false) :=
402 OneBitDiff_symm hflip
403 simpa [left, right, hrev_last] using hflip'
404 -- rewrite `append` on the first index, and replace `left 0` with the successor-index append via `hnext`
405 -- also rewrite the starting index to `addNat` to match the goal presentation
406 have happK : Fin.append left right (k.addNat T) = right k := by
407 have : Fin.append left right (Fin.natAdd T k) = right k := by
408 simpa using (Fin.append_right (u := left) (v := right) (i := k))
409 simpa [natAdd_eq_addNat (T := T) (k := k)] using this
410 have happNext : Fin.append left right ((Fin.natAdd T k : Fin (T + T)) + 1) = left 0 := by
411 have : Fin.append left right (Fin.castAdd T (0 : Fin T)) = left 0 := by
412 simpa using (Fin.append_left (u := left) (v := right) (i := (0 : Fin T)))
413 -- `(natAdd T k) + 1 = castAdd T 0`
414 simpa [hnext.symm] using this
415 have hstep0 : OneBitDiff (Fin.append left right (k.addNat T)) (left 0) := by
416 simpa [happK] using hstep'
417 -- replace `left 0` with the successor-index append
418 simpa [happNext.symm] using hstep0
419
420 -- lift back to the `Fin (2^(d+2))` index space
421 simpa [brgcPath, T, hTT, left, right, i', hcast_succ] using hTTgoal
422
423/-! ## Packaged GrayCycle/GrayCover -/
424
425noncomputable def brgcGrayCycle (d : Nat) (hdpos : 0 < d) : GrayCycle d :=
426{ path := brgcPath d
427 inj := brgcPath_injective d
428 oneBit_step := brgc_oneBit_step (d := d) hdpos
429}
430
431noncomputable def brgcGrayCover (d : Nat) (hdpos : 0 < d) : GrayCover d (2 ^ d) :=
432{ path := brgcPath d
433 complete := by
434 classical
435 have h_inj : Function.Injective (brgcPath d) := brgcPath_injective d
436 have h_card : Fintype.card (Fin (2 ^ d)) = Fintype.card (Pattern d) := by
437 simp [Patterns.card_pattern]
438 have h_bij : Function.Bijective (brgcPath d) :=
439 (Fintype.bijective_iff_injective_and_card (brgcPath d)).2 ⟨h_inj, h_card⟩
440 exact h_bij.2
441 oneBit_step := brgc_oneBit_step (d := d) hdpos
442}
443
444end GrayCycleBRGC
445
446end Patterns
447end IndisputableMonolith
448