theorem
proved
boson_phase_from_foundation
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.QFT.SpinStatistics on GitHub at line 374.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
371
372 This explicitly connects the spin-statistics theorem to the proven
373 phase_0_is_one theorem in Foundation.EightTick. -/
374theorem boson_phase_from_foundation :
375 Foundation.EightTick.phaseExp ⟨0, by norm_num⟩ = 1 :=
376 Foundation.EightTick.phase_0_is_one
377
378open Foundation.EightTick in
379/-- **FOUNDATION CONNECTION**: The sum of all 8 phases is zero, which
380 underlies vacuum fluctuation cancellation.
381
382 This is proven in Foundation.EightTick.sum_8_phases_eq_zero. -/
383theorem vacuum_fluctuation_cancellation :
384 ∑ k : Fin 8, Foundation.EightTick.phaseExp k = 0 :=
385 Foundation.EightTick.sum_8_phases_eq_zero
386
387/-- **UNIFIED SPIN-STATISTICS FROM FOUNDATION**
388
389 The complete spin-statistics theorem grounded in Foundation proofs:
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