Foundation Complex Structure Forcing Real Shift Eigenvalue Sq One

The real shift's square

An eight-step cycle is a rotation of eight positions, like the hours on a clock or the days of a week. In the Recognition Science framework, the cycle acts on a discrete record of eight real numbers, one per tick, a tick being one step of the cycle. The operation that moves each entry one position forward is the shift. The question is which real numbers can serve as scaling factors when the shift is applied to a nonzero real signal, meaning a list of eight real numbers that is not all zeros. The answer, proved in the framework's machine-checked library of formal theorems, is stark: the only real scalars that work are 1 and -1, because the scaling factor must satisfy its square equals one.

The proof is short and depends only on the cycle's period. Applying the shift eight times returns the original signal, since the cycle closes after eight steps. If a real number lam scales the signal under one shift, then applying the shift eight times scales the signal by lam to the eighth power. But the signal returns to itself, so lam to the eighth equals one. For a real number, the only way its eighth power equals one is if its square equals one, so lam is either 1 or -1. The formal statement is realShift_eigenvalue_sq_one, a theorem in the framework's library that takes a nonzero real signal, assumes the shift equals lam times the signal, and concludes lam squared equals one.

This fact matters because it exposes a limitation of working only with real numbers. The same cycle, when allowed complex entries, has eight distinct scaling factors, the eighth roots of unity, including the imaginary unit i, whose square is -1. The real setting cannot see those: it only sees the two real scalars. The framework reads this as a forced step: to describe the full cycle, one must pass from real to complex numbers. The theorem itself does not perform that passage; it only establishes the real constraint. The companion result that no real basis of eigenvectors exists for the shift is a separate theorem, and the complexification is a further conclusion drawn from the whole collection of results.

In Recognition Science, this result is one link in a chain that leads from the cost function to complex Hilbert-space structure. The framework's library proves that the cost depends only on the modulus of a complex number, not its phase, and that the discrete Fourier transform of length eight preserves the inner product. Those results, together with the eigenvalue constraint, support the framework's claim that complex structure is forced rather than chosen. But the single theorem about the real shift's square does not by itself establish unitarity, the Fourier transform, or the full complexification; it only pins down the real scalars.

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

/-- **THEOREM (8-Tick Periodicity)**: T⁸ = id.
    Applying the shift 8 times returns to the original signal.
    This is the fundamental periodicity of the recognition clock. -/
theorem shift_period_8 (f : Signal8) : shiftIter 8 f = f := by
  funext k
  simp only [shiftIter, Function.comp_apply, shift]
  exact congrArg f (nextIdx_8 k)

/-- The k=2 eigenvalue is exactly i = √(-1). -/
theorem eigenvalue_2_is_I :
    eigenvalue ⟨2, by norm_num⟩ = Complex.I := by
  simp only [eigenvalue]
  exact ζ_sq_eq_I

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

What this page does not claim

The theorem does not prove that complex numbers are needed for the shift; that is a separate conclusion from the lack of a real eigenbasis. The theorem does not establish the discrete Fourier transform or its norm-preserving property. The theorem does not imply that the framework's cost function is phase-invariant or that unitarity holds for the full evolution.

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: