phasePerTick
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.