spin_statistics_key
plain-language theorem explainer
Researchers deriving discrete symmetries from the Recognition Science clock cite this result to fix the phase signs that distinguish fermions from bosons. It asserts that the exponential phase at four ticks equals negative one while the zero-tick case equals one. The proof is a term construction that pairs the two specialized phase evaluations already established upstream.
Claim. The complex phase factor for a four-tick rotation satisfies $e^{iπ}=-1$ and the factor for a zero-tick rotation satisfies $e^{0}=1$.
background
The EightTick module introduces the fundamental discrete clock of Recognition Science whose phases run through multiples of π/4. This clock supplies the discrete symmetry underlying spin-statistics, CPT, and gauge structure. The function phaseExp maps an integer tick count to the corresponding complex exponential phase. Upstream theorems phase_4_is_minus_one and phase_0_is_one supply the explicit evaluations, with their doc-comments stating that k=4 yields the fermion antisymmetry sign while k=0 yields the boson symmetry sign.
proof idea
The proof is a term-mode construction that directly assembles the required conjunction from the two upstream theorems phase_4_is_minus_one and phase_0_is_one.
why it matters
This supplies the concrete phase values required by the spin-statistics theorem in the SpinStatistics module, which equates exchange sign under particle swap to the rotation phase of each particle. The result realizes the eight-tick octave (T7) and the explicit link between the discrete clock and fermion/boson statistics stated in the module doc-comment. It closes one step in the forcing chain that connects the 8-tick structure to observed particle exchange symmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.