fermion_antisymmetric
plain-language theorem explainer
Half-integer spin particles acquire a phase factor of -1 after one full 8-tick cycle, equivalent to a 2π rotation. Researchers deriving the spin-statistics theorem from discrete time structures in Recognition Science would cite this result. The tactic proof unfolds the phase and spin definitions, uses oddness of twice the spin to rewrite the exponent, then reduces via complex exponential identities for multiples of πi.
Claim. For a spin quantum number $s$ that is half-integer, the phase factor acquired under one full 8-tick cycle satisfies $e^{2π i s} = -1$.
background
The module derives the spin-statistics connection from Recognition Science's 8-tick structure. Spin is the structure whose twice field is a non-negative integer encoding twice the spin value in units of ħ/2; isHalfInteger asserts that this integer is odd. The fundamental time quantum is the tick τ₀ = 1. Upstream, EightTick.phase supplies the discrete phases kπ/4 for k = 0..7, and cyclePhase accumulates the total phase over one full octave (2π rotation).
proof idea
The tactic proof unfolds cyclePhase, Spin.value and Spin.isHalfInteger. It obtains twice odd from the hypothesis, rewrites the phase expression 2πi·(twice/2) to πi·twice by ring, splits the exponent as 2kπi + πi, then applies Complex.exp_int_mul_two_pi_mul_I to reduce the integer multiple to 1 and Complex.exp_pi_mul_I to obtain the factor -1.
why it matters
This supplies the fermion phase factor required by exchange_equals_rotation (which equates exchange to 2π rotation) and by fermion_antisymmetry_from_8tick (which concludes ψ(x,y) = -ψ(y,x)). It fills the QFT-001 step linking the eight-tick octave (T7) to Fermi-Dirac statistics. The result closes the derivation of antisymmetric wavefunctions for half-integer spins directly from the discrete time structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.