IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForcedJoint

   1import Mathlib
   2import IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForced
   3
   4/-!
   5# Gravity Track 2.C: Joint-Substrate Lift of the Amplitude-Linear Forcing
   6
   7Session 85 (`AmplitudeLinearForced`) closed the **single-factor substrate
   8dichotomy** on `Signal8`: no nontrivial channel response is simultaneously
   9amplitude-linear and density-only.
  10
  11This module lifts that result to the **joint matter-plus-channel substrate**
  12modelled as the binary tensor product
  13`JointSubstrate := Signal8 ⊗[ℂ] Signal8`. The substantive theorems:
  14
  15* `isAmplitudeLinear_matter_of_pureTensorFactorization` — if a `ℂ`-linear
  16  joint operator `R_J` factorizes on pure tensors as
  17  `R_J(ψ ⊗ φ) = R_M(ψ) ⊗ R_C(φ)`, and the channel response is nontrivial
  18  in the sense that some coordinate `(R_C φ₀) i₀ ≠ 0`, then the matter-side
  19  response `R_M` is amplitude-linear.
  20
  21* `isAmplitudeLinear_channel_of_pureTensorFactorization` — symmetric, with
  22  the channel-side amplitude-linear under nontrivial matter coupling.
  23
  24* `isAmplitudeLinear_both_of_pureTensorFactorization` — composite: both
  25  factor responses are amplitude-linear under bilateral nontriviality.
  26
  27* `channel_eq_zero_of_density_only_of_pureTensorFactorization` — the
  28  **Track 2.C closure step** under the binary-tensor model. Composing the
  29  joint-substrate lift with the Session 85 single-factor dichotomy, no joint
  30  substrate with nontrivial matter coupling admits a nontrivial density-only
  31  channel response. Equivalently, on the joint substrate, a candidate
  32  channel-side CPTP-classical readout collapses to the zero response.
  33
  34The full Track 2.C closure of paper IV T2 (upgrade from `MODEL` to `THEOREM`)
  35requires combining this lift with
  36`Foundation.SchrodingerDerivation.schrodinger_linear` (the joint recognition
  37operator is `ℂ`-linear on the joint substrate by lifting the single-factor
  38Schrodinger linearity via `PiTensorProduct.map`), which is the next
  39subsessions of Track 2.C.
  40
  41Zero `sorry`. Zero new RS-specific axioms.
  42-/
  43
  44namespace IndisputableMonolith
  45namespace Gravity
  46namespace QuantumChannel
  47namespace AmplitudeLinearForced
  48
  49open scoped TensorProduct
  50
  51/-- The joint matter-plus-channel substrate as a binary tensor product over `ℂ`.
  52The first factor is the matter ledger, the second factor is the channel ledger;
  53both are copies of `Signal8`. -/
  54abbrev JointSubstrate : Type := Signal8 ⊗[ℂ] Signal8
  55
  56/-- **Pure-tensor factorization** of a joint operator. The joint operator
  57`R_J` acts on pure-tensor states as the factor-wise application of separate
  58matter and channel responses. This is the physical content of the joint
  59substrate being a tensor product of matter and channel ledgers. -/
  60def PureTensorFactorization
  61    (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
  62    (R_M R_C : Signal8 → Signal8) : Prop :=
  63  ∀ (ψ φ : Signal8), R_J (ψ ⊗ₜ[ℂ] φ) = (R_M ψ) ⊗ₜ[ℂ] (R_C φ)
  64
  65/-- Coordinate-evaluation linear functional on `Signal8 = Fin 8 → ℂ`. -/
  66def evalAt (i : Fin 8) : Signal8 →ₗ[ℂ] ℂ := LinearMap.proj i
  67
  68@[simp]
  69theorem evalAt_apply (i : Fin 8) (v : Signal8) : evalAt i v = v i := rfl
  70
  71/-- Insert a fixed channel state into the second factor of the joint
  72substrate, as a `ℂ`-linear map `Signal8 →ₗ[ℂ] JointSubstrate` taking
  73`ψ ↦ ψ ⊗ₜ[ℂ] φ`. -/
  74noncomputable def insertSecond (φ : Signal8) : Signal8 →ₗ[ℂ] JointSubstrate :=
  75  (TensorProduct.mk ℂ Signal8 Signal8).flip φ
  76
  77@[simp]
  78theorem insertSecond_apply (φ ψ : Signal8) :
  79    insertSecond φ ψ = ψ ⊗ₜ[ℂ] φ := rfl
  80
  81/-- Insert a fixed matter state into the first factor of the joint substrate,
  82as a `ℂ`-linear map `Signal8 →ₗ[ℂ] JointSubstrate` taking `φ ↦ ψ ⊗ₜ[ℂ] φ`. -/
  83noncomputable def insertFirst (ψ : Signal8) : Signal8 →ₗ[ℂ] JointSubstrate :=
  84  TensorProduct.mk ℂ Signal8 Signal8 ψ
  85
  86@[simp]
  87theorem insertFirst_apply (ψ φ : Signal8) :
  88    insertFirst ψ φ = ψ ⊗ₜ[ℂ] φ := rfl
  89
  90/-- Extract the first factor of a pure tensor, scaled by the coordinate-`i`
  91component of the second factor. Linear on the whole `JointSubstrate` by the
  92universal property of the tensor product. -/
  93noncomputable def extractFirst (i : Fin 8) : JointSubstrate →ₗ[ℂ] Signal8 :=
  94  (TensorProduct.rid ℂ Signal8).toLinearMap.comp
  95    (TensorProduct.map (LinearMap.id : Signal8 →ₗ[ℂ] Signal8) (evalAt i))
  96
  97@[simp]
  98theorem extractFirst_tmul (i : Fin 8) (ψ φ : Signal8) :
  99    extractFirst i (ψ ⊗ₜ[ℂ] φ) = (φ i) • ψ := by
 100  simp [extractFirst, TensorProduct.map_tmul, TensorProduct.rid_tmul]
 101
 102/-- Extract the second factor of a pure tensor, scaled by the coordinate-`i`
 103component of the first factor. -/
 104noncomputable def extractSecond (i : Fin 8) : JointSubstrate →ₗ[ℂ] Signal8 :=
 105  (TensorProduct.lid ℂ Signal8).toLinearMap.comp
 106    (TensorProduct.map (evalAt i) (LinearMap.id : Signal8 →ₗ[ℂ] Signal8))
 107
 108@[simp]
 109theorem extractSecond_tmul (i : Fin 8) (ψ φ : Signal8) :
 110    extractSecond i (ψ ⊗ₜ[ℂ] φ) = (ψ i) • φ := by
 111  simp [extractSecond, TensorProduct.map_tmul, TensorProduct.lid_tmul]
 112
 113/-- **Track 2.C forward direction (matter side).** If a `ℂ`-linear joint
 114operator `R_J` factorizes on pure tensors through factor-wise responses
 115`R_M, R_C`, and the channel response is nontrivial at some coordinate
 116`(R_C φ₀) i₀`, then the matter-side response `R_M` is amplitude-linear. -/
 117theorem isAmplitudeLinear_matter_of_pureTensorFactorization
 118    {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 119    {R_M R_C : Signal8 → Signal8}
 120    (hFact : PureTensorFactorization R_J R_M R_C)
 121    {φ₀ : Signal8} {i₀ : Fin 8} (hNontrivial : (R_C φ₀) i₀ ≠ 0) :
 122    IsAmplitudeLinear R_M := by
 123  refine ⟨((R_C φ₀) i₀)⁻¹ •
 124    ((extractFirst i₀).comp (R_J.comp (insertSecond φ₀))), ?_⟩
 125  intro ψ
 126  show R_M ψ = _
 127  rw [LinearMap.smul_apply, LinearMap.comp_apply, LinearMap.comp_apply,
 128      insertSecond_apply, hFact, extractFirst_tmul,
 129      smul_smul, inv_mul_cancel₀ hNontrivial, one_smul]
 130
 131/-- **Track 2.C forward direction (channel side).** If a `ℂ`-linear joint
 132operator `R_J` factorizes on pure tensors through factor-wise responses
 133`R_M, R_C`, and the matter response is nontrivial at some coordinate
 134`(R_M ψ₀) i₀`, then the channel-side response `R_C` is amplitude-linear. -/
 135theorem isAmplitudeLinear_channel_of_pureTensorFactorization
 136    {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 137    {R_M R_C : Signal8 → Signal8}
 138    (hFact : PureTensorFactorization R_J R_M R_C)
 139    {ψ₀ : Signal8} {i₀ : Fin 8} (hNontrivial : (R_M ψ₀) i₀ ≠ 0) :
 140    IsAmplitudeLinear R_C := by
 141  refine ⟨((R_M ψ₀) i₀)⁻¹ •
 142    ((extractSecond i₀).comp (R_J.comp (insertFirst ψ₀))), ?_⟩
 143  intro φ
 144  show R_C φ = _
 145  rw [LinearMap.smul_apply, LinearMap.comp_apply, LinearMap.comp_apply,
 146      insertFirst_apply, hFact, extractSecond_tmul,
 147      smul_smul, inv_mul_cancel₀ hNontrivial, one_smul]
 148
 149/-- **Composite forward direction.** Under joint `ℂ`-linearity, pure-tensor
 150factorization, and bilateral nontriviality, both factor responses are
 151amplitude-linear. -/
 152theorem isAmplitudeLinear_both_of_pureTensorFactorization
 153    {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 154    {R_M R_C : Signal8 → Signal8}
 155    (hFact : PureTensorFactorization R_J R_M R_C)
 156    {φ₀ : Signal8} {i_C : Fin 8} (hC : (R_C φ₀) i_C ≠ 0)
 157    {ψ₀ : Signal8} {i_M : Fin 8} (hM : (R_M ψ₀) i_M ≠ 0) :
 158    IsAmplitudeLinear R_M ∧ IsAmplitudeLinear R_C :=
 159  ⟨isAmplitudeLinear_matter_of_pureTensorFactorization hFact hC,
 160   isAmplitudeLinear_channel_of_pureTensorFactorization hFact hM⟩
 161
 162/-- **Track 2.C closure step (no density-only channel under nontrivial matter
 163coupling).** If `R_J` is `ℂ`-linear, factorizes on pure tensors through
 164`R_M, R_C`, the matter response is nontrivial, and the channel response is
 165density-only (the structural footprint of a CPTP-classical readout), then
 166the channel response is identically zero.
 167
 168This is the substantive Track 2.C dichotomy at the joint substrate level:
 169no joint substrate with nontrivial matter coupling admits a nontrivial
 170density-only channel response. Composing the joint-substrate lift
 171(`isAmplitudeLinear_channel_of_pureTensorFactorization`) with the Session 85
 172single-factor dichotomy (`eq_zero_of_isAmplitudeLinear_isDensityOnly`). -/
 173theorem channel_eq_zero_of_density_only_of_pureTensorFactorization
 174    {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 175    {R_M R_C : Signal8 → Signal8}
 176    (hFact : PureTensorFactorization R_J R_M R_C)
 177    {ψ₀ : Signal8} {i₀ : Fin 8} (hM : (R_M ψ₀) i₀ ≠ 0)
 178    (hDen : IsDensityOnly R_C) (φ : Signal8) :
 179    R_C φ = 0 :=
 180  eq_zero_of_isAmplitudeLinear_isDensityOnly
 181    (isAmplitudeLinear_channel_of_pureTensorFactorization hFact hM) hDen φ
 182
 183/-- Symmetric closure: under nontrivial channel coupling, no density-only
 184matter response is admissible. -/
 185theorem matter_eq_zero_of_density_only_of_pureTensorFactorization
 186    {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 187    {R_M R_C : Signal8 → Signal8}
 188    (hFact : PureTensorFactorization R_J R_M R_C)
 189    {φ₀ : Signal8} {i₀ : Fin 8} (hC : (R_C φ₀) i₀ ≠ 0)
 190    (hDen : IsDensityOnly R_M) (ψ : Signal8) :
 191    R_M ψ = 0 :=
 192  eq_zero_of_isAmplitudeLinear_isDensityOnly
 193    (isAmplitudeLinear_matter_of_pureTensorFactorization hFact hC) hDen ψ
 194
 195/-- **No-go (existence form).** On the joint substrate, there is no candidate
 196joint recognition operator that factorizes through nontrivial matter coupling
 197*and* a nontrivial density-only channel response. The hypotheses cannot be
 198simultaneously satisfied. -/
 199theorem not_exists_pureTensorFactorization_nontrivial_matter_density_only_channel :
 200    ¬ ∃ (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
 201        (R_M R_C : Signal8 → Signal8),
 202      PureTensorFactorization R_J R_M R_C ∧
 203        (∃ ψ₀ : Signal8, ∃ i₀ : Fin 8, (R_M ψ₀) i₀ ≠ 0) ∧
 204        IsDensityOnly R_C ∧
 205        (∃ φ : Signal8, R_C φ ≠ 0) := by
 206  rintro ⟨R_J, R_M, R_C, hFact, ⟨ψ₀, i₀, hM⟩, hDen, φ, hCφ⟩
 207  exact hCφ (channel_eq_zero_of_density_only_of_pureTensorFactorization
 208    hFact hM hDen φ)
 209
 210end AmplitudeLinearForced
 211end QuantumChannel
 212end Gravity
 213end IndisputableMonolith
 214