phases_require_complex
plain-language theorem explainer
The theorem shows that the imaginary part of the k-th tick phase is nonzero for k in {1,2,3,5,6,7}. Researchers deriving the necessity of complex numbers from the Recognition Science 8-tick ledger would cite it. The proof reduces the claim to sin(k π /4) ≠ 0 via the complex exponential, then uses integer arithmetic on the zero set of sine to reach a contradiction with the hypothesis on k.
Claim. Let $k$ be an integer satisfying $0 ≤ k ≤ 7$ with $k ≠ 0$ and $k ≠ 4$. Then the imaginary part of $e^{i π k / 4}$ is nonzero.
background
The module MATH-004 derives the necessity of complex numbers from Recognition Science's 8-tick phase structure: the ledger cycle produces phases at multiples of π/4, which are rotations and therefore require a two-dimensional representation. tickPhase is the definition that realizes these phases as Complex.exp(I * π * k / 4) for k : Fin 8. The upstream Physical structure supplies only the minimal positivity assumptions on c, ħ, G that anchor bridge data; the arithmetic lemmas mul_one, mul_zero, zero_add supply the integer ring facts used in the range argument.
proof idea
The tactic proof unfolds tickPhase, rewrites the argument of the exponential to isolate the imaginary unit, applies exp_mul_I together with ofReal_cos and ofReal_sin, then assumes the imaginary part vanishes. It invokes Real.sin_eq_zero_iff, solves the resulting equation to obtain k = 4n, and uses the bounds 0 ≤ k < 8 together with mul_zero and mul_one to force n = 0 or n = 1, hence k = 0 or 4, contradicting the hypothesis.
why it matters
This is the central lemma of MATH-004 establishing that the 8-tick cycle (T7) forces the imaginary unit because nonzero phases cannot be represented on the real line. It directly supports the module claim that quantum mechanics and phasor representations inherit complex structure from the ledger. No downstream theorems are recorded yet; the result closes the rotation-to-complex step in the forcing chain before the quantum_requires_complex sibling is reached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.