pith. machine review for the scientific record. sign in
theorem proved tactic proof

fermion_antisymmetric

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 126theorem fermion_antisymmetric (s : Spin) (h : s.isHalfInteger) :
 127    cyclePhase s = -1 := by

proof body

Tactic-mode proof.

 128  unfold cyclePhase Spin.value Spin.isHalfInteger at *
 129  -- s.twice is odd, so s.twice % 2 = 1
 130  have hodd : s.twice % 2 = 1 := h
 131  -- Get k such that s.twice = 2k + 1
 132  have ⟨k, hk⟩ := Int.odd_iff.mpr hodd
 133  -- The phase is exp(2πi × (twice/2)) = exp(πi × twice)
 134  have h_rewrite : 2 * π * I * (s.twice / 2 : ℝ) = π * I * s.twice := by
 135    push_cast; ring
 136  rw [h_rewrite, hk]
 137  push_cast
 138  -- exp(πi × (2k+1)) = exp(2kπi) × exp(πi) = 1 × (-1) = -1
 139  have h_split : π * I * (2 * k + 1) = (k : ℂ) * (2 * π * I) + π * I := by ring
 140  rw [h_split, Complex.exp_add, Complex.exp_int_mul_two_pi_mul_I, one_mul, Complex.exp_pi_mul_I]
 141
 142/-- **THEOREM (Boson Phase)**: Integer spin particles acquire +1
 143    under the full 8-tick cycle (2π rotation). -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (16)

Lean names referenced from this declaration's body.