Foundation Complex Structure Forcing

Complex structure forcing

In linear algebra, a rotation by 90 degrees is a simple operation: it sends a point (x, y) to (-y, x). If you apply it four times, you return to the start. But no real number, when squared, gives -1, so this rotation has no real eigenvalue. Its natural description lives in the complex plane, where the number i, with i² = -1, provides the missing coordinate. The same necessity appears in Recognition Science when an eight-step cycle of states is studied.

The framework's recognition process, a discrete record of events, produces a cyclic shift operator T that moves a signal forward by one step and satisfies T⁸ = I, meaning eight shifts return the signal to its original form. The eigenvalues of this operator are the 8th roots of unity, the complex numbers ωᵏ = e^(2πik/8). Among these, the eigenvalue ω² equals i, the imaginary unit. Since no real number squares to -1, the operator cannot be diagonalized using only real numbers. The framework's library proves this directly: the theorem complexification_forced states that one eigenvalue is i and that x² + 1 is never zero for any real x.

This algebraic fact has a physical consequence: the state space must be complex. The framework models signals as functions from the eight positions to complex numbers, written Signal8 = Fin 8 → ℂ. The shift operator acts on this space, and the discrete Fourier transform of length 8 (DFT-8) provides the canonical basis that diagonalizes it. Each basis vector is an eigenvector of the shift, and the transform preserves the inner product, a property known as Parseval's identity. The framework proves that the shift cannot have a real eigenbasis at all: the theorem no_real_tick_eigenbasis states that no basis of real-valued signals exists where every basis vector is an eigenvector of the real shift operator.

In Recognition Science, this complexification is not a choice but a forced step. The cost function J, which measures the price of recognition, depends only on the magnitude of a complex number, not its phase. The theorem jcost_phase_invariant proves that multiplying a signal by a unit complex number e^(iθ) leaves the cost unchanged. This phase invariance means that the physical content of a state lies in its modulus, while the phase carries no cost. The framework's library shows that the total mode cost, summed over all eight components, is likewise invariant under independent phase changes of each component.

The result closes a gap in the framework's derivation: the cost axioms force an eight-tick cycle, and that cycle forces complex numbers, and complex numbers enable a unitary evolution operator. The framework models evolution as a linear map on the complex signal space, and the DFT-8 provides the natural diagonal form. This is not a claim that the physical world is made of complex numbers; it is a claim that the mathematics of an eight-step periodic process, when combined with the cost structure, requires complex amplitudes to describe it completely.

/-- **THEOREM (Complexification is Forced)**:
    The shift operator T on Signal8 has eigenvalue i (at k=2).
    Since i is not real (no real x satisfies x² + 1 = 0), the eigenspace
    decomposition of T REQUIRES ℂ. Working over ℝ alone, T can only
    be block-diagonalized into 2×2 rotation matrices — it cannot
    be fully diagonalized.

    This is the core theorem: the 8-tick forces ℂ. -/
theorem complexification_forced :
    (∃ k : Fin 8, eigenvalue k = Complex.I) ∧
    (∀ x : ℝ, x ^ 2 + 1 ≠ 0) := by
  exact ⟨⟨⟨2, by norm_num⟩, eigenvalue_2_is_I⟩, x2_plus_1_no_real_root⟩

/-- No real basis of the 8-register consists entirely of one-dimensional tick eigenstates. -/
theorem no_real_tick_eigenbasis :
    ¬ (∃ (b : Module.Basis (Fin 8) ℝ RealSignal8) (mu : Fin 8 → ℝ),
        ∀ k, realShift (b k) = mu k • b k) := by
  classical
  rintro ⟨b, mu, hb⟩
  let W : Submodule ℝ RealSignal8 :=
    { carrier := {v | v (2 : Fin 8) = v 0}
      zero_mem' := rfl
      add_mem' := by
        intro x y hx hy
        have hx' : x (2 : Fin 8) = x 0 := hx
        have hy' : y (2 : Fin 8) = y 0 := hy
        show x (2 : Fin 8) + y (2 : Fin 8) = x 0 + y 0
        rw [hx', hy']
      smul_mem' := by
        intro c x hx
        have hx' : x (2 : Fin 8) = x 0 := hx
        show c • x (2 : Fin 8) = c • x 0
        rw [hx'] }
  have hbW : Set.range (fun k => b k) ⊆ W := by
    rintro v ⟨k, rfl⟩
    have hper := realShift_eigenvector_two_periodic (mu k) (b k) (b.ne_zero k) (hb k) 0
    simpa [W, nextIdx] using hper
  have hspan_le : Submodule.span ℝ (Set.range fun k => b k) ≤ W :=
    Submodule.span_le.mpr hbW
  have htop_le : (⊤ : Submodule ℝ RealSignal8) ≤ W := by
    simpa [Module.Basis.span_eq] using hspan_le
  have hWtop : W = ⊤ := le_antisymm le_top htop_le
  let e0 : RealSignal8 := Pi.single (0 : Fin 8) (1 : ℝ)
  have he0_mem : e0 ∈ W := by
    rw [hWtop]
    trivial
  have he0_not_mem : e0 ∉ W := by
    intro he
    have h20 : (2 : Fin 8) ≠ 0 := by decide
    simpa [W, e0, h20] using he
  exact he0_not_mem he0_mem

/-- **THEOREM (Phase Invariance of J-Cost)**:
    J(‖z‖) = J(‖z·e^{iθ}‖) for any phase θ.
    The cost functional depends ONLY on the modulus, not the phase.
    This is the root cause of the Born rule: P = |ψ|² is the unique
    probability function that respects cost-phase invariance. -/
theorem jcost_phase_invariant (z : ℂ) (θ : ℝ) :
    JcostC z = JcostC (z * Complex.exp (↑θ * Complex.I)) := by
  simp only [JcostC]
  congr 1
  rw [norm_mul]
  have : ‖Complex.exp (↑θ * Complex.I)‖ = 1 := by
    rw [Complex.norm_exp_ofReal_mul_I]
  rw [this, mul_one]

/-- **THEOREM (Mode Cost is Phase-Invariant)**:
    Rotating each mode by an independent phase does not change
    the total cost. This means the cost landscape has a U(1)⁸
    gauge symmetry in the mode basis.

    Combined with the norm constraint, this forces the dynamics
    to be unitary: any cost-preserving, norm-preserving linear
    map on ℂ⁸ is unitary. -/
theorem mode_cost_phase_invariant (f : Signal8) (phases : Fin 8 → ℝ) :
    totalModeCost f =
    totalModeCost (fun k => f k * Complex.exp (↑(phases k) * Complex.I)) := by
  simp only [totalModeCost]
  congr 1; ext k; congr 1
  rw [norm_mul, Complex.norm_exp_ofReal_mul_I, mul_one]

/-- **COROLLARY**: The DFT-8 preserves the norm: ‖F(f)‖² = ‖f‖². -/
theorem dft8_preserves_norm (f : Signal8) :
    inner8 (dft8 f) (dft8 f) = inner8 f f :=
  dft8_preserves_inner f f

What this page does not claim

This does not claim that physical space itself is complex, only that the state space of the eight-tick cycle requires complex amplitudes. This does not claim that the complexification alone produces the three spatial dimensions; that result depends on the separate linking closure theorem.

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/Foundation/ComplexStructureForcing.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: