/-
  JORDAN FIXED-POINT COMMUTATIVITY — MATRIX-LEVEL PROOF
  Ahmad Ali Parr · SnapKitty Collective · 2026-07-21

  Theorem: For the Jordan operator
    T(ρ) = φ⁻¹ · U * ρ * Uᴴ + φ⁻² · ρ
  any fixed point ρ* satisfying T(ρ*) = ρ* commutes with U:
    U * ρ* = ρ* * U   (i.e., [U, ρ*] = 0)

  Proof is purely algebraic — no analysis, no epsilon-delta.
  Uses only: linear algebra over ℂ, scalar cancellation, matrix multiplication.

  PAR-013: Fibonacci-Banach contraction (scalar bound)
  PAR-011: Jordan Spectral Transformer fixed-point commutativity (this file)
-/

import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Algebra.Star.Basic

namespace JordanMatrixProof

variable {n : Type*} [Fintype n] [DecidableEq n]

-- φ⁻¹ as an element of ℂ
noncomputable def φ_inv : ℂ := (Real.sqrt 5 - 1) / 2

-- φ⁻² = φ⁻¹²  (since φ² = φ + 1 ⟹ φ⁻² = 1 - φ⁻¹ · φ⁻¹ ... use the identity directly)
noncomputable def φ_inv_sq : ℂ := 1 - φ_inv

-- The key algebraic identity: φ⁻¹ + φ⁻² = 1
theorem phi_sum_one : φ_inv + φ_inv_sq = 1 := by
  simp [φ_inv_sq]

-- φ⁻¹ ≠ 0  (since φ⁻¹ = (√5-1)/2 ≈ 0.618 ≠ 0)
theorem phi_inv_ne_zero : φ_inv ≠ 0 := by
  simp [φ_inv]
  intro h
  have h5 : Real.sqrt 5 > 0 := Real.sqrt_pos.mpr (by norm_num)
  linarith [h5]

-- ════════════════════════════════════════════════════════════════
-- MAIN THEOREM: Jordan Fixed-Point Commutativity
-- ════════════════════════════════════════════════════════════════

/--
  For the Jordan operator T(ρ) = φ⁻¹ · U * ρ * Uᴴ + φ⁻² · ρ,
  any fixed point ρ* satisfying T(ρ*) = ρ* commutes with U.

  Proof:
    T(ρ*) = ρ*
    ⟹ φ⁻¹ · U * ρ* * Uᴴ + φ⁻² · ρ* = ρ*
    ⟹ φ⁻¹ · U * ρ* * Uᴴ = (1 - φ⁻²) · ρ* = φ⁻¹ · ρ*
                            [using phi_sum_one: 1 - φ⁻² = φ⁻¹]
    ⟹ U * ρ* * Uᴴ = ρ*    [divide by φ⁻¹ ≠ 0]
    ⟹ U * ρ* * Uᴴ = ρ*

  Commutativity U * ρ* = ρ* * U then follows because U is unitary:
    U * ρ* * Uᴴ = ρ*
    ⟹ U * ρ* = ρ* * U      [right-multiply by U, use Uᴴ * U = I]
-/
theorem jordan_fixed_point_commutes
    (U ρ_star : Matrix n n ℂ)
    -- U is unitary: U * Uᴴ = I  and  Uᴴ * U = I
    (hU_mul  : U * star U = 1)
    (hUH_mul : star U * U = 1)
    -- ρ* is the fixed point: T(ρ*) = ρ*
    (h_fp : φ_inv • (U * ρ_star * star U) + φ_inv_sq • ρ_star = ρ_star) :
    -- Conclusion: ρ* commutes with U
    U * ρ_star = ρ_star * U := by

  -- Step 1: From fixed-point equation, isolate φ⁻¹ · U ρ* Uᴴ
  have step1 : φ_inv • (U * ρ_star * star U) = (1 - φ_inv_sq) • ρ_star := by
    have key : φ_inv • (U * ρ_star * star U) + φ_inv_sq • ρ_star = ρ_star := h_fp
    have sum1 : φ_inv + φ_inv_sq = 1 := phi_sum_one
    rw [← sum1, add_smul] at key
    have eq : φ_inv • (U * ρ_star * star U) + φ_inv_sq • ρ_star =
              φ_inv • ρ_star + φ_inv_sq • ρ_star := key
    have h1 : φ_inv • (U * ρ_star * star U) = φ_inv • ρ_star := by linarith
    rw [show (1 : ℂ) - φ_inv_sq = φ_inv by linarith [sum1]]
    exact h1

  -- Step 1 (matrix version over ℂ):
  have step1' : φ_inv • (U * ρ_star * star U) = φ_inv • ρ_star := by
    have key : φ_inv • (U * ρ_star * star U) + φ_inv_sq • ρ_star = ρ_star := h_fp
    have sum1 : φ_inv + φ_inv_sq = 1 := phi_sum_one
    -- Rewrite ρ* = 1 • ρ* = (φ⁻¹ + φ⁻²) • ρ*
    rw [← sum1, add_smul] at key
    -- key : φ⁻¹ • (U ρ* Uᴴ) + φ⁻² • ρ* = φ⁻¹ • ρ* + φ⁻² • ρ*
    have : φ_inv • (U * ρ_star * star U) + φ_inv_sq • ρ_star =
           φ_inv • ρ_star + φ_inv_sq • ρ_star := key
    linarith -- over an additive group with smul, cancel φ⁻² • ρ* from both sides

  -- Step 2: Cancel φ⁻¹ ≠ 0 from both sides
  have step2 : U * ρ_star * star U = ρ_star := by
    have hne := phi_inv_ne_zero
    exact smul_left_cancel₀ hne step1'

  -- Step 3: U * ρ* * Uᴴ = ρ* ⟹ U * ρ* = ρ* * U
  -- Right-multiply both sides by U:  (U * ρ* * Uᴴ) * U = ρ* * U
  -- LHS = U * ρ* * (Uᴴ * U) = U * ρ* * I = U * ρ*
  calc U * ρ_star
      = U * ρ_star * 1            := by simp
    _ = U * ρ_star * (star U * U) := by rw [hUH_mul]
    _ = (U * ρ_star * star U) * U := by ring
    _ = ρ_star * U                := by rw [step2]

-- ════════════════════════════════════════════════════════════════
-- SCALAR CONTRACTION BOUND (supports the contraction claim)
-- Over ℝ, not IEEE Float
-- ════════════════════════════════════════════════════════════════

/--
  The scalar sequence (φ⁻¹)^N is strictly decreasing:
  φ⁻¹^(N+1) < φ⁻¹^N   iff   φ⁻¹ ∈ (0, 1)
  This is a necessary condition for Banach contraction.
  (The full operator contraction on density matrices requires
   the signal-dependent U_k averaging argument; this gives the scalar rate.)
-/
theorem phi_inv_pow_lt (N : ℕ) :
    (0 : ℝ) < (Real.sqrt 5 - 1) / 2 ∧
    (Real.sqrt 5 - 1) / 2 < 1 ∧
    ((Real.sqrt 5 - 1) / 2) ^ (N + 1) < ((Real.sqrt 5 - 1) / 2) ^ N := by
  constructor
  · -- 0 < (√5 - 1)/2
    apply div_pos
    · have : Real.sqrt 5 > 1 := by
        rw [show (1:ℝ) = Real.sqrt 1 from (Real.sqrt_one).symm]
        exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
      linarith
    · norm_num
  constructor
  · -- (√5 - 1)/2 < 1
    have h5 : Real.sqrt 5 < 3 := by
      rw [show (3:ℝ) = Real.sqrt 9 from by
        rw [Real.sqrt_eq_iff_sq_eq (by norm_num) (by norm_num)]; norm_num]
      exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
    linarith
  · -- (φ⁻¹)^(N+1) < (φ⁻¹)^N
    apply pow_lt_pow_of_lt_one
    · apply div_pos
      · have : Real.sqrt 5 > 1 := by
          rw [show (1:ℝ) = Real.sqrt 1 from (Real.sqrt_one).symm]
          exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
        linarith
      · norm_num
    · have h5 : Real.sqrt 5 < 3 := by
        rw [show (3:ℝ) = Real.sqrt 9 from by
          rw [Real.sqrt_eq_iff_sq_eq (by norm_num) (by norm_num)]; norm_num]
        exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
      linarith

-- ════════════════════════════════════════════════════════════════
-- DENSITY MATRIX PRESERVATION UNDER JORDAN STEP
-- ════════════════════════════════════════════════════════════════

/--
  If ρ has trace 1 and U is unitary, then T(ρ) = φ⁻¹ · UρUᴴ + φ⁻² · ρ
  also has trace 1.
  Uses: tr(U ρ Uᴴ) = tr(ρ) for any unitary U (cyclic trace).
-/
theorem jordan_preserves_trace
    (U ρ : Matrix n n ℂ)
    (hU : U * star U = 1)
    (htr : Matrix.trace ρ = 1) :
    Matrix.trace (φ_inv • (U * ρ * star U) + φ_inv_sq • ρ) = 1 := by
  rw [map_add, map_smul, map_smul]
  -- tr(U ρ Uᴴ) = tr(ρ) by cyclic property: tr(ABC) = tr(CAB)
  have cyclic : Matrix.trace (U * ρ * star U) = Matrix.trace ρ := by
    rw [Matrix.trace_mul_comm (U * ρ) (star U)]
    rw [Matrix.mul_assoc]
    rw [hU]
    simp [Matrix.trace_mul_comm]
  rw [cyclic, htr]
  -- φ⁻¹ · 1 + φ⁻² · 1 = 1
  have : φ_inv + φ_inv_sq = 1 := phi_sum_one
  push_cast
  linarith

end JordanMatrixProof