IndisputableMonolith.Patterns.GrayCycleGeneral
IndisputableMonolith/Patterns/GrayCycleGeneral.lean · 339 lines · 15 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Patterns
3import IndisputableMonolith.Patterns.GrayCycle
4import IndisputableMonolith.Patterns.GrayCode
5import IndisputableMonolith.Patterns.GrayCodeAxioms
6import IndisputableMonolith.Patterns.GrayCycleBRGC
7
8/-!
9# GrayCycle (general D) via BRGC (bounded) assumptions
10
11This module is the **Workstream A generalization**: it constructs an adjacent Gray cover/cycle
12for general dimension `d` using the standard BRGC formula
13
14 `gray(n) = n XOR (n >>> 1)`
15
16and exposes it as a `Patterns.GrayCover d (2^d)` / `Patterns.GrayCycle d`.
17
18Status / hygiene:
19- The construction is definitional.
20- This file is intentionally a **bounded / bitwise-formula** development:
21 the *successor adjacency* and the 64-bit inverse are routed through
22 `Patterns/GrayCodeAxioms.lean`, so the packaged objects here require
23 `[GrayCodeAxioms.GrayCodeFacts]` and a bound `d ≤ 64`.
24- **Canonical axiom-free general-D certificate**: use
25 `IndisputableMonolith/Patterns/GrayCycleBRGC.lean`, which constructs a recursive BRGC
26 path via `append` + `rev` and proves injectivity + one-bit adjacency (including wrap)
27 for all `d > 0` with **no axioms** and no `d ≤ 64` bound.
28- The D=3 case remains fully axiom-free in `Patterns/GrayCycle.lean`.
29-/
30
31namespace IndisputableMonolith
32namespace Patterns
33
34open Classical
35
36namespace GrayCycleGeneral
37
38open GrayCodeAxioms
39
40/-! ## The BRGC path as a Pattern-valued map -/
41
42/-- The BRGC path as a `Fin (2^d) → Pattern d`. -/
43def brgcPath (d : Nat) : Fin (2 ^ d) → Pattern d :=
44 fun i => binaryReflectedGray d i
45
46/-! ## One-bit adjacency of BRGC (bounded) -/
47
48/-! ### Wrap-around step (last → 0) is one-bit adjacent (axiom-free) -/
49
50private def allOnes (d : Nat) : Nat := 2 ^ d - 1
51
52private lemma allOnes_succ_eq_bit (t : Nat) :
53 allOnes (t + 1) = Nat.bit true (allOnes t) := by
54 have hpos1 : 1 ≤ 2 ^ (t + 1) := Nat.succ_le_of_lt (pow_pos (by decide : 0 < (2 : Nat)) (t + 1))
55 have hpos0 : 1 ≤ 2 ^ t := Nat.succ_le_of_lt (pow_pos (by decide : 0 < (2 : Nat)) t)
56 -- LHS + 1
57 have hL : allOnes (t + 1) + 1 = 2 ^ (t + 1) := by
58 simp [allOnes, Nat.sub_add_cancel hpos1]
59 -- RHS + 1
60 have hR : Nat.bit true (allOnes t) + 1 = 2 ^ (t + 1) := by
61 have hge : 2 ≤ 2 * (2 ^ t) := by
62 have h1 : 1 ≤ 2 ^ t := Nat.one_le_pow t 2 (by decide : 0 < (2 : Nat))
63 -- multiply the inequality by 2
64 simpa using (Nat.mul_le_mul_left 2 h1)
65 calc
66 Nat.bit true (allOnes t) + 1
67 = (2 * (allOnes t) + 1) + 1 := by simp [Nat.bit_val, Nat.add_assoc]
68 _ = 2 * (allOnes t) + 2 := by
69 simp [Nat.add_assoc]
70 _ = 2 * (2 ^ t - 1) + 2 := by
71 simp [allOnes]
72 _ = (2 * (2 ^ t) - 2) + 2 := by
73 -- distribute `2 * (a - 1)` and simplify
74 simp [Nat.mul_sub_left_distrib, Nat.mul_one, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm,
75 Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
76 _ = 2 * (2 ^ t) := Nat.sub_add_cancel hge
77 _ = 2 ^ (t + 1) := by
78 -- `2^(t+1) = 2^t * 2`
79 simp [pow_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]
80 have h : allOnes (t + 1) + 1 = Nat.bit true (allOnes t) + 1 := by
81 calc
82 allOnes (t + 1) + 1 = 2 ^ (t + 1) := hL
83 _ = Nat.bit true (allOnes t) + 1 := by
84 simpa using hR.symm
85 exact Nat.add_right_cancel h
86
87private lemma allOnes_testBit_lt : ∀ {t k : Nat}, k < t → (allOnes t).testBit k = true
88 | 0, _, hk => (Nat.not_lt_zero _ hk).elim
89 | (t + 1), 0, _ => by
90 -- `allOnes (t+1) = bit true (allOnes t)`
91 have hrepr : allOnes (t + 1) = Nat.bit true (allOnes t) := allOnes_succ_eq_bit t
92 simpa [hrepr] using (Nat.testBit_bit_zero true (allOnes t))
93 | (t + 1), (k + 1), hk => by
94 have hk' : k < t := Nat.lt_of_succ_lt_succ hk
95 have hrepr : allOnes (t + 1) = Nat.bit true (allOnes t) := allOnes_succ_eq_bit t
96 -- shift the bit index down one using `testBit_bit_succ`
97 have hshift :
98 (allOnes (t + 1)).testBit (k + 1) = (allOnes t).testBit k := by
99 simpa [hrepr] using (Nat.testBit_bit_succ (b := true) (n := allOnes t) (m := k))
100 -- now finish by IH
101 simpa [hshift] using (allOnes_testBit_lt (t := t) (k := k) hk')
102
103private lemma allOnes_testBit_eq_false_at (t : Nat) : (allOnes t).testBit t = false := by
104 -- `allOnes t < 2^t`
105 have hlt : allOnes t < 2 ^ t := by
106 -- `2^t - 1 < 2^t` since `2^t > 0`
107 simpa [allOnes] using Nat.sub_lt (pow_pos (by decide : 0 < (2 : Nat)) t) (by decide : 0 < 1)
108 exact Nat.testBit_eq_false_of_lt hlt
109
110theorem brgc_wrap_oneBitDiff {d : Nat} (hdpos : 0 < d) :
111 OneBitDiff (brgcPath d ⟨2 ^ d - 1, by
112 exact Nat.sub_lt (pow_pos (by decide : 0 < (2 : Nat)) d) (by decide)⟩) (brgcPath d 0) := by
113 classical
114 rcases Nat.exists_eq_succ_of_ne_zero (Nat.ne_of_gt hdpos) with ⟨t, rfl⟩
115 -- d = t+1, unique differing bit is the last one (value t)
116 let iLast : Fin (2 ^ (t + 1)) :=
117 ⟨2 ^ (t + 1) - 1, by
118 exact Nat.sub_lt (pow_pos (by decide : 0 < (2 : Nat)) (t + 1)) (by decide)⟩
119 have hw : OneBitDiff (brgcPath (t + 1) iLast) (brgcPath (t + 1) 0) := by
120 refine ⟨Fin.last t, ?_, ?_⟩
121 · -- show the last bit differs (it is true at iLast, false at 0)
122 have ht_true : (natToGray iLast.val).testBit t = true := by
123 -- compute `natToGray (allOnes (t+1))` at bit t: true XOR false = true
124 have hn : iLast.val = allOnes (t + 1) := rfl
125 have hshift : (iLast.val >>> 1) = allOnes t := by
126 -- `allOnes (t+1) = bit true (allOnes t)` ⇒ shiftRight 1 yields `allOnes t`
127 have hrepr : allOnes (t + 1) = Nat.bit true (allOnes t) := allOnes_succ_eq_bit t
128 -- use `bit_shiftRight_one`
129 have : (Nat.bit true (allOnes t) >>> 1) = allOnes t := Nat.bit_shiftRight_one true (allOnes t)
130 simpa [hn, hrepr] using this
131 -- now compute testBit of xor
132 -- n.testBit t = true (all ones), (n>>>1).testBit t = false
133 have hnbit : (iLast.val).testBit t = true := by
134 -- t < t+1
135 have : t < t + 1 := Nat.lt_succ_self t
136 simpa [hn, allOnes] using allOnes_testBit_lt (t := t + 1) (k := t) this
137 have hmbit : (iLast.val >>> 1).testBit t = false := by
138 -- iLast>>>1 = allOnes t, and that has bit t = false
139 simpa [hshift] using allOnes_testBit_eq_false_at t
140 -- combine via xor
141 simp [natToGray, hnbit, hmbit]
142 -- translate to the Pattern statement
143 have : brgcPath (t + 1) iLast (Fin.last t) ≠ brgcPath (t + 1) 0 (Fin.last t) := by
144 -- right side is false, left side is true
145 have h0 : brgcPath (t + 1) 0 (Fin.last t) = false := by
146 simp [brgcPath, binaryReflectedGray, natToGray]
147 have h1 : brgcPath (t + 1) iLast (Fin.last t) = true := by
148 simpa [brgcPath, binaryReflectedGray] using ht_true
149 simpa [h0, h1]
150 simpa using this
151 · intro j hj
152 -- any differing index must be the last one (all other bits are equal/false)
153 induction j using Fin.lastCases with
154 | last => rfl
155 | cast j =>
156 -- show contradiction: at castSucc j, both patterns are false
157 have hjlt : (j.val : Nat) < t := j.isLt
158 -- compute natToGray at bit j.val: true XOR true = false (since both allOnes have ones there)
159 have hfalse : brgcPath (t + 1) iLast j.castSucc = false := by
160 -- n = allOnes(t+1), m = n>>>1 = allOnes t
161 have hn : iLast.val = allOnes (t + 1) := rfl
162 have hnbit : (iLast.val).testBit j.val = true := by
163 have : j.val < t + 1 := Nat.lt_succ_of_lt hjlt
164 simpa [hn, allOnes] using allOnes_testBit_lt (t := t + 1) (k := j.val) this
165 have hshift : (iLast.val >>> 1) = allOnes t := by
166 have hrepr : allOnes (t + 1) = Nat.bit true (allOnes t) := allOnes_succ_eq_bit t
167 have : (Nat.bit true (allOnes t) >>> 1) = allOnes t := Nat.bit_shiftRight_one true (allOnes t)
168 simpa [hn, hrepr] using this
169 have hmbit : (iLast.val >>> 1).testBit j.val = true := by
170 simpa [hshift, allOnes] using allOnes_testBit_lt (t := t) (k := j.val) hjlt
171 have : (natToGray iLast.val).testBit j.val = false := by
172 simp [natToGray, hnbit, hmbit]
173 simpa [brgcPath, binaryReflectedGray] using this
174 have h0 : brgcPath (t + 1) 0 j.castSucc = false := by
175 simp [brgcPath, binaryReflectedGray, natToGray]
176 have : False := by
177 -- hj says they differ, but both patterns are false
178 simpa [hfalse, h0] using hj
179 exact this.elim
180 simpa [iLast] using hw
181
182/-! ## Injectivity of the BRGC path (no extra axioms) -/
183
184private lemma natToGray_testBit_false_of_ge {d n k : Nat} (hn : n < 2 ^ d) (hk : d ≤ k) :
185 (natToGray n).testBit k = false := by
186 -- natToGray n = n XOR (n >>> 1)
187 have hn_lt : n < 2 ^ k := by
188 have hpow : 2 ^ d ≤ 2 ^ k := by
189 rcases lt_or_eq_of_le hk with hlt | rfl
190 · exact le_of_lt (Nat.pow_lt_pow_right (by decide : 1 < (2 : Nat)) hlt)
191 · rfl
192 exact lt_of_lt_of_le hn hpow
193 have hn_bit : n.testBit k = false := Nat.testBit_eq_false_of_lt hn_lt
194 have hdiv_le : (n >>> 1) ≤ n := by
195 -- shiftRight_eq_div_pow: n >>> 1 = n / 2
196 simp [Nat.shiftRight_eq_div_pow, Nat.div_le_self]
197 have hdiv_lt : (n >>> 1) < 2 ^ k := lt_of_le_of_lt hdiv_le hn_lt
198 have hdiv_bit : (n >>> 1).testBit k = false := Nat.testBit_eq_false_of_lt hdiv_lt
199 -- combine
200 simp [natToGray, hn_bit, hdiv_bit]
201
202variable [GrayCodeFacts]
203
204theorem brgcPath_injective {d : Nat} (hdpos : 0 < d) (hd : d ≤ 64) : Function.Injective (brgcPath d) := by
205 intro i j hij
206 -- reduce to equality of the Nat Gray codes, then invert using `GrayCodeFacts.grayToNat_inverts_natToGray`.
207 have hbits : ∀ k : Nat, (natToGray i.val).testBit k = (natToGray j.val).testBit k := by
208 intro k
209 by_cases hk : k < d
210 · have := congrArg (fun p : Pattern d => p ⟨k, hk⟩) hij
211 simpa [brgcPath, binaryReflectedGray, natToGray] using this
212 · have hkge : d ≤ k := le_of_not_gt hk
213 have hi0 : (natToGray i.val).testBit k = false :=
214 natToGray_testBit_false_of_ge (d := d) (n := i.val) (k := k) i.isLt hkge
215 have hj0 : (natToGray j.val).testBit k = false :=
216 natToGray_testBit_false_of_ge (d := d) (n := j.val) (k := k) j.isLt hkge
217 simp [hi0, hj0]
218 have hgray : natToGray i.val = natToGray j.val := by
219 exact Nat.eq_of_testBit_eq hbits
220 -- show both indices are < 2^64
221 have hpow : 2 ^ d ≤ 2 ^ 64 := Nat.pow_le_pow_right (by decide : 0 < (2 : Nat)) hd
222 have hi64 : i.val < 2 ^ 64 := lt_of_lt_of_le i.isLt hpow
223 have hj64 : j.val < 2 ^ 64 := lt_of_lt_of_le j.isLt hpow
224 have hi_inv : GrayCodeAxioms.grayInverse (natToGray i.val) = i.val :=
225 GrayCodeFacts.grayToNat_inverts_natToGray (n := i.val) hi64
226 have hj_inv : GrayCodeAxioms.grayInverse (natToGray j.val) = j.val :=
227 GrayCodeFacts.grayToNat_inverts_natToGray (n := j.val) hj64
228 have : i.val = j.val := by
229 have := congrArg GrayCodeAxioms.grayInverse hgray
230 simpa [hi_inv, hj_inv] using this
231 exact Fin.ext this
232
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
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. -/
295noncomputable def brgcGrayCycle (d : Nat) (hdpos : 0 < d) (hd : d ≤ 64) : GrayCycle d :=
296{ path := brgcPath d
297 inj := brgcPath_injective (d := d) hdpos hd
298 oneBit_step := brgc_oneBit_step (d := d) hdpos hd
299}
300
301/-- A packaged Gray cover (surjective + one-bit steps) derived from `brgcGrayCycle`. -/
302noncomputable def brgcGrayCover (d : Nat) (hdpos : 0 < d) (hd : d ≤ 64) : GrayCover d (2 ^ d) :=
303{ path := brgcPath d
304 complete := by
305 classical
306 have h_inj : Function.Injective (brgcPath d) := brgcPath_injective (d := d) hdpos hd
307 have h_card : Fintype.card (Fin (2 ^ d)) = Fintype.card (Pattern d) := by
308 simp [Patterns.card_pattern]
309 have h_bij : Function.Bijective (brgcPath d) := by
310 -- Use the `Fintype` lemma: injective + equal card ⇒ bijective.
311 exact (Fintype.bijective_iff_injective_and_card (brgcPath d)).2 ⟨h_inj, h_card⟩
312 exact h_bij.2
313 oneBit_step := brgc_oneBit_step (d := d) hdpos hd
314}
315
316/-- **THEOREM (GENERAL)**: There exists a Gray cycle for any dimension `d > 0`.
317
318 This theorem provides the unconditional existence witness by delegating to
319 the recursive BRGC construction in `GrayCycleBRGC.lean`. -/
320theorem exists_grayCycle {d : Nat} (hdpos : 0 < d) : ∃ w : GrayCycle d, w.path 0 = GrayCycleBRGC.brgcPath d 0 :=
321 ⟨GrayCycleBRGC.brgcGrayCycle d hdpos, rfl⟩
322
323/-- **THEOREM (GENERAL)**: There exists a Gray cover for any dimension `d > 0`. -/
324theorem exists_grayCover {d : Nat} (hdpos : 0 < d) : ∃ w : GrayCover d (2 ^ d), w.path 0 = GrayCycleBRGC.brgcPath d 0 :=
325 ⟨GrayCycleBRGC.brgcGrayCover d hdpos, rfl⟩
326
327theorem exists_grayCycle_of_le64 {d : Nat} (hdpos : 0 < d) (hd : d ≤ 64) :
328 ∃ w : GrayCycle d, w.path = brgcPath d :=
329 ⟨brgcGrayCycle d hdpos hd, rfl⟩
330
331theorem exists_grayCover_of_le64 {d : Nat} (hdpos : 0 < d) (hd : d ≤ 64) :
332 ∃ w : GrayCover d (2 ^ d), w.path = brgcPath d :=
333 ⟨brgcGrayCover d hdpos hd, rfl⟩
334
335end GrayCycleGeneral
336
337end Patterns
338end IndisputableMonolith
339