exchange_equals_rotation
plain-language theorem explainer
The theorem states that exchange of identical particles induces phase -1 for half-integer spin and +1 for integer spin. Researchers deriving spin-statistics from discrete time structures would cite this equivalence. The proof is a term-mode case split that applies the pre-established fermion antisymmetry and boson symmetry lemmas.
Claim. For every spin quantum number $s$, if $s$ is half-integer then the exchange phase equals $-1$, and if $s$ is integer then the exchange phase equals $+1$.
background
Recognition Science derives the spin-statistics connection from the 8-tick cycle whose phases are $kπ/4$ for $k=0..7$. The structure Spin encodes twice the spin value as an integer, with predicates isHalfInteger and isInteger distinguishing the cases. Exchange phase is the factor acquired under particle interchange, identified with the phase from a $2π$ rotation that traverses one full 8-tick cycle for bosons and two cycles for fermions. The upstream result phase_4_is_minus_one states: Phase at k=4 gives -1 (fermion phase). This is the key to antisymmetry under particle exchange.
proof idea
The proof is a term-mode construction. It introduces the spin $s$, builds the conjunction via constructor, then applies fermion_antisymmetric under the half-integer hypothesis and boson_symmetric under the integer hypothesis.
why it matters
This declaration supplies the explicit phase rule that realizes the module's target of deriving spin-statistics from the 8-tick structure (T7). It directly invokes phase_4_is_minus_one from Foundation.EightTick and the symmetry lemmas defined in the same file, closing the link between exchange and rotation. The result sits inside the Recognition framework's derivation of QFT statistics from the eight-tick octave and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.