Foundation Complex Structure Forcing X2 Plus 1 Divides X8 Minus 1

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

/-- **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 (Phase Invariance — Explicit)**:
    Multiplying a mode amplitude by a unit-modulus phase e^{iθ}
    does not change the J-cost. This is the structural reason
    why probability depends on |ψ|² and not on arg(ψ). -/
theorem jcost_modulus_only (r : ℝ) (hr : 0 < r) (θ : ℝ) :
    Cost.Jcost r = Cost.Jcost ‖(↑r : ℂ) * Complex.exp (↑θ * Complex.I)‖ := by
  rw [norm_mul, Complex.norm_exp_ofReal_mul_I, mul_one]
  congr 1
  simp [Complex.norm_real, abs_of_pos hr]

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

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