theorem
proved
tactic proof
roots_form_group
show as:
view Lean formalization →
formal statement (Lean)
195theorem roots_form_group :
196 ∀ j k : Fin 8, rootOfUnity j * rootOfUnity k = rootOfUnity (j + k) := by
proof body
Tactic-mode proof.
197 intro j k
198 unfold rootOfUnity
199 rw [← Complex.exp_add]
200 push_cast
201 have h_val : ((j + k : Fin 8).val : ℝ) = ((j.val + k.val) % 8 : ℕ) := by
202 simp only [Fin.val_add]
203 rw [h_val]
204 have h_div : (j.val + k.val : ℕ) = ((j.val + k.val) % 8) + 8 * ((j.val + k.val) / 8) := by
205 rw [add_comm, Nat.div_add_mod]
206 push_cast
207 rw [h_div]
208 rw [mul_add, add_div, mul_add]
209 rw [← Complex.exp_add]
210 congr 1
211 · ring
212 · have h_period : I * (2 * Real.pi * (8 * ((j.val + k.val) / 8)) / 8) = I * (2 * Real.pi * ((j.val + k.val) / 8)) := by
213 ring
214 rw [h_period]
215 rw [mul_comm I, ← mul_assoc]
216 rw [Complex.exp_int_mul_two_pi_mul_I ((j.val + k.val) / 8)]
217 simp
218
219/-! ## Falsification Criteria -/
220
221/-- The derivation would be falsified if:
222 1. i² ≠ -1 (impossible, it's definitional)
223 2. Physics didn't need complex numbers (many alternatives tried, all failed)
224 3. 8-tick structure not fundamental -/