tickPhase
plain-language theorem explainer
The phase assignment for the eight recognition ticks maps each integer k from 0 to 7 to the complex number exp(i π k /4). Researchers investigating the origin of complex numbers in physics from the eight-tick ledger cycle would reference this construction. It is supplied by a direct definition via the complex exponential function.
Claim. For each integer $k$ with $0 ≤ k < 8$, the phase of the $k$-th tick is $e^{i π k / 4}$.
background
The module derives the necessity of complex numbers from the 8-tick phase structure in Recognition Science. The eight-tick octave produces phases spaced by π/4, which are rotations in the plane and thus require the complex numbers. The tick is the fundamental time quantum, set to 1 in RS-native units.
proof idea
This is a direct definition that maps each k to Complex.exp (I * π * k / 4), which encodes rotation by the angle π k /4.
why it matters
It supplies the explicit phases used in tick_phases_roots_of_unity and phases_require_complex, which establish that the phases are 8th roots of unity and that non-real phases require the imaginary unit. It fills the MATH-004 target of showing complex numbers arise from the 8-tick structure (T7 in the forcing chain) and connects to the claim that physics requires ℂ because of ledger phases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.