IndisputableMonolith.Gravity.QuantumChannel.MediatorUniversalityBoundary

   1import Mathlib
   2import IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForced
   3
   4/-!
   5# Gravity quantum channel: mediator universality boundary
   6
   7The vector-level no-go lives in
   8`Gravity.QuantumChannel.AmplitudeLinearForced` and
   9`Gravity.QuantumChannel.NoClassicalMediator`; it is not re-proved here.
  10That result says a vector response on `Signal8` cannot be simultaneously
  11amplitude-linear, density-only, and nonzero.
  12
  13This module proves the exact boundary of the universality premise. For every
  14fixed update `U`, the density-level map `rho ↦ U * rho * Uᴴ` exists, reproduces
  15the amplitude dynamics on pure states, is phase-insensitive on pure densities,
  16and is trace-preserving when `U` is unitary. Thus algebra alone does not
  17exclude update-dependent mediation.
  18
  19The new density-level no-go is also formalized: even at density level, no
  20single fixed map serves all unitary updates. The identity update and the
  210-1 swap already disagree on the same input density.
  22
  23Honesty note on strength: the no-go is a quantifier-order fact (a fixed
  24`Phi` with `forall U` versus `forall U` each with its own `Phi`), witnessed
  25by a one-shot clash of two unitaries on one pure density. Its value is that
  26it makes the strong reading of the universality premise exact and
  27kernel-checked, not that it is a deep new density-level obstruction. It
  28formalizes the strongest reading of universality (one fixed map implementing
  29every unitary update simultaneously); weaker readings (update-parameterized
  30families, a single CP architecture) are untouched and remain the MODEL
  31premise. This module does not remove the premise, and it must never be
  32quoted as "algebra forbids density mediation": the positive half proves the
  33opposite for every fixed update.
  34
  35Zero `sorry`. Zero new axioms.
  36-/
  37
  38namespace IndisputableMonolith
  39namespace Gravity
  40namespace QuantumChannel
  41namespace MediatorUniversalityBoundary
  42
  43open AmplitudeLinearForced
  44
  45noncomputable section
  46
  47/-! ## Pure densities -/
  48
  49/-- The pure-state density matrix `|psi><psi|`. -/
  50def densityOf (psi : Signal8) : Matrix (Fin 8) (Fin 8) Complex :=
  51  Matrix.of fun i j => psi i * star (psi j)
  52
  53/-- Pure-state densities are invariant under unit-modulus global phase. -/
  54theorem densityOf_phase_invariant
  55    (c : Complex) (hc : ‖c‖ = 1) (psi : Signal8) :
  56    densityOf (c • psi) = densityOf psi := by
  57  ext i j
  58  unfold densityOf
  59  simp only [Matrix.of_apply, Pi.smul_apply, smul_eq_mul]
  60  have hnormSqReal : Complex.normSq c = 1 := by
  61    rw [Complex.normSq_eq_norm_sq, hc]
  62    norm_num
  63  have hmul : c * star c = 1 := by
  64    calc
  65      c * star c = (Complex.normSq c : Complex) := by
  66        rw [Complex.star_def, Complex.mul_conj]
  67      _ = 1 := by
  68        exact_mod_cast hnormSqReal
  69  calc
  70    (c * psi i) * star (c * psi j)
  71        = (c * star c) * (psi i * star (psi j)) := by
  72          rw [star_mul]
  73          ring
  74    _ = psi i * star (psi j) := by
  75      rw [hmul, one_mul]
  76
  77/-- The trace of a pure density is the sum of squared amplitudes. -/
  78theorem trace_densityOf (psi : Signal8) :
  79    (densityOf psi).trace = ∑ k : Fin 8, psi k * star (psi k) := by
  80  simp [densityOf, Matrix.trace]
  81
  82/-- The density of the first basis vector is nonzero. -/
  83theorem densityOf_single_ne_zero :
  84    densityOf (Pi.single (0 : Fin 8) (1 : Complex)) ≠ 0 := by
  85  intro h
  86  have h00 := congrFun (congrFun h (0 : Fin 8)) (0 : Fin 8)
  87  simp [densityOf] at h00
  88
  89/-! ## Per-update density mediators -/
  90
  91/-- The density-level conjugation channel `rho ↦ U * rho * Uᴴ`. -/
  92def conjugationChannel
  93    (U : Matrix (Fin 8) (Fin 8) Complex)
  94    (rho : Matrix (Fin 8) (Fin 8) Complex) :
  95    Matrix (Fin 8) (Fin 8) Complex :=
  96  U * rho * U.conjTranspose
  97
  98/-- Conjugation by `U` reproduces the amplitude update on pure states.
  99No unitarity hypothesis is needed. -/
 100theorem conjugationChannel_reproduces
 101    (U : Matrix (Fin 8) (Fin 8) Complex) (psi : Signal8) :
 102    conjugationChannel U (densityOf psi) = densityOf (U.mulVec psi) := by
 103  ext i j
 104  simp only [conjugationChannel, densityOf, Matrix.mul_apply, Matrix.of_apply,
 105    Matrix.conjTranspose_apply, Matrix.mulVec, dotProduct, star_sum, star_mul,
 106    Finset.sum_mul, Finset.mul_sum]
 107  exact Finset.sum_congr rfl fun l _ => Finset.sum_congr rfl fun k _ => by ring
 108
 109/-- Conjugation by a unitary matrix is trace-preserving. -/
 110theorem conjugationChannel_trace_preserving
 111    (U : Matrix (Fin 8) (Fin 8) Complex)
 112    (hU : U.conjTranspose * U = 1)
 113    (rho : Matrix (Fin 8) (Fin 8) Complex) :
 114    (conjugationChannel U rho).trace = rho.trace := by
 115  unfold conjugationChannel
 116  rw [Matrix.trace_mul_cycle U rho U.conjTranspose]
 117  rw [hU, one_mul]
 118
 119/-- For every fixed update, an update-dependent density mediator exists. -/
 120theorem per_update_density_mediator_exists
 121    (U : Matrix (Fin 8) (Fin 8) Complex) :
 122    ∃ Phi :
 123        Matrix (Fin 8) (Fin 8) Complex →
 124          Matrix (Fin 8) (Fin 8) Complex,
 125      ∀ psi : Signal8, Phi (densityOf psi) = densityOf (U.mulVec psi) :=
 126  ⟨conjugationChannel U, conjugationChannel_reproduces U⟩
 127
 128/-! ## No universal density mediator -/
 129
 130private def basis0 : Signal8 :=
 131  Pi.single (0 : Fin 8) (1 : Complex)
 132
 133private def basis1 : Signal8 :=
 134  Pi.single (1 : Fin 8) (1 : Complex)
 135
 136private def swap01 : Equiv.Perm (Fin 8) :=
 137  Equiv.swap (0 : Fin 8) 1
 138
 139private def swapMatrix : Matrix (Fin 8) (Fin 8) Complex :=
 140  Matrix.swap Complex (0 : Fin 8) 1
 141
 142private theorem swapMatrix_unitary :
 143    swapMatrix.conjTranspose * swapMatrix = 1 := by
 144  simp [swapMatrix, Matrix.swap_mul_self]
 145
 146private theorem swapMatrix_mulVec_basis0 :
 147    swapMatrix.mulVec basis0 = basis1 := by
 148  calc
 149    swapMatrix.mulVec basis0 = basis0 ∘ swap01 := by
 150      simpa [swapMatrix, swap01] using
 151        Matrix.swap_mulVec (R := Complex) (i := (0 : Fin 8)) (j := 1) basis0
 152    _ = basis1 := by
 153      funext i
 154      show basis0 (swap01 i) = basis1 i
 155      fin_cases i <;>
 156        simp [basis0, basis1, swap01, Equiv.swap_apply_def, Pi.single_apply]
 157
 158private theorem densityOf_basis0_ne_densityOf_basis1 :
 159    densityOf basis0 ≠ densityOf basis1 := by
 160  intro h
 161  have h00 := congrFun (congrFun h (0 : Fin 8)) (0 : Fin 8)
 162  simp [basis0, basis1, densityOf] at h00
 163
 164/-- No single fixed density-level mediator serves all unitary updates. -/
 165theorem no_universal_density_mediator :
 166    ¬ ∃ Phi :
 167        Matrix (Fin 8) (Fin 8) Complex →
 168          Matrix (Fin 8) (Fin 8) Complex,
 169      ∀ U : Matrix (Fin 8) (Fin 8) Complex,
 170        U.conjTranspose * U = 1 →
 171          ∀ psi : Signal8,
 172            Phi (densityOf psi) = densityOf (U.mulVec psi) := by
 173  rintro ⟨Phi, hPhi⟩
 174  have hId :
 175      Phi (densityOf basis0) = densityOf basis0 := by
 176    have h := hPhi (1 : Matrix (Fin 8) (Fin 8) Complex)
 177      (by rw [Matrix.conjTranspose_one, one_mul]) basis0
 178    rwa [Matrix.one_mulVec] at h
 179  have hSwap :
 180      Phi (densityOf basis0) = densityOf basis1 := by
 181    have h := hPhi swapMatrix swapMatrix_unitary basis0
 182    rwa [swapMatrix_mulVec_basis0] at h
 183  exact densityOf_basis0_ne_densityOf_basis1 (hId.symm.trans hSwap)
 184
 185/-! ## Boundary package -/
 186
 187/-- The exact mediator-universality boundary: every fixed update has a
 188density-level mediator, but no one mediator works for all unitary updates. -/
 189theorem mediator_universality_boundary :
 190    (∀ U : Matrix (Fin 8) (Fin 8) Complex,
 191      ∃ Phi :
 192          Matrix (Fin 8) (Fin 8) Complex →
 193            Matrix (Fin 8) (Fin 8) Complex,
 194        ∀ psi : Signal8, Phi (densityOf psi) = densityOf (U.mulVec psi)) ∧
 195    (¬ ∃ Phi :
 196        Matrix (Fin 8) (Fin 8) Complex →
 197          Matrix (Fin 8) (Fin 8) Complex,
 198      ∀ U : Matrix (Fin 8) (Fin 8) Complex,
 199        U.conjTranspose * U = 1 →
 200          ∀ psi : Signal8,
 201            Phi (densityOf psi) = densityOf (U.mulVec psi)) :=
 202  ⟨fun U => per_update_density_mediator_exists U,
 203    no_universal_density_mediator⟩
 204
 205end
 206
 207end MediatorUniversalityBoundary
 208end QuantumChannel
 209end Gravity
 210end IndisputableMonolith
 211
 212#print axioms IndisputableMonolith.Gravity.QuantumChannel.MediatorUniversalityBoundary.conjugationChannel_reproduces
 213#print axioms IndisputableMonolith.Gravity.QuantumChannel.MediatorUniversalityBoundary.no_universal_density_mediator
 214#print axioms IndisputableMonolith.Gravity.QuantumChannel.MediatorUniversalityBoundary.mediator_universality_boundary
 215