pith. machine review for the scientific record. sign in
theorem proved tactic proof high

phases_require_complex

show as:
view Lean formalization →

The result shows that phase factors exp(i π k /4) for k in {1,2,3,5,6,7} have nonzero imaginary part. Researchers deriving the necessity of complex numbers from discrete rotation structures in foundational physics would cite it. The tactic proof unfolds the phase definition, rewrites via exp_mul_I to isolate the sine term, assumes vanishing sine, and reaches a contradiction with the excluded indices via sin_eq_zero_iff and integer range bounds.

claimFor each integer $k$ with $0 < k < 8$ and $k$ not equal to 4, 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. Each tick corresponds to a 45° rotation, represented by the phase factors $e^{i π k /4}$ for $k=0$ to 7. The definition tickPhase(k) := Complex.exp(I * π * k /4) encodes these factors directly. Upstream, the Physical structure supplies minimal positivity assumptions on c, ħ, and G that anchor later analytic lemmas, while arithmetic results such as mul_one, mul_zero, and zero_add ensure basic ring identities hold in the underlying logic.

proof idea

The tactic proof begins by unfolding tickPhase and rewriting the exponent via push_cast and ring to isolate the form (k π /4) * I. It applies Complex.exp_mul_I followed by ofReal_cos and ofReal_sin to obtain cos + i sin. Assuming the imaginary part vanishes triggers Real.sin_eq_zero_iff, yielding k π /4 = n π. Field simplification and cast lemmas reduce this to k = 4n. The range 0 ≤ k < 8 then forces n = 0 or 1 via omega, producing the two cases excluded by the hypothesis hk.

why it matters in Recognition Science

This theorem supplies the key algebraic step in MATH-004 showing that the 8-tick cycle (T7) cannot be realized inside the reals. It directly supports the claim that physics requires ℂ because ledger phases are rotations in the plane. No downstream uses are recorded yet, but the result underpins later declarations such as quantum_requires_complex and phasor constructions that invoke the same phase factors.

scope and limits

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. -/

depends on (6)

Lean names referenced from this declaration's body.