Mathematics Complex Numbers

Complex numbers and rotation

A complex number combines a real part and an imaginary part, written a + bi, where i is the square root of -1. The system is closed under addition, multiplication, and division, and it is algebraically closed: every polynomial with complex coefficients has a complex root. Its defining geometric property is that multiplication by a complex number of unit length rotates a point in the plane, while multiplication by a general complex number scales and rotates. This single property makes complex numbers the natural language for any phenomenon that involves cyclic change, from alternating current to the phase of a light wave.

The French mathematician Abraham de Moivre linked complex numbers to trigonometry in the early 1700s, and Leonhard Euler gave the formula e^(iθ) = cos θ + i sin θ in 1748. The formula shows that complex exponentials trace circles, and that the eight equally spaced points on the unit circle, the eighth roots of unity, are exactly the powers of e^(iπ/4). These points represent rotations by multiples of 45 degrees. The real numbers alone cannot express such a rotation, because multiplying two real numbers always keeps the result on the same line; there is no perpendicular component. Complex numbers supply that perpendicular direction.

In Recognition Science, the framework models a discrete ledger of recognition events, and its fundamental cycle has eight ticks. Each tick is a 45 degree rotation, so the eight phases are the eighth roots of unity. The framework's library of machine-checked theorems defines these phases as complex exponentials and proves that they are equally spaced and that their eighth power is 1. A theorem proves that any phase at a tick other than 0 or 4 has a nonzero imaginary part, which means the real numbers cannot represent the cycle. The framework therefore derives that physics must use complex numbers, because its ledger has phases that are rotations.

The framework's library also proves that complex multiplication preserves the product of lengths and adds angles, which is the algebraic statement of rotation plus scaling. It proves that the split-complex numbers, which have hyperbolic geometry, cannot represent cyclic phases, and that quaternions, which describe three-dimensional rotations, are not needed because the phase is two-dimensional. The framework states that quantum mechanics requires complex amplitudes, citing that experiments with Bell-like setups ruled out real-only quantum theory in 2021, and that the Fourier basis functions are complex exponentials, which are the continuous extension of the eight discrete phases.

The plain consequence is that complex numbers are not an optional convenience in this account; they are forced by the existence of a cyclic phase structure. The framework's theorem complex_from_ledger is a placeholder that asserts the implication from an eight-tick ledger to the complex numbers, but it is tagged as trivial, meaning the formal derivation of that bridge is not yet complete. What is proved is the mathematical backbone: the phases are complex, they rotate, and no smaller number system can represent them.

/-- **THEOREM**: The 8 tick phases are 8th roots of unity. -/
theorem tick_phases_roots_of_unity (k : Fin 8) :
    (tickPhase k)^8 = 1 := by
  unfold tickPhase
  -- exp(I × π × k / 4)^8 = exp(8 × I × π × k / 4) = exp(2πIk) = 1
  rw [← Complex.exp_nat_mul]
  have h : (8 : ℕ) * (I * ↑π * ↑(k : ℕ) / 4) = ↑(k : ℕ) * (2 * ↑π * I) := by
    push_cast
    ring
  rw [h]
  exact Complex.exp_nat_mul_two_pi_mul_I k

/-- The phases are equally spaced around the unit circle.
    Consecutive phases differ by π/4 (45°). -/
theorem tick_phases_equally_spaced (j k : Fin 8) (hjk : j < k) :
    -- The quotient tickPhase k / tickPhase j has argument (k - j) * π/4 modulo 2π
    tickPhase k / tickPhase j = Complex.exp ((k.val - j.val : ℝ) * π / 4 * I) := by
  unfold tickPhase
  -- Use exp_sub: exp(a) / exp(b) = exp(a - b)
  rw [← Complex.exp_sub]
  congr 1
  -- Show: I * π * k / 4 - I * π * j / 4 = (k - j) * π / 4 * I
  push_cast
  ring

/-- General statement: for k ∈ {1,2,3,5,6,7}, the tick phase has nonzero imaginary part. -/
theorem phases_require_complex (k : Fin 8) (hk : k.val ≠ 0 ∧ k.val ≠ 4) :
    (tickPhase k).im ≠ 0 := by
  -- For phases 1,2,3,5,6,7, sin(k*π/4) ≠ 0
  unfold tickPhase
  have h_exp : I * π * k / 4 = ↑((k.val : ℝ) * π / 4 : ℝ) * I := by push_cast; ring
  rw [h_exp, Complex.exp_mul_I]
  rw [← Complex.ofReal_cos, ← Complex.ofReal_sin]
  simp only [Complex.add_im, Complex.mul_I_im, Complex.ofReal_im, Complex.ofReal_re, zero_add]
  -- sin(k * π / 4) ≠ 0 when k ∉ {0, 4}
  intro h_sin
  rw [Real.sin_eq_zero_iff] at h_sin
  rcases h_sin with ⟨n, hn⟩
  -- k * π / 4 = n * π implies k = 4n
  have h_eq : (k.val : ℤ) = 4 * n := by
    have : (k.val : ℝ) * π / 4 = n * π := hn.symm
    field_simp [Real.pi_ne_zero] at this
    exact_mod_cast this
  -- k ∈ {0,...,7} and k = 4n implies n ∈ {0, 1}, hence k ∈ {0, 4}
  have h_n_range : n = 0 ∨ n = 1 := by
    have h1 : 0 ≤ (k.val : ℤ) := Int.natCast_nonneg _
    have h2 : (k.val : ℤ) < 8 := by omega
    omega
  cases h_n_range with
  | inl h0 =>
    simp only [h0, mul_zero, Int.cast_zero] at h_eq
    have : k.val = 0 := by omega
    exact hk.left this
  | inr h1 =>
    simp only [h1, mul_one, Int.cast_one] at h_eq
    have : k.val = 4 := by omega
    exact hk.right this

/-- Complex multiplication includes rotation.
    z × w rotates z by arg(w) and scales by |w|. -/
theorem complex_rotation (z w : ℂ) :
    -- |z × w| = |z| × |w| (scaling)
    -- arg(z × w) = arg(z) + arg(w) modulo 2π (rotation) when both are nonzero
    ‖z * w‖ = ‖z‖ * ‖w‖ ∧
    (∀ hz : z ≠ 0, ∀ hw : w ≠ 0, (Complex.arg (z * w) : Real.Angle) = Complex.arg z + Complex.arg w) := by
  constructor
  · exact Complex.norm_mul z w
  · intro hz hw
    -- Use arg_mul_coe_angle which works modulo 2π
    exact Complex.arg_mul_coe_angle hz hw

/-- In RS, complex numbers arise because:

    1. The ledger has 8 ticks (discrete)
    2. Ticks are phases (cyclic)
    3. Phase differences matter (interference)
    4. Phase is additive under composition
    5. The unique structure satisfying these is ℂ

    Complex numbers aren't a human invention - they're forced by nature! -/
theorem complex_from_ledger :
    -- 8-tick ledger → cyclic phases → ℂ
    True := trivial

What this page does not claim

The framework does not formally prove that an eight-tick ledger implies the complex numbers; the theorem complex_from_ledger is a trivial placeholder. The framework does not derive the specific value of the imaginary unit i from first principles. The framework does not claim that quaternions are never useful in physics, only that they are not the minimal system for representing a two-dimensional phase.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Mathematics/ComplexNumbers.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: