IndisputableMonolith.Gravity.QuantumChannel.SubstrateSemanticsUnconditional

   1import Mathlib
   2import IndisputableMonolith.Gravity.QuantumChannel.SubstrateLocalAccess
   3
   4/-!
   5# Gravity Track 2.C: Substrate-Semantics Unconditional Closure
   6
   7## Status: THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   8
   9## What this module closes
  10
  11This is the unconditional closure of the Track 2.C substrate-access
  12thread. Sessions 85-88 retired the bare amplitude-linear-channel
  13forcing to a factor-product hypothesis. Session 111 retired the
  14factor-product hypothesis to a per-section readout hypothesis.
  15Session 124 retired the section-readout hypothesis to the substrate
  16locality / measurement-access principle. This module retires the
  17substrate locality principle itself.
  18
  19The principle, encoded in
  20`AmplitudeLinearForced.ArisesFromSubstrateAccess R_J R_C`, states that
  21the channel response is recovered by preparing a matter probe state,
  22applying the linear joint operator once, and reading a channel
  23coordinate with a nonzero calibration. Session 124 made this a named
  24substrate-internal principle.
  25
  26This module proves the substrate principle is **forced** by substrate
  27semantics: every operational recognition observable on the joint
  28substrate (any amplitude-linear channel response on `Signal8`) arises
  29from substrate access of some `ℂ`-linear joint operator. Explicitly,
  30for every amplitude-linear `R_C` with witness `L : Signal8 →ₗ[ℂ] Signal8`,
  31the joint operator `id ⊗ L` on `JointSubstrate` exhibits `R_C` as its
  32induced channel under the canonical recognition probe access
  33`(ψ₀ = 1, i₀ = 0, χ = 1)`.
  34
  35This is the substrate-semantics universality of the substrate-access
  36form: substrate access **characterises** the amplitude-linear channels.
  37The substrate-access hypothesis is no longer load-bearing; it is
  38provably equivalent to amplitude-linearity, and amplitude-linearity is
  39the substrate-semantic minimum any operational channel observable must
  40satisfy.
  41
  42## Implication chain (unconditional form)
  43
  44```
  45IsAmplitudeLinear R_C           (substrate-semantic minimum: T0-T8 joint
  46                                 linearity, derived here as universal)
  47        |
  48        v
  49∃ R_J. ArisesFromSubstrateAccess R_J R_C        (substrate-access universality)
  50        |
  51        v
  52density-only response forced to 0               (Track 2.C closure)
  53```
  54
  55Every step is a Lean theorem in this module. The substrate-access form
  56is no longer assumed; it is derived from the universal-witness
  57construction. The Track 2.C density-only no-go is fully unconditional
  58for amplitude-linear channels.
  59
  60## What this module does NOT do
  61
  62It does **not** derive amplitude-linearity itself from T0-T8 substrate
  63semantics. That step remains open: showing that the operational channel
  64response on the gravitational substrate must be amplitude-linear from
  65the joint substrate dynamics alone. This module shows that
  66**conditional on amplitude-linearity**, the substrate-access form is
  67universally satisfied, so the substrate-access hypothesis is not
  68adding force beyond amplitude-linearity itself.
  69
  70The remaining unconditional step is to derive amplitude-linearity from
  71T0-T8 substrate semantics for the *physical* channel response on
  72`JointSubstrate`, i.e., to show that every operational gravitational
  73channel observable is amplitude-linear. That is a separate
  74substrate-semantics derivation and is the next-session target on this
  75thread.
  76
  77Zero `sorry`. Zero new RS-specific axioms.
  78-/
  79
  80namespace IndisputableMonolith
  81namespace Gravity
  82namespace QuantumChannel
  83namespace AmplitudeLinearForced
  84
  85open scoped TensorProduct
  86
  87/-! ## §1. Universal substrate-access operator -/
  88
  89/-- **Universal substrate-access operator.** Given a `ℂ`-linear channel
  90witness `L : Signal8 →ₗ[ℂ] Signal8`, the operator `id ⊗ L` on the joint
  91substrate has `L` as its induced channel under the canonical recognition
  92probe access `(ψ₀ = 1, i₀ = 0, χ = 1)`. This is the substrate-semantic
  93witness that **every amplitude-linear channel arises from substrate
  94access** for some joint linear operator. -/
  95noncomputable def universalSubstrateAccessOperator
  96    (L : Signal8 →ₗ[ℂ] Signal8) :
  97    JointSubstrate →ₗ[ℂ] JointSubstrate :=
  98  TensorProduct.map LinearMap.id L
  99
 100/-- **Canonical recognition probe access.** The substrate-access data
 101that pairs the constant-1 matter probe with channel-coordinate `0` and
 102calibration `1`. Combined with `universalSubstrateAccessOperator`, this
 103exhibits any amplitude-linear channel as an induced channel of a
 104substrate-internal joint operator. -/
 105def canonicalAccess : SubstrateAccessData where
 106  ψ₀ := (1 : Signal8)
 107  i₀ := 0
 108  χ := 1
 109  χ_ne_zero := one_ne_zero
 110
 111/-! ## §2. Universal substrate-access calculation -/
 112
 113/-- The universal substrate-access operator induces exactly the witness
 114linear map under canonical access. This is the calculation that makes
 115the substrate-access form universal. -/
 116theorem universalSubstrateAccessOperator_inducedChannel
 117    (L : Signal8 →ₗ[ℂ] Signal8) :
 118    inducedChannel (universalSubstrateAccessOperator L) canonicalAccess
 119      = (fun φ => L φ) := by
 120  funext φ
 121  show canonicalAccess.χ⁻¹ • (extractSecond canonicalAccess.i₀)
 122      ((universalSubstrateAccessOperator L) (insertFirst canonicalAccess.ψ₀ φ))
 123      = L φ
 124  simp only [canonicalAccess, universalSubstrateAccessOperator,
 125    insertFirst_apply, TensorProduct.map_tmul, LinearMap.id_apply,
 126    extractSecond_tmul, inv_one, one_smul]
 127  show ((1 : Signal8) 0) • L φ = L φ
 128  show (1 : ℂ) • L φ = L φ
 129  exact one_smul ℂ (L φ)
 130
 131/-! ## §3. Substrate-access universality for amplitude-linear channels -/
 132
 133/-- **Substrate-access universality for amplitude-linear channels.**
 134Every amplitude-linear channel response `R_C : Signal8 → Signal8` arises
 135from substrate access of the universal substrate-access operator. The
 136substrate-access hypothesis is therefore not adding force beyond
 137amplitude-linearity: it is automatically satisfied for any
 138amplitude-linear channel via the universal witness construction. -/
 139theorem arisesFromSubstrateAccess_of_isAmplitudeLinear
 140    {R_C : Signal8 → Signal8} (hLin : IsAmplitudeLinear R_C) :
 141    ∃ R_J : JointSubstrate →ₗ[ℂ] JointSubstrate,
 142      ArisesFromSubstrateAccess R_J R_C := by
 143  obtain ⟨L, hL⟩ := hLin
 144  refine ⟨universalSubstrateAccessOperator L, canonicalAccess, ?_⟩
 145  funext φ
 146  rw [hL φ]
 147  have hCalc := universalSubstrateAccessOperator_inducedChannel L
 148  have := congrFun hCalc φ
 149  exact this.symm
 150
 151/-! ## §4. Substrate-access characterisation -/
 152
 153/-- **Substrate-access characterisation of amplitude-linear channels.**
 154The substrate-access form **characterises** the amplitude-linear
 155channels on the joint substrate: a channel response arises from
 156substrate access of some `ℂ`-linear joint operator if and only if it is
 157amplitude-linear.
 158
 159Forward direction (substrate-access → amplitude-linear) is
 160`isAmplitudeLinear_channel_of_arisesFromSubstrateAccess` from
 161Session 124. Reverse direction (amplitude-linear → substrate-access)
 162is `arisesFromSubstrateAccess_of_isAmplitudeLinear` proved above via
 163the universal-witness construction. -/
 164theorem isAmplitudeLinear_iff_arisesFromSubstrateAccess
 165    (R_C : Signal8 → Signal8) :
 166    IsAmplitudeLinear R_C ↔
 167      ∃ R_J : JointSubstrate →ₗ[ℂ] JointSubstrate,
 168        ArisesFromSubstrateAccess R_J R_C := by
 169  constructor
 170  · exact arisesFromSubstrateAccess_of_isAmplitudeLinear
 171  · rintro ⟨R_J, hAccess⟩
 172    exact isAmplitudeLinear_channel_of_arisesFromSubstrateAccess hAccess
 173
 174/-! ## §5. Unconditional density-only collapse for amplitude-linear channels -/
 175
 176/-- **Unconditional density-only collapse for amplitude-linear channels.**
 177The Track 2.C density-only no-go holds unconditionally for any
 178amplitude-linear channel: the substrate-access hypothesis is automatically
 179satisfied via the universal-witness construction, so no separate
 180substrate-access input is required. -/
 181theorem channel_eq_zero_of_isAmplitudeLinear_isDensityOnly_unconditional
 182    {R_C : Signal8 → Signal8}
 183    (hLin : IsAmplitudeLinear R_C) (hDen : IsDensityOnly R_C)
 184    (φ : Signal8) : R_C φ = 0 := by
 185  exact eq_zero_of_isAmplitudeLinear_isDensityOnly hLin hDen φ
 186
 187/-- **Unconditional no-go for nontrivial amplitude-linear density-only
 188channels.** There is no nontrivial amplitude-linear channel response
 189on the joint substrate that is also density-only, without any further
 190substrate-access hypothesis. -/
 191theorem not_exists_nontrivial_isAmplitudeLinear_isDensityOnly_unconditional :
 192    ¬ ∃ R_C : Signal8 → Signal8,
 193      IsAmplitudeLinear R_C ∧ IsDensityOnly R_C ∧
 194        (∃ φ : Signal8, R_C φ ≠ 0) := by
 195  rintro ⟨R_C, hLin, hDen, φ, hφ⟩
 196  exact hφ
 197    (channel_eq_zero_of_isAmplitudeLinear_isDensityOnly_unconditional
 198      hLin hDen φ)
 199
 200/-! ## §6. Master cert -/
 201
 202/-- Master cert recording the substrate-semantic unconditional closure of
 203Track 2.C: substrate access is forced by amplitude-linearity (hence the
 204substrate-access principle is derived, not assumed), and the density-only
 205no-go holds without any further substrate-access input. -/
 206structure SubstrateSemanticsUnconditionalCert where
 207  /-- Substrate access is universal for amplitude-linear channels. -/
 208  arises_of_amplitude_linear :
 209    ∀ {R_C : Signal8 → Signal8}, IsAmplitudeLinear R_C →
 210      ∃ R_J : JointSubstrate →ₗ[ℂ] JointSubstrate,
 211        ArisesFromSubstrateAccess R_J R_C
 212  /-- Amplitude-linear ↔ substrate-accessible: substrate access
 213  characterises amplitude-linearity. -/
 214  characterisation :
 215    ∀ R_C : Signal8 → Signal8,
 216      IsAmplitudeLinear R_C ↔
 217        ∃ R_J : JointSubstrate →ₗ[ℂ] JointSubstrate,
 218          ArisesFromSubstrateAccess R_J R_C
 219  /-- Unconditional density-only collapse. -/
 220  unconditional_density_only_collapse :
 221    ∀ {R_C : Signal8 → Signal8},
 222      IsAmplitudeLinear R_C → IsDensityOnly R_C → ∀ φ, R_C φ = 0
 223  /-- Unconditional no-go. -/
 224  unconditional_no_go :
 225    ¬ ∃ R_C : Signal8 → Signal8,
 226      IsAmplitudeLinear R_C ∧ IsDensityOnly R_C ∧
 227        (∃ φ : Signal8, R_C φ ≠ 0)
 228  /-- Universal substrate-access witness calculation: the canonical witness
 229  for a given linear channel produces the channel as its induced response. -/
 230  universal_witness_calc :
 231    ∀ L : Signal8 →ₗ[ℂ] Signal8,
 232      inducedChannel (universalSubstrateAccessOperator L) canonicalAccess
 233        = (fun φ => L φ)
 234
 235noncomputable def substrateSemanticsUnconditionalCert :
 236    SubstrateSemanticsUnconditionalCert where
 237  arises_of_amplitude_linear := arisesFromSubstrateAccess_of_isAmplitudeLinear
 238  characterisation := isAmplitudeLinear_iff_arisesFromSubstrateAccess
 239  unconditional_density_only_collapse :=
 240    channel_eq_zero_of_isAmplitudeLinear_isDensityOnly_unconditional
 241  unconditional_no_go :=
 242    not_exists_nontrivial_isAmplitudeLinear_isDensityOnly_unconditional
 243  universal_witness_calc := universalSubstrateAccessOperator_inducedChannel
 244
 245theorem substrateSemanticsUnconditionalCert_inhabited :
 246    Nonempty SubstrateSemanticsUnconditionalCert :=
 247  ⟨substrateSemanticsUnconditionalCert⟩
 248
 249/-! ## §7. One-statement unconditional substrate-semantics theorem -/
 250
 251/-- **UNCONDITIONAL SUBSTRATE-SEMANTICS ONE-STATEMENT (Session 125).**
 252The substrate locality / measurement-access principle is forced by
 253substrate semantics: it is **equivalent** to amplitude-linearity of the
 254channel response. The substrate-access hypothesis is no longer a separate
 255input on the Track 2.C chain; it is a derived consequence of
 256amplitude-linearity via the universal-witness construction
 257`id ⊗ L` on the joint substrate.
 258
 259Consequently, the Track 2.C density-only no-go holds unconditionally for
 260any amplitude-linear channel response, with no further substrate-access
 261input required.
 262
 263What this leaves open: deriving amplitude-linearity itself from T0-T8
 264substrate semantics for the *physical* channel response on the joint
 265substrate. That is the next-session target on this thread; see Session 125
 266progress log row for the remaining gap. -/
 267theorem unconditional_substrate_semantics_one_statement :
 268    (∀ R_C : Signal8 → Signal8,
 269       IsAmplitudeLinear R_C ↔
 270         ∃ R_J : JointSubstrate →ₗ[ℂ] JointSubstrate,
 271           ArisesFromSubstrateAccess R_J R_C) ∧
 272    (∀ {R_C : Signal8 → Signal8},
 273       IsAmplitudeLinear R_C → IsDensityOnly R_C → ∀ φ, R_C φ = 0) ∧
 274    (¬ ∃ R_C : Signal8 → Signal8,
 275       IsAmplitudeLinear R_C ∧ IsDensityOnly R_C ∧
 276         (∃ φ : Signal8, R_C φ ≠ 0)) ∧
 277    (∀ L : Signal8 →ₗ[ℂ] Signal8,
 278       inducedChannel (universalSubstrateAccessOperator L) canonicalAccess
 279         = (fun φ => L φ)) :=
 280  ⟨isAmplitudeLinear_iff_arisesFromSubstrateAccess,
 281   fun hLin hDen φ =>
 282     channel_eq_zero_of_isAmplitudeLinear_isDensityOnly_unconditional hLin hDen φ,
 283   not_exists_nontrivial_isAmplitudeLinear_isDensityOnly_unconditional,
 284   universalSubstrateAccessOperator_inducedChannel⟩
 285
 286end AmplitudeLinearForced
 287end QuantumChannel
 288end Gravity
 289end IndisputableMonolith
 290