IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForced

   1import Mathlib
   2import IndisputableMonolith.Foundation.ComplexStructureForcing
   3
   4/-!
   5# Gravity Track 2.C: Amplitude-Linear Forced (substrate dichotomy)
   6
   7Track 2.C of the quantum-gravity master plan is the deepest physics step of
   8Track 2: the amplitude-linear gravitational channel must be *forced* from
   9substrate linearity, not chosen as a modeling assumption. This is the upgrade
  10of paper IV's T2 from `MODEL` to `THEOREM`.
  11
  12This module opens Track 2.C with the **substrate dichotomy on a single
  13channel factor**. On the canonical `Foundation.ComplexStructureForcing.Signal8`
  14state space, a candidate channel response `R : Signal8 → Signal8` cannot be
  15simultaneously
  16
  17* `IsAmplitudeLinear` (it agrees with some `ℂ`-linear map), and
  18* `IsDensityOnly` (it is invariant under multiplication by unit-modulus
  19  complex scalars, i.e. it depends only on the density matrix `|ψ�⟩⟨ψ|`)
  20
  21unless it is identically zero on `Signal8`. The contrapositive form
  22`not_isDensityOnly_of_isAmplitudeLinear_of_ne_zero` is the first Lean
  23substrate-forcing statement of Track 2.C: a nontrivial amplitude-linear
  24channel response does *not* factor through a density-only readout.
  25
  26Subsequent Track 2.C work will lift this single-factor dichotomy to the
  27joint matter-plus-channel `MacroscopicLedger` substrate to force
  28amplitude-linearity of the gravitational channel from the joint linearity
  29of the recognition operator (`Foundation.SchrodingerDerivation.schrodinger_linear`
  30composed factor-wise via `Gravity.MacroscopicLedger.MacroscopicShift`).
  31
  32Zero `sorry`. Zero new RS-specific axioms.
  33-/
  34
  35namespace IndisputableMonolith
  36namespace Gravity
  37namespace QuantumChannel
  38namespace AmplitudeLinearForced
  39
  40/-- Local abbreviation for the eight-tick analytic signal carrier
  41`Fin 8 → ℂ`, identified with the canonical
  42`Foundation.ComplexStructureForcing.Signal8`. -/
  43abbrev Signal8 : Type :=
  44  IndisputableMonolith.Foundation.ComplexStructureForcing.Signal8
  45
  46/-- A candidate gravitational-channel response on `Signal8` is
  47**amplitude-linear** when it agrees with some `ℂ`-linear map.
  48Amplitude-linear responses preserve coherent superpositions of ledger
  49states. -/
  50def IsAmplitudeLinear (R : Signal8 → Signal8) : Prop :=
  51  ∃ L : Signal8 →ₗ[ℂ] Signal8, ∀ ψ : Signal8, R ψ = L ψ
  52
  53/-- A candidate response is **phase-equivariant** when it commutes with
  54arbitrary complex scaling. Amplitude-linear responses are phase-equivariant. -/
  55def IsPhaseEquivariant (R : Signal8 → Signal8) : Prop :=
  56  ∀ (c : ℂ) (ψ : Signal8), R (c • ψ) = c • R ψ
  57
  58/-- A candidate response is **density-only** when it is invariant under
  59multiplication by unit-modulus complex scalars. This is the structural
  60footprint of a CPTP-classical readout: the density matrix `|ψ⟩⟨ψ|` is
  61invariant under `ψ ↦ c · ψ` whenever `‖c‖ = 1`, so any response computed from
  62the density matrix alone must agree on `c • ψ` and `ψ`. -/
  63def IsDensityOnly (R : Signal8 → Signal8) : Prop :=
  64  ∀ (c : ℂ), ‖c‖ = 1 → ∀ ψ : Signal8, R (c • ψ) = R ψ
  65
  66/-- Amplitude-linear responses are phase-equivariant. -/
  67theorem isPhaseEquivariant_of_isAmplitudeLinear
  68    {R : Signal8 → Signal8} (h : IsAmplitudeLinear R) :
  69    IsPhaseEquivariant R := by
  70  rcases h with ⟨L, hL⟩
  71  intro c ψ
  72  rw [hL (c • ψ), hL ψ, L.map_smul]
  73
  74/-- **Substrate dichotomy on a single channel factor.** If a candidate
  75gravitational-channel response is simultaneously amplitude-linear and
  76density-only, then it is identically zero on `Signal8`. The proof tests the
  77two structural conditions against each other at the unit-modulus scalar
  78`c = -1`. -/
  79theorem eq_zero_of_isAmplitudeLinear_isDensityOnly
  80    {R : Signal8 → Signal8}
  81    (hLin : IsAmplitudeLinear R) (hDen : IsDensityOnly R)
  82    (ψ : Signal8) : R ψ = 0 := by
  83  have hPhase : IsPhaseEquivariant R :=
  84    isPhaseEquivariant_of_isAmplitudeLinear hLin
  85  have hcnorm : ‖((-1 : ℂ))‖ = 1 := by
  86    rw [norm_neg, norm_one]
  87  -- Amplitude-linear / phase-equivariant: `R(-ψ) = (-1) • R ψ`.
  88  have hAmp : R ((-1 : ℂ) • ψ) = (-1 : ℂ) • R ψ := hPhase (-1) ψ
  89  -- Density-only: `R(-ψ) = R(ψ)` since `‖-1‖ = 1`.
  90  have hDen' : R ((-1 : ℂ) • ψ) = R ψ := hDen (-1) hcnorm ψ
  91  -- Combine: `R ψ = - R ψ`.
  92  have hEq : R ψ = - R ψ := by
  93    have h := hDen'.symm.trans hAmp
  94    rwa [neg_one_smul] at h
  95  -- Hence `2 • R ψ = 0` in the `ℂ`-module `Signal8`.
  96  have h2 : (2 : ℂ) • R ψ = 0 := by
  97    rw [two_smul]
  98    nth_rewrite 1 [hEq]
  99    exact neg_add_cancel _
 100  -- `(2 : ℂ) ≠ 0`, and `Signal8 = Fin 8 → ℂ` is a `NoZeroSMulDivisors ℂ`
 101  -- module, so `R ψ = 0`.
 102  have h2ne : (2 : ℂ) ≠ 0 := by norm_num
 103  rcases smul_eq_zero.mp h2 with h | h
 104  · exact absurd h h2ne
 105  · exact h
 106
 107/-- **Contrapositive substrate-forcing statement (Track 2.C seed).** A
 108nontrivial amplitude-linear channel response on `Signal8` is *not*
 109density-only. Equivalently: on a single channel factor, no nontrivial
 110gravitational-channel response can be simultaneously consistent with
 111substrate linearity (`Foundation.SchrodingerDerivation.schrodinger_linear`)
 112and with a CPTP-classical density-only readout. -/
 113theorem not_isDensityOnly_of_isAmplitudeLinear_of_ne_zero
 114    {R : Signal8 → Signal8}
 115    (hLin : IsAmplitudeLinear R)
 116    {ψ : Signal8} (hψ : R ψ ≠ 0) :
 117    ¬ IsDensityOnly R := by
 118  intro hDen
 119  exact hψ (eq_zero_of_isAmplitudeLinear_isDensityOnly hLin hDen ψ)
 120
 121/-- **No-go for amplitude-linear-and-density-only nontrivial responses.**
 122Existence form of the substrate dichotomy: there is no channel response on
 123`Signal8` that is simultaneously amplitude-linear, density-only, and
 124nontrivial (i.e. nonzero on some ledger state). -/
 125theorem not_exists_nontrivial_isAmplitudeLinear_and_isDensityOnly :
 126    ¬ ∃ (R : Signal8 → Signal8),
 127      IsAmplitudeLinear R ∧ IsDensityOnly R ∧ (∃ ψ : Signal8, R ψ ≠ 0) := by
 128  rintro ⟨R, hLin, hDen, ψ, hψ⟩
 129  exact hψ (eq_zero_of_isAmplitudeLinear_isDensityOnly hLin hDen ψ)
 130
 131end AmplitudeLinearForced
 132end QuantumChannel
 133end Gravity
 134end IndisputableMonolith
 135