module module high

`IndisputableMonolith.QFT.SpinStatistics`

This module defines the Spin type for half-integer quantum numbers within Recognition Science QFT derivations. It supplies the representation used by Pauli exclusion and thermal statistics modules. The content consists of type definitions, value constructors, and integrality predicates built on the imported 8-tick structure.

claimThe module introduces the type $S$ of spin quantum numbers where each element is $n/2$ for $n \in \mathbb{Z}$, together with the projection $v: S o rac12 \mathbb{Z}$ and the predicates distinguishing integer versus half-integer cases.

background

The module sits inside the QFT tier of Recognition Science and imports the 8-tick discretization. Constants supplies the base time quantum $ au_0 = 1$ tick. Foundation.EightTick and RRF.Hypotheses.EightTick define the discrete 8-phase cycle that underpins ledger parity arguments for bosons and fermions. The doc-comment states the core object is the spin quantum number expressed as a half-integer.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds the parent QFT module and the downstream derivations PauliExclusion (ledger single-occupancy), BoseEinstein (even-phase ledger), FermiDirac (odd-phase ledger), and JCostThermoBridge. It supplies the spin representation required for the spin-statistics component of the tier-2 QFT derivations listed in the QFT module doc-comment.

scope and limits

Does not derive the spin-statistics theorem.
Does not link spin values to mass ladders or J-cost.
Does not treat continuous or infinite-dimensional representations.
Does not address relativistic wave equations.

used by (5)

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

IndisputableMonolith.QFT module_import
IndisputableMonolith.QFT.PauliExclusion module_import
IndisputableMonolith.Thermodynamics.BoseEinstein module_import
IndisputableMonolith.Thermodynamics.FermiDirac module_import
IndisputableMonolith.Thermodynamics.JCostThermoBridge module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.EightTick module_import
IndisputableMonolith.RRF.Hypotheses.EightTick module_import

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