Foundation Complex Structure Forcing Dft Tick Basis Is Tick Eigenvector

The tick shift and its eigenbasis

The discrete Fourier transform (DFT) is a standard tool that decomposes a periodic signal into a sum of pure frequency components. For a signal with eight time steps, the DFT uses the eight complex eighth roots of unity, numbers like i and -1, as its building blocks. The eigenvectors of the shift operator, which moves every entry one position forward, are exactly these frequency components. This is a classical fact of linear algebra.

In Recognition Science, the framework's library contains a machine-checked proof of this fact for its own eight-step model. The declaration dftBasis_is_tick_eigenvector states that shifting a DFT basis vector is the same as multiplying it by its corresponding eigenvalue. This is a theorem, proved in the framework's formal library. It means that the eight frequency components form a complete set of axes along which the shift operation acts by simple scaling, a property that makes the DFT the natural coordinate system for studying the eight-step cycle.

The framework's deeper point is that this complex structure is not an optional convenience. Its library proves that the shift operator, which cycles through eight states, cannot be diagonalized using only real numbers. The eigenvalue i, which appears for the second frequency component, has no real counterpart because no real number squares to -1. The library proves this algebraically: for every real x, the value x² + 1 is never zero. Therefore, the framework concludes, moving to complex numbers is forced by the mathematics of the eight-step cycle, not a choice made for convenience.

This complex basis also respects the framework's cost function. The library proves that the cost of a mode depends only on its magnitude, not its phase, and that the DFT preserves the inner product of signals. These results mean that the complex frequency representation is a faithful and cost-neutral way to analyze the eight-step dynamics, closing a gap between the framework's basic axioms and the full complex Hilbert space structure it uses.

What the declaration does not claim is also important. It does not prove that the physical world is made of complex numbers, nor does it claim that the eight-step cycle is the only structure in the framework. It establishes a precise algebraic relationship within a specific model, and the forcing argument applies to that model's shift operator, not to all possible linear maps. The theorem is a piece of internal mathematics, not a statement about empirical reality.

/-- The local DFT vectors are tick eigenvectors over `ℂ`. -/
theorem dftBasis_is_tick_eigenvector (k : Fin 8) :
    shift (dftBasis k) = eigenvalue k • dftBasis k := by
  funext j
  simp only [shift, dftBasis, eigenvalue, nextIdx, Pi.smul_apply, smul_eq_mul]
  have hzk : (ζ ^ k.val) ^ 8 = 1 := by
    rw [← pow_mul, mul_comm, pow_mul, ζ_pow_8, one_pow]
  calc
    ζ ^ (k.val * ((j.val + 1) % 8))
        = (ζ ^ k.val) ^ ((j.val + 1) % 8) := by rw [← pow_mul]
    _ = (ζ ^ k.val) ^ ((j.val + 1) % 8 + 8 * ((j.val + 1) / 8)) := by
      rw [pow_add, pow_mul, hzk, one_pow, mul_one]
    _ = (ζ ^ k.val) ^ (j.val + 1) := by rw [Nat.mod_add_div]
    _ = ζ ^ (k.val * (j.val + 1)) := by rw [← pow_mul]
    _ = ζ ^ (k.val * j.val + k.val) := by rw [Nat.mul_succ]
    _ = ζ ^ k.val * ζ ^ (k.val * j.val) := by
      rw [pow_add]
      ring

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

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

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

The declaration does not prove that physical reality is fundamentally complex-valued. The forcing argument applies only to the eight-step shift operator, not to all linear maps. The theorem does not establish the empirical correctness of the framework's eight-step model.

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: