Foundation Complex Structure Forcing Complex Structure Certificate

The forced complex numbers

The declaration complex_structure_certificate establishes a specific mathematical fact: a certain eight-step cyclic process, which the framework calls the eight-tick cycle (a repeating sequence of eight discrete states), cannot be completely analyzed using only real numbers. The process is represented by a shift operator, which moves a signal one step forward in the cycle. Applying this shift eight times returns the signal to its starting point, a property expressed as T⁸ = I.

For such an operator to be fully understood, one looks for its eigenvectors and eigenvalues, the special directions and scaling factors that the operator leaves unchanged in direction. The eigenvalues of this eight-step shift are the eight complex numbers that satisfy ω⁸ = 1, the eighth roots of unity. Among these is the number i, the imaginary unit, which satisfies i² = -1. No real number has this property, since the square of any real number is never negative. The theorem complexification_forced proves this directly: it states that the eigenvalue i exists and that no real number x satisfies x² + 1 = 0.

Because one of the eigenvalues is not a real number, the shift operator cannot be diagonalized over the real numbers. A basis of real eigenvectors that would fully decompose the operator does not exist; the theorem no_real_tick_eigenbasis proves this absence. The mathematics therefore forces an extension to the complex numbers, where all eight eigenvalues exist and the operator can be diagonalized. This is the core meaning of the declaration: the complex structure is not an optional convenience but a logical necessity.

In Recognition Science, this result closes a specific gap. The framework's cost function, which assigns a cost to each recognition event, depends only on the magnitude (absolute value) of a complex number, not on its phase (angle). The theorems jcost_phase_invariant and mode_cost_phase_invariant prove this phase invariance. This fact, combined with the forced complexification, provides the structure needed for a genuine unitary evolution, where the total cost of a system is preserved over time. The declaration thus establishes the mathematical foundation for the complex Hilbert space structure used in the framework's account of quantum mechanics.

What the declaration does not claim is equally important. It does not prove that the physical world is made of complex numbers, nor does it derive the rules of quantum mechanics from the cost function. It proves a purely algebraic theorem: given an eight-step cyclic shift, the complex numbers are required for its complete spectral analysis. The physical interpretation of this mathematics, and the bridge from the cost axioms to observed quantum phenomena, remains a separate and open question within the framework.

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

/-- **COROLLARY**: The polynomial x² + 1 has no real roots. -/
theorem x2_plus_1_no_real_root : ∀ x : ℝ, x ^ 2 + 1 ≠ 0 :=
  fun x => ne_of_gt (no_real_root_x2_plus_1 x)

/-- **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]

What this page does not claim

The declaration does not prove that the physical world is fundamentally complex-valued. The declaration does not derive the full formalism of quantum mechanics from the cost function. The declaration does not claim that the complexification is a physical process; it is a mathematical requirement.

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: