eight_ticks_full_cycle
plain-language theorem explainer
The theorem establishes that for any spin quantum number s the phase increment per tick raised to the eighth power recovers the full cycle phase. Researchers deriving the spin-statistics theorem from discrete time in Recognition Science would cite this when linking the 8-tick octave to exchange symmetry. The proof unfolds the two phase definitions, rewrites via the complex exponential power rule, and reduces the resulting equality by congruence followed by ring normalization.
Claim. For any spin quantum number $s$, the eighth power of the phase accumulated per fundamental time quantum equals the phase after one complete cycle: $ (phasePerTick(s))^8 = cyclePhase(s) $.
background
The module derives the spin-statistics connection from Recognition Science's 8-tick phase structure. Spin is the structure holding twice the spin value as a nonnegative integer, so half-integer spins correspond to odd twice-values. The upstream tick definition supplies the fundamental time quantum τ₀ = 1, while the phase definition from the EightTick foundation returns kπ/4 for k = 0..7. The local setting is the phase accumulation rule: a 2π rotation traverses one 8-tick octave, with half-integer spins requiring two octaves for identity and integer spins requiring one.
proof idea
The tactic proof unfolds phasePerTick and cyclePhase, rewrites with the lemma Complex.exp_nat_mul, applies congr 1 to reduce to the exponent, and closes with the ring tactic for algebraic simplification.
why it matters
The result fills the phase identity inside the 8-tick octave (T7) and supplies the algebraic step used by the spin_statistics_fermion and spin_statistics_boson examples later in the module. It therefore connects the discrete time quantum directly to the sign that distinguishes Fermi-Dirac from Bose-Einstein statistics. No open scaffolding remains in this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.