phasePerTick
phasePerTick defines the complex phase factor acquired by a spin-s particle after one step inside the eight-tick cycle. Researchers deriving the spin-statistics theorem from Recognition Science's forced discrete time structure cite it when tracking phase accumulation that distinguishes half-integer from integer spins. The definition is a direct algebraic expression that applies the complex exponential to the scaled spin value.
claimFor spin quantum number $s$, the phase accumulated per tick is $e^{2π i s/8}$, where $s$ is the real number obtained by dividing the integer twice-value by two.
background
The Spin structure encodes the quantum number as twice an integer that is required to be non-negative, so the companion value function recovers the actual spin $s$ as twice/2. The QFT module places this definition inside the derivation of the spin-statistics connection from the eight-tick cycle, where a $2π$ rotation traverses exactly eight ticks. Upstream results supply the base eight-tick phases $kπ/4$ for $k=0..7$ and the complex exponential wrapper that turns a real angle into a unimodular complex number.
proof idea
The definition is a direct one-line expression that multiplies the spin value by $2π i$, divides by eight, and applies the complex exponential.
why it matters in Recognition Science
This definition supplies the per-tick phase factor raised to the eighth power in the downstream theorem eight_ticks_full_cycle to recover the full cycle phase. It fills the phase mechanism step in the module's derivation of the spin-statistics theorem from the eight-tick octave (T7), where half-integer spins accumulate a minus sign after one cycle while integer spins return to plus one. The construction supports the claim that the spin-statistics connection emerges from discrete time structure in Recognition Science.
scope and limits
- Does not define the phase after a full eight-tick cycle.
- Does not classify particles as fermions or bosons.
- Does not incorporate the Riemann hypothesis wedge phase.
- Does not handle negative spins.
formal statement (Lean)
240noncomputable def phasePerTick (s : Spin) : ℂ :=
proof body
Definition body.
241 Complex.exp (2 * π * I * s.value / 8)
242
243/-- **THEOREM**: 8 ticks gives the full cycle phase. -/