`phase`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.EightTick
domain: Foundation
line: 29 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.EightTick on GitHub at line 29.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  26open Real
  27
  28/-- The 8-tick phases: kπ/4 for k = 0, 1, ..., 7 -/
  29noncomputable def phase (k : Fin 8) : ℝ := (k : ℝ) * Real.pi / 4
  30
  31/-- The 8-tick phase is periodic with period 2π. -/
  32theorem phase_periodic : phase 0 + 2 * Real.pi = 2 * Real.pi := by
  33  unfold phase
  34  simp
  35
  36/-- Even ticks (0, 2, 4, 6) correspond to bosons. -/
  37def isEvenTick (k : Fin 8) : Bool := k.val % 2 = 0
  38
  39/-- Odd ticks (1, 3, 5, 7) correspond to fermions. -/
  40def isOddTick (k : Fin 8) : Bool := k.val % 2 = 1
  41
  42/-- Phase advance by one tick. -/
  43noncomputable def nextPhase (k : Fin 8) : Fin 8 := ⟨(k.val + 1) % 8, Nat.mod_lt _ (by norm_num)⟩
  44
  45/-- The complex exponential of a phase. -/
  46noncomputable def phaseExp (k : Fin 8) : ℂ := Complex.exp (Complex.I * phase k)
  47
  48/-- **THEOREM**: The 8th power of each phase gives 1.
  49    exp(i × k × π/4)^8 = exp(2πik) = 1.
  50    Uses periodicity: exp(2πin) = 1 for n ∈ ℤ. -/
  51theorem phase_eighth_power_is_one (k : Fin 8) :
  52    (phaseExp k)^8 = 1 := by
  53  unfold phaseExp phase
  54  rw [← Complex.exp_nat_mul]
  55  -- 8 * (I * (k * π / 4)) = 2kπI, and exp(2kπI) = 1
  56  have h : (8 : ℕ) * (Complex.I * ((k.val : ℕ) * Real.pi / 4 : ℝ)) = 2 * Real.pi * Complex.I * k.val := by
  57    push_cast
  58    ring
  59  simp only [] at h

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.