`spin_statistics_from_foundation`

proved

show as: view math explainer →

module: IndisputableMonolith.QFT.SpinStatistics
domain: QFT
line: 393 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.SpinStatistics on GitHub at line 393.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 390    1. phase(4) = -1 → fermions antisymmetric (from Foundation)
 391    2. phase(0) = +1 → bosons symmetric (from Foundation)
 392    3. All 8 phases sum to 0 → vacuum fluctuations cancel (from Foundation) -/
 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) :=
 397  ⟨fermion_phase_from_foundation, boson_phase_from_foundation, vacuum_fluctuation_cancellation⟩
 398
 399end SpinStatistics
 400end QFT
 401end IndisputableMonolith

papers checked against this theorem

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