Foundation Complex Structure Forcing Real Shift Eigenvector Two Periodic

The real shift's eigenvalue constraint

A ledger (a discrete record of events) that cycles through eight positions has a natural operation: move everything one step forward, wrapping around after the eighth. This is the shift operator. The question is what numbers can describe its behavior when the entries are real. The answer, proved in the framework's machine-checked library of formal theorems, is that a real-valued eigenvector, a nonzero vector that the shift merely scales, can only have a scaling factor of 1 or -1. The theorem realShift_eigenvalue_sq_one states that if a real vector satisfies the shift equation, its eigenvalue squared must equal one.

The reason is simple. If you shift an eight-step cycle eight times, you return to the start. This means the eighth power of the scaling factor is one. Over the real numbers, the only solutions to x^8 = 1 are x = 1 and x = -1. The theorem proves exactly this constraint. It does not say that every real vector is an eigenvector, nor that the shift can be fully described by real eigenvectors. In fact, a separate theorem, no_real_tick_eigenbasis, proves that no basis of real eigenvectors exists for this shift at all.

The obstruction is the number i, the imaginary unit. The shift operator has eigenvalues that are the eighth roots of unity, and among them is i itself. Since no real number squared equals -1, the eigenvalue i cannot correspond to a real eigenvector. The theorem complexification_forced captures this: there exists an eigenvalue equal to i, and no real number satisfies x^2 + 1 = 0. This is why the framework says complex numbers are forced, not chosen. The real shift is a concrete example of a broader phenomenon: a simple periodic structure can demand complex numbers for its complete description.

What the theorem does not claim is that it introduces complex numbers into the framework. The complex shift operator and its eigenvectors are defined separately. It also does not claim that the real shift is useless; it is a well-defined operation on real vectors. The theorem only constrains what eigenvalues are possible for real eigenvectors. It is a precise, limited statement about the real-number description of an eight-step cycle, and it sets the stage for the framework's claim that complex Hilbert space structure is a necessary consequence of the cost axioms.

/-- A real one-dimensional tick eigenstate has eigenvalue squaring to one. -/
theorem realShift_eigenvalue_sq_one (lam : ℝ) (v : RealSignal8)
    (hv : v ≠ 0) (h : realShift v = lam • v) :
    lam ^ 2 = 1 := by
  classical
  obtain ⟨k, hk⟩ : ∃ k, v k ≠ 0 := by
    by_contra hnone
    have hz : ∀ k, ¬ v k ≠ 0 := not_exists.mp hnone
    apply hv
    funext k
    exact not_not.mp (hz k)
  have hcycle :
      v (nextIdx (nextIdx (nextIdx (nextIdx
        (nextIdx (nextIdx (nextIdx (nextIdx k)))))))) = v k := by
    exact congrArg v (nextIdx_8 k)
  have heig := realShift_eigen_step_eight lam v h k
  have hlam8_mul : lam ^ 8 * v k = 1 * v k := by
    rw [← heig, hcycle, one_mul]
  have hlam8 : lam ^ 8 = 1 := mul_right_cancel₀ hk hlam8_mul
  have hprod : (lam ^ 2 - 1) * (lam ^ 2 + 1) * (lam ^ 4 + 1) = 0 := by
    calc
      (lam ^ 2 - 1) * (lam ^ 2 + 1) * (lam ^ 4 + 1)
          = lam ^ 8 - 1 := by ring
      _ = 0 := by rw [hlam8, sub_self]
  have hplus2 : lam ^ 2 + 1 ≠ 0 := by
    nlinarith [sq_nonneg lam]
  have hplus4 : lam ^ 4 + 1 ≠ 0 := by
    nlinarith [sq_nonneg (lam ^ 2)]
  have hminus : lam ^ 2 - 1 = 0 := by
    rcases mul_eq_zero.mp hprod with hleft | hright
    · exact (mul_eq_zero.mp hleft).resolve_right hplus2
    · exact False.elim (hplus4 hright)
  exact sub_eq_zero.mp hminus

/-- 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 (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⟩

What this page does not claim

This theorem does not introduce complex numbers into the framework. This theorem does not claim that the real shift operator is undefined or unusable. This theorem does not prove that every real vector is an eigenvector of the shift.

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: