spin_statistics_from_foundation
plain-language theorem explainer
The theorem asserts that the phase factor at tick 4 equals -1, at tick 0 equals +1, and the sum of all eight phase factors vanishes. A physicist deriving spin-statistics from discrete time would cite it as the capstone linking the eight-tick cycle to fermionic antisymmetry and bosonic symmetry. The proof is a one-line term that packages three prior foundation lemmas into a single conjunction.
Claim. Let phaseExp(k) denote the complex phase factor exp(i * phase(k)) for k in the eight-tick cycle. Then phaseExp(4) = -1, phaseExp(0) = +1, and the sum over k from 0 to 7 of phaseExp(k) equals zero.
background
The module derives the spin-statistics connection from Recognition Science's eight-tick structure. The key definition is phaseExp(k) = Complex.exp(Complex.I * phase k) for k : Fin 8, which encodes the phase accumulated after k ticks. The module doc states that a 2π rotation traverses the full eight-tick cycle, half-integer spin requires two cycles for identity (yielding -1), and integer spin requires one cycle (yielding +1). Upstream results supply the three concrete facts: fermion_phase_from_foundation proves phaseExp(4) = -1 via the foundation lemma phase_4_is_minus_one; boson_phase_from_foundation proves phaseExp(0) = +1 via phase_0_is_one; vacuum_fluctuation_cancellation proves the sum equals zero via sum_8_phases_eq_zero.
proof idea
The proof is a term-mode wrapper that directly returns the triple of the three upstream theorems: fermion_phase_from_foundation, boson_phase_from_foundation, and vacuum_fluctuation_cancellation. No additional tactics or reductions are applied; the conjunction is assembled by constructor application.
why it matters
This theorem realizes the module's target of grounding the spin-statistics theorem in the eight-tick phase mechanism, directly implementing the T7 eight-tick octave landmark. It packages the three foundation connections into the unified statement described in the doc comment. No downstream uses are recorded, leaving open its integration into larger QFT constructions such as particle exchange or vacuum energy calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.