IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForcedSubstrate

   1import Mathlib
   2import IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForcedJoint
   3import IndisputableMonolith.Gravity.MacroscopicLedger
   4
   5/-!
   6# Gravity Track 2.C: Substrate-Side Closure
   7
   8Sessions 85 (`AmplitudeLinearForced`) and 86 (`AmplitudeLinearForcedJoint`)
   9established:
  10
  11* the single-factor substrate dichotomy `IsAmplitudeLinear ∧ IsDensityOnly → 0`
  12  (Session 85), and
  13
  14* the joint-substrate lift `R_J ℂ-linear ∧ PureTensorFactorization R_J R_M R_C ∧
  15  (R_M nontrivial) → IsAmplitudeLinear R_C` (Session 86).
  16
  17Both prior sessions were modulo the assumption that the joint operator
  18factorizes on pure tensors through factor-wise responses. This session
  19substantiates Track 2.C by plugging in the actual substrate dynamics
  20`cyclic_shift` (the unique `ℂ`-linear single-tick recognition update on
  21`Signal8` from `Foundation.SchrodingerDerivation`, packaged as
  22`Gravity.MacroscopicLedger.cyclicShiftLinear`) on the matter side.
  23
  24Substantive theorems:
  25
  26* `recognitionUpdate_nontrivial` — the substrate recognition update is
  27  nontrivial: `(cyclic_shift 1) 0 = 1 ≠ 0`. Hence the Session 86 lift's
  28  nontriviality hypothesis is satisfied by substrate-default matter dynamics.
  29
  30* `isAmplitudeLinear_channel_of_recognitionUpdate` — under the substrate
  31  recognition update on the matter side, any candidate channel response
  32  participating in a `ℂ`-linear joint operator via pure-tensor factorization
  33  is forced to be amplitude-linear. This is the **Track 2.C substrate-side
  34  forcing** restricted to the binary-tensor model.
  35
  36* `channel_eq_zero_of_density_only_of_recognitionUpdate` — composing with
  37  Session 85's dichotomy: a density-only channel response under substrate
  38  matter dynamics is identically zero.
  39
  40* `not_exists_density_only_channel_with_recognitionUpdate` — no-go theorem
  41  (existence form): no joint recognition operator on the binary tensor
  42  substrate factorizes through cyclic-shift matter dynamics and a
  43  nontrivial density-only channel response simultaneously.
  44
  45* `canonicalCyclicJointOperator` — concrete witness that the hypothesis
  46  space of the forcing theorem is nonempty: `TensorProduct.map cyclicShiftLinear
  47  cyclicShiftLinear` factorizes through the recognition update on both sides.
  48
  49The remaining gap in the master-plan §4 Track 2.C step 5 ("in any joint
  50extension that preserves `schrodinger_linear`, `R_channel` must be
  51amplitude-linear") is that the pure-tensor factorization hypothesis is
  52*assumed*, not *derived* from substrate Schrodinger linearity alone. A general
  53`ℂ`-linear endomorphism of `Signal8 ⊗[ℂ] Signal8` need not be of the form
  54`f ⊗ g`; the tensor-product structure of the joint substrate plus the matter
  55side being constrained to `cyclic_shift` is the additional physical input
  56needed. Subsequent sessions will address this last step (either by
  57restricting to operators that factorize, or by deriving factorization from
  58stricter substrate axioms).
  59
  60Zero `sorry`. Zero new RS-specific axioms.
  61-/
  62
  63namespace IndisputableMonolith
  64namespace Gravity
  65namespace QuantumChannel
  66namespace AmplitudeLinearForced
  67
  68open scoped TensorProduct
  69
  70/-- The substrate recognition update on a single `Signal8` factor:
  71`Foundation.SchrodingerDerivation.cyclic_shift` (an `abbrev` for
  72`Spectral.cyclic_shift`), expressed as a function `Signal8 → Signal8`. -/
  73abbrev recognitionUpdate : Signal8 → Signal8 :=
  74  IndisputableMonolith.Spectral.cyclic_shift
  75
  76/-- The substrate recognition update is amplitude-linear, witnessed by
  77`Gravity.MacroscopicLedger.cyclicShiftLinear`. This packages the
  78`schrodinger_linear` content for the single-factor side. -/
  79theorem isAmplitudeLinear_recognitionUpdate :
  80    IsAmplitudeLinear recognitionUpdate :=
  81  ⟨IndisputableMonolith.Gravity.MacroscopicLedger.cyclicShiftLinear,
  82   fun _ => rfl⟩
  83
  84/-- The substrate recognition update is nontrivial. Concrete witness: the
  85constant-1 signal maps to itself under the cyclic shift, so
  86`(recognitionUpdate 1) 0 = 1 ≠ 0`. -/
  87theorem recognitionUpdate_nontrivial :
  88    ∃ (ψ₀ : Signal8) (i₀ : Fin 8), (recognitionUpdate ψ₀) i₀ ≠ 0 := by
  89  refine ⟨(1 : Signal8), 0, ?_⟩
  90  -- `recognitionUpdate 1 0` unfolds to `(1 : Signal8) ⟨(0+1)%8, _⟩ = 1 ⟨1, _⟩ = 1`.
  91  show (1 : Signal8) ⟨1, by decide⟩ ≠ (0 : ℂ)
  92  exact one_ne_zero
  93
  94/-- **Track 2.C substrate-side forcing.** If a `ℂ`-linear joint operator
  95factorizes on pure tensors with the substrate recognition update on the
  96matter side, then the channel response is necessarily amplitude-linear.
  97This is the substantive forcing step: substrate dynamics on the matter
  98factor inherits amplitude-linearity to the channel factor via the joint
  99linearity of `R_J`. -/
 100theorem isAmplitudeLinear_channel_of_recognitionUpdate
 101    {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 102    {R_C : Signal8 → Signal8}
 103    (hFact : PureTensorFactorization R_J recognitionUpdate R_C) :
 104    IsAmplitudeLinear R_C := by
 105  obtain ⟨ψ₀, i₀, hNontrivial⟩ := recognitionUpdate_nontrivial
 106  exact isAmplitudeLinear_channel_of_pureTensorFactorization
 107    (R_M := recognitionUpdate) (R_C := R_C) hFact hNontrivial
 108
 109/-- **Track 2.C closure step under substrate dynamics.** Under the substrate
 110recognition update on the matter side, no density-only channel response is
 111admissible: any such response is identically zero. Composes the joint-substrate
 112lift with Session 85's single-factor dichotomy, and substantiates the lift's
 113nontriviality hypothesis with the actual cyclic-shift recognition update.
 114
 115This is the binary-tensor-model upgrade of paper IV's T2 from MODEL to
 116THEOREM, modulo the pure-tensor factorization assumption that the joint
 117operator is of product form. The remaining MODEL tag concerns precisely
 118that factorization: a general `ℂ`-linear endomorphism of `Signal8 ⊗[ℂ]
 119Signal8` need not factorize; deriving the factorization from substrate
 120axioms alone is the next subsession. -/
 121theorem channel_eq_zero_of_density_only_of_recognitionUpdate
 122    {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 123    {R_C : Signal8 → Signal8}
 124    (hFact : PureTensorFactorization R_J recognitionUpdate R_C)
 125    (hDen : IsDensityOnly R_C) (φ : Signal8) :
 126    R_C φ = 0 :=
 127  eq_zero_of_isAmplitudeLinear_isDensityOnly
 128    (isAmplitudeLinear_channel_of_recognitionUpdate hFact) hDen φ
 129
 130/-- **No-go theorem (existence form).** No joint recognition operator on
 131`JointSubstrate` factorizes through cyclic-shift matter dynamics and a
 132nontrivial density-only channel response. -/
 133theorem not_exists_density_only_channel_with_recognitionUpdate :
 134    ¬ ∃ (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
 135        (R_C : Signal8 → Signal8),
 136      PureTensorFactorization R_J recognitionUpdate R_C ∧
 137        IsDensityOnly R_C ∧
 138        (∃ φ : Signal8, R_C φ ≠ 0) := by
 139  rintro ⟨R_J, R_C, hFact, hDen, φ, hCφ⟩
 140  exact hCφ
 141    (channel_eq_zero_of_density_only_of_recognitionUpdate hFact hDen φ)
 142
 143/-- **Canonical joint operator from substrate dynamics.** Concrete witness
 144that the hypothesis space of the forcing theorem is nonempty:
 145`TensorProduct.map cyclicShiftLinear cyclicShiftLinear` is a `ℂ`-linear
 146endomorphism of `JointSubstrate` that factorizes through `recognitionUpdate`
 147on both factors. -/
 148noncomputable def canonicalCyclicJointOperator :
 149    JointSubstrate →ₗ[ℂ] JointSubstrate :=
 150  TensorProduct.map
 151    IndisputableMonolith.Gravity.MacroscopicLedger.cyclicShiftLinear
 152    IndisputableMonolith.Gravity.MacroscopicLedger.cyclicShiftLinear
 153
 154/-- The canonical joint operator factorizes through the recognition update on
 155both factors. -/
 156theorem canonicalCyclicJointOperator_pureTensorFactorization :
 157    PureTensorFactorization canonicalCyclicJointOperator
 158      recognitionUpdate recognitionUpdate := by
 159  intro ψ φ
 160  show (TensorProduct.map _ _) (ψ ⊗ₜ[ℂ] φ) =
 161       (recognitionUpdate ψ) ⊗ₜ[ℂ] (recognitionUpdate φ)
 162  rw [TensorProduct.map_tmul]
 163  rfl
 164
 165end AmplitudeLinearForced
 166end QuantumChannel
 167end Gravity
 168end IndisputableMonolith
 169