phase_eighth_power_is_one
plain-language theorem explainer
Each of the eight discrete phases satisfies (exp(i k π/4))^8 = 1. Researchers on spin-statistics theorems and integer Chern numbers cite the result to close the periodicity argument for the 8-tick clock. The tactic proof unfolds the phase and phaseExp definitions, reduces the argument by ring arithmetic to 2π i k, and invokes the standard exponential periodicity identity.
Claim. For every integer $k$ with $0 ≤ k ≤ 7$, $ (e^{i k π / 4})^8 = 1 $.
background
The module introduces the 8-tick structure as the fundamental discrete clock of Recognition Science, with phases at multiples of π/4 that underlie spin-statistics, CPT symmetry, and gauge structure. The definition phase(k) = k π/4 supplies the real angle, while phaseExp(k) = exp(i · phase(k)) supplies the complex multiplier on the unit circle. Upstream results establish that these phases are periodic with period 2π and that the exponential map converts the linear angle into the required root-of-unity behavior.
proof idea
The tactic proof unfolds phaseExp and phase, rewrites the power via Complex.exp_nat_mul, then applies a ring calculation to show the argument equals 2π i k. It finishes by converting to the library lemma Complex.exp_int_mul_two_pi_mul_I k.val, which directly yields 1.
why it matters
The result supplies the first conjunct of the spin_statistics_certificate, which certifies the entire RS_Spin_Statistics_Theorem.tex, and is invoked verbatim in chern_number_integer_from_8tick to guarantee integer winding numbers. It realizes the T7 eight-tick octave of the forcing chain, furnishing the exact periodicity required for the D = 3 spatial structure and the alpha-band constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Diffusion LLMs reach 1109 tokens per second on H100
"diffusion models... parallel generation, which can greatly improve speed"