roots_form_group

formal source

 192  cexp (I * (2 * Real.pi * k / 8))
 193
 194/-- The roots form a group. -/
 195theorem roots_form_group :
 196    ∀ j k : Fin 8, rootOfUnity j * rootOfUnity k = rootOfUnity (j + k) := by
 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 -/
 225structure ImaginaryUnitFalsifier where