boson_rotation_phase_pos_one
plain-language theorem explainer
The complex phase factor for an 8-tick boson under a full 2π rotation equals +1. Researchers deriving exchange statistics from discrete periodic structures would cite this base identity when establishing bosonic symmetry. The proof is a direct one-line application of the zero-phase lemma.
Claim. The complex exponential of the eight-tick phase at index zero satisfies $e^{i k} = 1$ when $k=0$.
background
The SpinStatistics module derives the full spin-statistics connection from the eight-tick ledger structure. The phase function maps each Fin 8 index k to kπ/4; phaseExp then forms the complex exponential of that value. phase_0_is_one records that the zero index produces the identity phase (no net change under exchange). The module imports EightTick for these phase definitions and uses them to separate bosonic (+1) from fermionic (-1) exchange signs.
proof idea
One-line wrapper that applies phase_0_is_one.
why it matters
This identity supplies the +1 rotation phase required for bosons in the eight-tick model, directly supporting the module's spin_statistics_theorem and exchange_sign_boson. It realizes the T7 eight-tick octave landmark by confirming that an integer number of half-cycles returns the state to itself. The result closes one half of the discrete rotation-to-exchange map before the full spin-statistics theorem is assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.