theorem
proved
term proof
grayCycle3_oneBit_step
show as:
view Lean formalization →
formal statement (Lean)
157theorem grayCycle3_oneBit_step : ∀ i : Fin 8, OneBitDiff (grayCycle3Path i) (grayCycle3Path (i + 1)) := by
proof body
Term-mode proof.
158 intro i
159 -- 8 explicit cases; each step flips exactly one of the three bits.
160 fin_cases i
161 · -- 0 -> 1 (flip bit 0)
162 refine ⟨⟨0, by decide⟩, ?_, ?_⟩
163 · simp [grayCycle3Path, gray8At, pattern3]
164 · intro k hk
165 fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
166 · -- 1 -> 3 (flip bit 1)
167 refine ⟨⟨1, by decide⟩, ?_, ?_⟩
168 · simp [grayCycle3Path, gray8At, pattern3]
169 · intro k hk
170 fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
171 · -- 2 -> 3? (i=2 means gray8At 2 = 3, next is gray8At 3 = 2; flip bit 0)
172 refine ⟨⟨0, by decide⟩, ?_, ?_⟩
173 · simp [grayCycle3Path, gray8At, pattern3]
174 · intro k hk
175 fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
176 · -- i=3: 2 -> 6 (flip bit 2)
177 refine ⟨⟨2, by decide⟩, ?_, ?_⟩
178 · simp [grayCycle3Path, gray8At, pattern3]
179 · intro k hk
180 fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
181 · -- i=4: 6 -> 7 (flip bit 0)
182 refine ⟨⟨0, by decide⟩, ?_, ?_⟩
183 · simp [grayCycle3Path, gray8At, pattern3]
184 · intro k hk
185 fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
186 · -- i=5: 7 -> 5 (flip bit 1)
187 refine ⟨⟨1, by decide⟩, ?_, ?_⟩
188 · simp [grayCycle3Path, gray8At, pattern3]
189 · intro k hk
190 fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
191 · -- i=6: 5 -> 4 (flip bit 0)
192 refine ⟨⟨0, by decide⟩, ?_, ?_⟩
193 · simp [grayCycle3Path, gray8At, pattern3]
194 · intro k hk
195 fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
196 · -- i=7: 4 -> 0 (wrap; flip bit 2)
197 refine ⟨⟨2, by decide⟩, ?_, ?_⟩
198 · simp [grayCycle3Path, gray8At, pattern3]
199 · intro k hk
200 fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
201
202/-- A rigorous Gray cycle for 3-bit patterns (the “8-tick” cycle). -/