IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForcedSectionReadout

   1import Mathlib
   2import IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForcedSubstrate
   3
   4/-!
   5# Gravity Track 2.C: Section-Readout Forcing without Pure-Tensor Factorization
   6
   7## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   8
   9## What this module closes
  10
  11This module is the first direct attack on the remaining Track 2.C gap:
  12retiring the full pure-tensor factorization hypothesis. Earlier modules
  13proved:
  14
  15* `AmplitudeLinearForcedJoint`: if a joint operator factorizes on pure
  16  tensors, then the channel factor is forced amplitude-linear.
  17* `AmplitudeLinearForcedSubstrate`: plugging in the recognition update on
  18  the matter side gives the substrate-side forcing result.
  19* `AmplitudeLinearForcedCert`: bundles this as a STRUCTURAL THEOREM under
  20  the named `FactorizableJointSubstrate` hypothesis.
  21
  22The factor-product hypothesis is stronger than operationally necessary.
  23To force the channel response `R_C` to be amplitude-linear, we do **not**
  24need the joint operator `R_J : Signal8 ⊗ Signal8 →ₗ Signal8 ⊗ Signal8`
  25to factorize on every pure tensor. It is enough that the physical channel
  26response is obtained by a **nonzero matter section readout**:
  27
  28```
  29φ ↦ χ⁻¹ • extractSecond i₀ (R_J (ψ₀ ⊗ φ))
  30```
  31
  32for some fixed matter reference `ψ₀`, coordinate `i₀`, and nonzero scalar
  33`χ`. This is a linear slice of the joint operator, hence the channel response
  34is automatically amplitude-linear. The joint operator may still mix matter
  35and channel sectors away from that readout section.
  36
  37## Main result
  38
  39* `isAmplitudeLinear_channel_of_sectionReadout`:
  40  any channel response recovered as a nonzero section readout of a `ℂ`-linear
  41  joint operator is amplitude-linear.
  42
  43* `channel_eq_zero_of_density_only_of_sectionReadout`:
  44  composing with the single-factor dichotomy, any density-only response under
  45  such a readout collapses to zero.
  46
  47* `not_exists_nontrivial_density_only_channel_with_sectionReadout`:
  48  no nontrivial density-only classical channel can arise from a nonzero
  49  section readout of a linear joint substrate.
  50
  51* `sectionReadout_of_pureTensorFactorization`:
  52  the old pure-tensor factorization hypothesis implies the new section-readout
  53  hypothesis whenever the matter side is nontrivial. Thus the new hypothesis is
  54  a genuine weakening of the previous proof interface.
  55
  56## Anti-retreat scope
  57
  58This does not prove that every physically admissible joint operator admits a
  59nonzero section readout. That is the remaining substrate-locality statement.
  60But it **does** retire the need for global pure-tensor factorization in the
  61amplitude-linearity theorem: factorization is sufficient, not necessary.
  62
  63The next upgrade is to derive `JointSectionReadout` from a substrate locality
  64or measurement-access principle rather than assume it as a structural readout
  65law.
  66
  67Zero `sorry`. Zero new RS-specific axioms.
  68-/
  69
  70namespace IndisputableMonolith
  71namespace Gravity
  72namespace QuantumChannel
  73namespace AmplitudeLinearForced
  74
  75open scoped TensorProduct
  76
  77/-! ## §1. Section-readout substrate principle -/
  78
  79/-- A channel response `R_C` is a **nonzero matter-section readout** of a
  80joint linear operator `R_J` when it is recovered by:
  81
  821. injecting a fixed matter reference state `ψ₀` into the first tensor factor,
  832. applying the joint operator,
  843. extracting the channel factor at coordinate `i₀`, and
  854. dividing by a nonzero scalar `χ`.
  86
  87This is strictly weaker than global pure-tensor factorization: it constrains
  88only the operational readout section `ψ₀ ⊗ φ`, not the action of `R_J` on all
  89pure tensors. -/
  90structure JointSectionReadout
  91    (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
  92    (R_C : Signal8 → Signal8) where
  93  ψ₀ : Signal8
  94  i₀ : Fin 8
  95  χ : ℂ
  96  χ_ne_zero : χ ≠ 0
  97  readout :
  98    ∀ φ : Signal8,
  99      R_C φ = χ⁻¹ • (extractSecond i₀) (R_J (insertFirst ψ₀ φ))
 100
 101/-! ## §2. Section readout forces amplitude-linearity -/
 102
 103/-- **Section-readout forcing.** If a channel response is recovered as a
 104nonzero section readout of a `ℂ`-linear joint operator, then it is
 105amplitude-linear. No pure-tensor factorization hypothesis is used. -/
 106theorem isAmplitudeLinear_channel_of_sectionReadout
 107    {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 108    {R_C : Signal8 → Signal8}
 109    (hReadout : JointSectionReadout R_J R_C) :
 110    IsAmplitudeLinear R_C := by
 111  refine ⟨hReadout.χ⁻¹ •
 112    ((extractSecond hReadout.i₀).comp (R_J.comp (insertFirst hReadout.ψ₀))), ?_⟩
 113  intro φ
 114  rw [LinearMap.smul_apply, LinearMap.comp_apply, LinearMap.comp_apply]
 115  exact hReadout.readout φ
 116
 117/-- **Density-only collapse under section readout.** A density-only channel
 118response recovered by a nonzero section readout of a linear joint operator is
 119identically zero. -/
 120theorem channel_eq_zero_of_density_only_of_sectionReadout
 121    {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 122    {R_C : Signal8 → Signal8}
 123    (hReadout : JointSectionReadout R_J R_C)
 124    (hDen : IsDensityOnly R_C) (φ : Signal8) :
 125    R_C φ = 0 :=
 126  eq_zero_of_isAmplitudeLinear_isDensityOnly
 127    (isAmplitudeLinear_channel_of_sectionReadout hReadout) hDen φ
 128
 129/-- **Existence-form no-go.** There is no nontrivial density-only channel
 130response that is obtained as a nonzero section readout of a linear joint
 131operator. -/
 132theorem not_exists_nontrivial_density_only_channel_with_sectionReadout :
 133    ¬ ∃ (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
 134        (R_C : Signal8 → Signal8),
 135      (∃ _hReadout : JointSectionReadout R_J R_C,
 136        IsDensityOnly R_C ∧
 137        (∃ φ : Signal8, R_C φ ≠ 0)) := by
 138  rintro ⟨R_J, R_C, hReadout, hDen, φ, hφ⟩
 139  exact hφ (channel_eq_zero_of_density_only_of_sectionReadout hReadout hDen φ)
 140
 141/-! ## §3. Old factorization implies new section-readout principle -/
 142
 143/-- The previous pure-tensor factorization hypothesis implies the new
 144section-readout hypothesis whenever the matter response is nontrivial at some
 145coordinate. This proves that the section-readout theorem strictly generalizes
 146the old proof interface: global factorization is sufficient for readout, but
 147the section-readout theorem itself does not assume it. -/
 148def sectionReadout_of_pureTensorFactorization
 149    {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 150    {R_M R_C : Signal8 → Signal8}
 151    (hFact : PureTensorFactorization R_J R_M R_C)
 152    {ψ₀ : Signal8} {i₀ : Fin 8} (hχ : (R_M ψ₀) i₀ ≠ 0) :
 153    JointSectionReadout R_J R_C where
 154  ψ₀ := ψ₀
 155  i₀ := i₀
 156  χ := (R_M ψ₀) i₀
 157  χ_ne_zero := hχ
 158  readout := by
 159    intro φ
 160    rw [insertFirst_apply, hFact, extractSecond_tmul, smul_smul,
 161      inv_mul_cancel₀ hχ, one_smul]
 162
 163/-- The section-readout theorem recovers the old pure-tensor forcing theorem
 164as a corollary. -/
 165theorem isAmplitudeLinear_channel_of_pureTensorFactorization_via_sectionReadout
 166    {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 167    {R_M R_C : Signal8 → Signal8}
 168    (hFact : PureTensorFactorization R_J R_M R_C)
 169    {ψ₀ : Signal8} {i₀ : Fin 8} (hχ : (R_M ψ₀) i₀ ≠ 0) :
 170    IsAmplitudeLinear R_C :=
 171  isAmplitudeLinear_channel_of_sectionReadout
 172    (sectionReadout_of_pureTensorFactorization hFact hχ)
 173
 174/-! ## §4. Recognition-update specialization -/
 175
 176/-- Recognition-update section readout: the matter section is taken to be the
 177actual substrate recognition update `cyclic_shift`. This is the weaker
 178replacement for the old global factor-product assumption in Track 2.C. -/
 179structure RecognitionSectionReadout
 180    (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
 181    (R_C : Signal8 → Signal8) where
 182  ψ₀ : Signal8
 183  i₀ : Fin 8
 184  nontrivial_matter : (recognitionUpdate ψ₀) i₀ ≠ 0
 185  readout :
 186    ∀ φ : Signal8,
 187      R_C φ =
 188        ((recognitionUpdate ψ₀) i₀)⁻¹ •
 189          (extractSecond i₀) (R_J (insertFirst ψ₀ φ))
 190
 191/-- A recognition-section readout is a section readout. -/
 192def RecognitionSectionReadout.toJointSectionReadout
 193    {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 194    {R_C : Signal8 → Signal8}
 195    (hReadout : RecognitionSectionReadout R_J R_C) :
 196    JointSectionReadout R_J R_C where
 197  ψ₀ := hReadout.ψ₀
 198  i₀ := hReadout.i₀
 199  χ := (recognitionUpdate hReadout.ψ₀) hReadout.i₀
 200  χ_ne_zero := hReadout.nontrivial_matter
 201  readout := hReadout.readout
 202
 203/-- **Recognition-section forcing.** Under the substrate recognition update,
 204any channel response obtained by a nonzero section readout is amplitude-linear,
 205with no global pure-tensor factorization assumption. -/
 206theorem isAmplitudeLinear_channel_of_recognitionSectionReadout
 207    {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 208    {R_C : Signal8 → Signal8}
 209    (hReadout : RecognitionSectionReadout R_J R_C) :
 210    IsAmplitudeLinear R_C :=
 211  isAmplitudeLinear_channel_of_sectionReadout hReadout.toJointSectionReadout
 212
 213/-- Density-only collapse under recognition-section readout. -/
 214theorem channel_eq_zero_of_density_only_of_recognitionSectionReadout
 215    {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 216    {R_C : Signal8 → Signal8}
 217    (hReadout : RecognitionSectionReadout R_J R_C)
 218    (hDen : IsDensityOnly R_C) (φ : Signal8) :
 219    R_C φ = 0 :=
 220  channel_eq_zero_of_density_only_of_sectionReadout
 221    hReadout.toJointSectionReadout hDen φ
 222
 223/-- No nontrivial density-only channel can be recovered from a recognition
 224section readout of a linear joint substrate. -/
 225theorem not_exists_nontrivial_density_only_channel_with_recognitionSectionReadout :
 226    ¬ ∃ (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
 227        (R_C : Signal8 → Signal8),
 228      (∃ _hReadout : RecognitionSectionReadout R_J R_C,
 229        IsDensityOnly R_C ∧
 230        (∃ φ : Signal8, R_C φ ≠ 0)) := by
 231  rintro ⟨R_J, R_C, hReadout, hDen, φ, hφ⟩
 232  exact hφ
 233    (channel_eq_zero_of_density_only_of_recognitionSectionReadout hReadout hDen φ)
 234
 235/-! ## §5. Master cert -/
 236
 237/-- Master cert for the section-readout retirement of global pure-tensor
 238factorization. -/
 239structure SectionReadoutForcingCert where
 240  section_forces_amplitude_linear :
 241    ∀ {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 242      {R_C : Signal8 → Signal8},
 243      JointSectionReadout R_J R_C → IsAmplitudeLinear R_C
 244  section_density_only_collapse :
 245    ∀ {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 246      {R_C : Signal8 → Signal8},
 247      JointSectionReadout R_J R_C → IsDensityOnly R_C → ∀ φ, R_C φ = 0
 248  no_nontrivial_density_only_section :
 249    ¬ ∃ (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
 250        (R_C : Signal8 → Signal8),
 251      (∃ _hReadout : JointSectionReadout R_J R_C,
 252        IsDensityOnly R_C ∧ (∃ φ : Signal8, R_C φ ≠ 0))
 253  factorization_implies_section :
 254    ∀ {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 255      {R_M R_C : Signal8 → Signal8},
 256      PureTensorFactorization R_J R_M R_C →
 257        ∀ {ψ₀ : Signal8} {i₀ : Fin 8}, (R_M ψ₀) i₀ ≠ 0 →
 258          JointSectionReadout R_J R_C
 259
 260noncomputable def sectionReadoutForcingCert : SectionReadoutForcingCert where
 261  section_forces_amplitude_linear := fun h => isAmplitudeLinear_channel_of_sectionReadout h
 262  section_density_only_collapse := fun h hDen φ =>
 263    channel_eq_zero_of_density_only_of_sectionReadout h hDen φ
 264  no_nontrivial_density_only_section :=
 265    not_exists_nontrivial_density_only_channel_with_sectionReadout
 266  factorization_implies_section := by
 267    intro R_J R_M R_C hFact ψ₀ i₀ hχ
 268    exact sectionReadout_of_pureTensorFactorization
 269      (R_J := R_J) (R_M := R_M) (R_C := R_C)
 270      hFact (ψ₀ := ψ₀) (i₀ := i₀) hχ
 271
 272theorem sectionReadoutForcingCert_inhabited : Nonempty SectionReadoutForcingCert :=
 273  ⟨sectionReadoutForcingCert⟩
 274
 275/-- **TRACK 2.C ONE-SHOT THEOREM (section-readout form).** Global pure-tensor
 276factorization is not needed to force channel amplitude-linearity. It suffices
 277that the physical channel response is recovered as a nonzero matter-section
 278readout of the joint linear substrate. Under that weaker readout principle,
 279the channel is amplitude-linear and any density-only response collapses to
 280zero. The previous factorization theorem is recovered as a corollary because
 281factorization implies section readout. -/
 282theorem factor_product_retirement_one_statement :
 283    (∀ {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 284      {R_C : Signal8 → Signal8},
 285      JointSectionReadout R_J R_C → IsAmplitudeLinear R_C) ∧
 286    (∀ {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 287      {R_C : Signal8 → Signal8},
 288      JointSectionReadout R_J R_C → IsDensityOnly R_C → ∀ φ, R_C φ = 0) ∧
 289    (¬ ∃ (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
 290        (R_C : Signal8 → Signal8),
 291      (∃ _hReadout : JointSectionReadout R_J R_C,
 292        IsDensityOnly R_C ∧ (∃ φ : Signal8, R_C φ ≠ 0))) :=
 293  ⟨fun h => isAmplitudeLinear_channel_of_sectionReadout h,
 294   fun h hDen φ => channel_eq_zero_of_density_only_of_sectionReadout h hDen φ,
 295   not_exists_nontrivial_density_only_channel_with_sectionReadout⟩
 296
 297end AmplitudeLinearForced
 298end QuantumChannel
 299end Gravity
 300end IndisputableMonolith
 301