phases_require_complex
For k in {1,2,3,5,6,7} the phase factor exp(i π k /4) has nonzero imaginary part. Researchers deriving quantum mechanics or electromagnetism from Recognition Science's discrete 8-tick ledger would cite the result to justify the appearance of complex amplitudes. The proof unfolds the tickPhase definition, rewrites via Euler's formula to isolate the sine, invokes the sine-zero condition, and uses integer bounds together with the hypothesis to reach a contradiction.
claimFor each $k$ with $0 < k < 8$ and $k$ not divisible by 4, the imaginary part of $e^{i k π /4}$ is nonzero.
background
The module MATH-004 shows that the 8-tick cycle forces complex numbers because its phases are 45° rotations. The definition tickPhase(k) := exp(I * π * k /4) encodes these phases as eighth roots of unity on the unit circle. This rests on the Physical structure supplying positivity of c, ħ and G, together with the arithmetic lemmas mul_one, mul_zero and zero_add that underwrite the integer arithmetic in the proof. The upstream CirclePhaseLift.and result supplies explicit log-derivative bounds used in related phase-lifting arguments.
proof idea
Tactic proof that unfolds tickPhase, rewrites the exponent as a real multiple of I, applies Complex.exp_mul_I and ofReal_cos/sin, then simplifies the imaginary part to sin(k π /4). Assuming the sine vanishes triggers Real.sin_eq_zero_iff, yielding k = 4n for integer n. The range 0 ≤ k < 8 forces n = 0 or 1, hence k = 0 or 4, contradicting the hypothesis; the integer steps use field_simp and omega.
why it matters in Recognition Science
The result completes the MATH-004 derivation that the eight-tick octave (T7) requires two-dimensional rotations and therefore the imaginary unit. It supplies the base case for sibling declarations such as quantum_requires_complex and schrodingerEquation, linking the Recognition forcing chain directly to the complex wavefunction without extra postulates. No open scaffolding remains; the theorem is fully proved.
scope and limits
- Does not claim that every physical observable must be represented by a complex number.
- Does not derive the numerical value of α or other constants from this phase argument.
- Does not address continuous-time phase evolution or non-cyclic dynamics.
- Does not prove that the complex representation is unique up to field automorphism.
formal statement (Lean)
128theorem phases_require_complex (k : Fin 8) (hk : k.val ≠ 0 ∧ k.val ≠ 4) :
129 (tickPhase k).im ≠ 0 := by
proof body
Tactic-mode proof.
130 -- For phases 1,2,3,5,6,7, sin(k*π/4) ≠ 0
131 unfold tickPhase
132 have h_exp : I * π * k / 4 = ↑((k.val : ℝ) * π / 4 : ℝ) * I := by push_cast; ring
133 rw [h_exp, Complex.exp_mul_I]
134 rw [← Complex.ofReal_cos, ← Complex.ofReal_sin]
135 simp only [Complex.add_im, Complex.mul_I_im, Complex.ofReal_im, Complex.ofReal_re, zero_add]
136 -- sin(k * π / 4) ≠ 0 when k ∉ {0, 4}
137 intro h_sin
138 rw [Real.sin_eq_zero_iff] at h_sin
139 rcases h_sin with ⟨n, hn⟩
140 -- k * π / 4 = n * π implies k = 4n
141 have h_eq : (k.val : ℤ) = 4 * n := by
142 have : (k.val : ℝ) * π / 4 = n * π := hn.symm
143 field_simp [Real.pi_ne_zero] at this
144 exact_mod_cast this
145 -- k ∈ {0,...,7} and k = 4n implies n ∈ {0, 1}, hence k ∈ {0, 4}
146 have h_n_range : n = 0 ∨ n = 1 := by
147 have h1 : 0 ≤ (k.val : ℤ) := Int.natCast_nonneg _
148 have h2 : (k.val : ℤ) < 8 := by omega
149 omega
150 cases h_n_range with
151 | inl h0 =>
152 simp only [h0, mul_zero, Int.cast_zero] at h_eq
153 have : k.val = 0 := by omega
154 exact hk.left this
155 | inr h1 =>
156 simp only [h1, mul_one, Int.cast_one] at h_eq
157 have : k.val = 4 := by omega
158 exact hk.right this
159
160/-! ## Physical Applications -/
161
162/-- Quantum mechanics: The wavefunction must be complex.
163 Recent theorem (2021) proves no real formulation works. -/