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

spin_statistics_from_foundation

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)

 393theorem spin_statistics_from_foundation :
 394    (Foundation.EightTick.phaseExp ⟨4, by norm_num⟩ = -1) ∧
 395    (Foundation.EightTick.phaseExp ⟨0, by norm_num⟩ = 1) ∧
 396    (∑ k : Fin 8, Foundation.EightTick.phaseExp k = 0) :=

proof body

Term-mode proof.

 397  ⟨fermion_phase_from_foundation, boson_phase_from_foundation, vacuum_fluctuation_cancellation⟩
 398
 399end SpinStatistics
 400end QFT
 401end IndisputableMonolith

depends on (4)

Lean names referenced from this declaration's body.