IndisputableMonolith.QFT.SpinStatistics

declarations in this module (41)

• structure Spin L49
• def ofInt L58
• def halfInt L61
• def zero L64
• def half L67
• def one L70
• def threeHalves L73
• def two L76
• def value L79
• def isHalfInteger L82
• def isInteger L85
• theorem int_or_half L96
• theorem int_half_exclusive L101
• def cyclePhase L111
• def halfCyclePhase L115
• def exchangePhase L120
• theorem fermion_antisymmetric L126
• theorem boson_symmetric L144
• inductive Statistics L161
• def statisticsFromSpin L167
• theorem spin_statistics_fermion L171
• theorem spin_statistics_boson L176
• inductive ExchangeSymmetry L185
• def exchangeSymmetryFromSpin L191
• theorem fermion_antisymmetric_wavefunction L196
• theorem boson_symmetric_wavefunction L201
• theorem pauli_exclusion L215
• structure PhaseEntry L233
• def phasePerTick L240
• theorem eight_ticks_full_cycle L244
• structure SpinStatisticsFalsifier L275
• theorem no_sm_falsifier L284
• theorem fermion_antisymmetry_from_8tick L298
• structure FermionLedgerEntry L306
• theorem boson_symmetry_from_8tick L321
• structure BosonLedgerEntry L329
• theorem exchange_equals_rotation L345
• theorem fermion_phase_from_foundation L364
• theorem boson_phase_from_foundation L374
• theorem vacuum_fluctuation_cancellation L383
• theorem spin_statistics_from_foundation L393