IndisputableMonolith.Gravity.QuantumChannel.SubstrateLocalAccess

   1import Mathlib
   2import IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForcedSectionReadout
   3
   4/-!
   5# Gravity Track 2.C: Substrate Locality / Measurement-Access Principle
   6
   7## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   8
   9## What this module closes
  10
  11This is the next step beyond Session 111's section-readout retirement.
  12
  13Session 111 proved: if a channel response is a nonzero matter-section
  14readout of a linear joint operator, then it is forced amplitude-linear.
  15Pure-tensor factorization is sufficient but not necessary for this
  16readout law.
  17
  18The remaining assumption was that the *physical channel* is operationally
  19obtained by such a section readout. This module derives **that**
  20assumption from a sharper substrate-level principle: **substrate
  21locality / measurement-access**.
  22
  23The principle says: every operational channel observable on the joint
  24substrate `Signal8 ⊗ Signal8` is obtained as a recognition probe — fix a
  25matter reference state `ψ₀`, run the joint operator `R_J` once, and read
  26a channel coordinate `i₀`, normalised by a calibration scalar `χ ≠ 0`.
  27
  28Under this principle, the channel `R_C` is *defined* by the induced
  29formula
  30`R_C φ = χ⁻¹ • extractSecond i₀ (R_J (insertFirst ψ₀ φ))`,
  31which is automatically a `JointSectionReadout`. Section readout is no
  32longer an assumption; it is the **definition** of how the operational
  33channel is harvested from `R_J` under substrate locality.
  34
  35## The implication chain
  36
  37```
  38SubstrateAccessData R_J R_C            (Session 113 substrate principle)
  39                |
  40                v
  41JointSectionReadout R_J R_C            (Session 111 readout law)
  42                |
  43                v
  44IsAmplitudeLinear R_C                  (channel forced amplitude-linear)
  45                |
  46                v
  47density-only response forced to 0      (Track 2.C closure)
  48```
  49
  50Each arrow is a Lean theorem. The chain replaces the global factor-product
  51hypothesis with the **substrate measurement-access principle**, which is
  52sharper and substrate-internal.
  53
  54## Anti-retreat
  55
  56The substrate-access principle is **not** an RS-specific axiom. It is the
  57standard quantum-mechanical fact that physical observables on a
  58tensor-product Hilbert space are obtained by partial inner products
  59against fixed probe states, composed with the joint dynamics. This module
  60makes that explicit in the binary `Signal8` substrate.
  61
  62What this module does NOT do: derive the substrate-access principle from
  63T0-T8 alone. That is the next layer down — showing that any operational
  64recognition observable on the joint substrate must be of induced form.
  65This module makes the principle the named structural axiom and proves
  66that under it, the channel forcing chain closes without any reference to
  67factor-product, pure-tensor decomposition, or operator factorisation.
  68
  69Zero `sorry`. Zero new RS-specific axioms.
  70-/
  71
  72namespace IndisputableMonolith
  73namespace Gravity
  74namespace QuantumChannel
  75namespace AmplitudeLinearForced
  76
  77open scoped TensorProduct
  78
  79/-! ## §1. Substrate measurement-access data -/
  80
  81/-- **Substrate measurement-access data.** A matter probe state `ψ₀`,
  82a channel-side readout coordinate `i₀`, and a nonzero calibration
  83scalar `χ`. This is the data of one recognition-update measurement
  84probe on the joint substrate. -/
  85structure SubstrateAccessData where
  86  ψ₀ : Signal8
  87  i₀ : Fin 8
  88  χ : ℂ
  89  χ_ne_zero : χ ≠ 0
  90
  91/-- The channel induced by a substrate access on a joint linear
  92operator: prepare matter state `ψ₀` in the first factor, apply `R_J`,
  93extract the `i₀`-coordinate of the channel factor, normalise by `χ`.
  94This is the operational channel-readout recipe enforced by substrate
  95locality. -/
  96noncomputable def inducedChannel
  97    (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
  98    (access : SubstrateAccessData) : Signal8 → Signal8 :=
  99  fun φ =>
 100    access.χ⁻¹ • (extractSecond access.i₀) (R_J (insertFirst access.ψ₀ φ))
 101
 102@[simp]
 103theorem inducedChannel_apply
 104    (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
 105    (access : SubstrateAccessData) (φ : Signal8) :
 106    inducedChannel R_J access φ =
 107      access.χ⁻¹ • (extractSecond access.i₀) (R_J (insertFirst access.ψ₀ φ)) :=
 108  rfl
 109
 110/-! ## §2. Induced channel is automatically a section readout -/
 111
 112/-- The induced channel of any substrate access is a `JointSectionReadout`
 113of `R_J`. No additional hypothesis needed. -/
 114noncomputable def inducedChannel_isSectionReadout
 115    (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
 116    (access : SubstrateAccessData) :
 117    JointSectionReadout R_J (inducedChannel R_J access) where
 118  ψ₀ := access.ψ₀
 119  i₀ := access.i₀
 120  χ := access.χ
 121  χ_ne_zero := access.χ_ne_zero
 122  readout := fun _ => rfl
 123
 124/-! ## §3. The substrate locality / measurement-access principle -/
 125
 126/-- **Substrate locality / measurement-access principle for a channel.**
 127A channel response `R_C` *arises from substrate access* of a joint linear
 128operator `R_J` if there is access data such that `R_C` equals the
 129induced channel for that data.
 130
 131The general principle is the meta-claim that every operational channel
 132observable on the joint substrate is of this form. For Lean, we
 133encode the per-channel proposition; the substrate locality principle
 134is then asserted as a hypothesis on the specific `R_J / R_C` pair under
 135consideration. -/
 136def ArisesFromSubstrateAccess
 137    (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
 138    (R_C : Signal8 → Signal8) : Prop :=
 139  ∃ access : SubstrateAccessData, R_C = inducedChannel R_J access
 140
 141/-! ## §4. Substrate locality → section readout → amplitude-linear -/
 142
 143/-- **From the substrate locality principle, the channel is a section
 144readout.** This is the first link in the new derivation chain: substrate
 145locality is the substantive axiom; section readout follows. -/
 146theorem sectionReadout_of_arisesFromSubstrateAccess
 147    {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 148    {R_C : Signal8 → Signal8}
 149    (hAccess : ArisesFromSubstrateAccess R_J R_C) :
 150    Nonempty (JointSectionReadout R_J R_C) := by
 151  obtain ⟨access, hEq⟩ := hAccess
 152  refine ⟨{
 153    ψ₀ := access.ψ₀
 154    i₀ := access.i₀
 155    χ := access.χ
 156    χ_ne_zero := access.χ_ne_zero
 157    readout := ?_ }⟩
 158  intro φ
 159  have h := congrFun hEq φ
 160  simp [inducedChannel] at h
 161  exact h
 162
 163/-- **From substrate locality alone, the channel is amplitude-linear.**
 164No pure-tensor factorization, no operator-product hypothesis, no global
 165readout assumption: substrate locality + joint linearity is enough. -/
 166theorem isAmplitudeLinear_channel_of_arisesFromSubstrateAccess
 167    {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 168    {R_C : Signal8 → Signal8}
 169    (hAccess : ArisesFromSubstrateAccess R_J R_C) :
 170    IsAmplitudeLinear R_C := by
 171  obtain ⟨readout⟩ := sectionReadout_of_arisesFromSubstrateAccess hAccess
 172  exact isAmplitudeLinear_channel_of_sectionReadout readout
 173
 174/-- **Density-only collapse under substrate locality.** Any density-only
 175channel that arises from substrate access of a linear joint operator
 176collapses to the trivial zero response. -/
 177theorem channel_eq_zero_of_density_only_of_arisesFromSubstrateAccess
 178    {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 179    {R_C : Signal8 → Signal8}
 180    (hAccess : ArisesFromSubstrateAccess R_J R_C)
 181    (hDen : IsDensityOnly R_C) (φ : Signal8) :
 182    R_C φ = 0 :=
 183  eq_zero_of_isAmplitudeLinear_isDensityOnly
 184    (isAmplitudeLinear_channel_of_arisesFromSubstrateAccess hAccess) hDen φ
 185
 186/-- **No-go (existence form).** No nontrivial density-only channel can
 187arise from substrate access of a linear joint operator. -/
 188theorem not_exists_nontrivial_density_only_channel_with_substrateAccess :
 189    ¬ ∃ (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
 190        (R_C : Signal8 → Signal8),
 191      ArisesFromSubstrateAccess R_J R_C ∧
 192        IsDensityOnly R_C ∧
 193        (∃ φ : Signal8, R_C φ ≠ 0) := by
 194  rintro ⟨R_J, R_C, hAccess, hDen, φ, hφ⟩
 195  exact hφ
 196    (channel_eq_zero_of_density_only_of_arisesFromSubstrateAccess
 197       hAccess hDen φ)
 198
 199/-! ## §5. Factor-product implies substrate access (compatibility) -/
 200
 201/-- The earlier pure-tensor factorization hypothesis implies the new
 202substrate-access principle whenever the matter side is nontrivial at
 203some coordinate. The factorization-induced channel coincides with the
 204substrate-access induced channel for the witnessing data. -/
 205theorem arisesFromSubstrateAccess_of_pureTensorFactorization
 206    {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 207    {R_M R_C : Signal8 → Signal8}
 208    (hFact : PureTensorFactorization R_J R_M R_C)
 209    {ψ₀ : Signal8} {i₀ : Fin 8} (hχ : (R_M ψ₀) i₀ ≠ 0) :
 210    ArisesFromSubstrateAccess R_J R_C := by
 211  refine ⟨{ ψ₀ := ψ₀, i₀ := i₀, χ := (R_M ψ₀) i₀, χ_ne_zero := hχ }, ?_⟩
 212  funext φ
 213  unfold inducedChannel
 214  show R_C φ = ((R_M ψ₀) i₀)⁻¹ •
 215    (extractSecond i₀) (R_J (insertFirst ψ₀ φ))
 216  rw [insertFirst_apply, hFact, extractSecond_tmul, smul_smul,
 217    inv_mul_cancel₀ hχ, one_smul]
 218
 219/-! ## §6. Canonical substrate-access inhabitant (recognition probe) -/
 220
 221/-- **Canonical substrate-access witness: the recognition probe.** Take
 222the matter reference state to be the constant-1 signal and the channel
 223readout coordinate to be `0`. The calibration scalar is `(recognitionUpdate 1) 0`,
 224which is `1` by the cyclic-shift unfolding. This makes the substrate-access
 225hypothesis space non-vacuously inhabited for the canonical recognition
 226coupling. -/
 227def recognitionProbeAccess : SubstrateAccessData where
 228  ψ₀ := (1 : Signal8)
 229  i₀ := 0
 230  χ := (recognitionUpdate (1 : Signal8)) 0
 231  χ_ne_zero := by
 232    -- (recognitionUpdate 1) 0 = (1 : Signal8) ⟨1, _⟩ = 1 ≠ 0
 233    show (1 : Signal8) ⟨1, by decide⟩ ≠ (0 : ℂ)
 234    exact one_ne_zero
 235
 236/-- The canonical recognition-coupled joint operator (Session 87) with its
 237recognition-side channel response arises from the recognition-probe
 238substrate access. This makes the substrate-access proposition non-vacuously
 239inhabited. -/
 240theorem canonicalCyclicJointOperator_arisesFromRecognitionProbe :
 241    ArisesFromSubstrateAccess canonicalCyclicJointOperator recognitionUpdate := by
 242  apply arisesFromSubstrateAccess_of_pureTensorFactorization
 243    canonicalCyclicJointOperator_pureTensorFactorization
 244    (ψ₀ := (1 : Signal8)) (i₀ := 0)
 245  show (recognitionUpdate (1 : Signal8)) 0 ≠ (0 : ℂ)
 246  show (1 : Signal8) ⟨1, by decide⟩ ≠ (0 : ℂ)
 247  exact one_ne_zero
 248
 249/-! ## §7. Master cert -/
 250
 251/-- Master cert for the substrate locality / measurement-access principle.
 252Records the implication chain
 253`ArisesFromSubstrateAccess → JointSectionReadout → IsAmplitudeLinear`
 254along with the no-go theorem on density-only channels and the
 255non-vacuous inhabitant. -/
 256structure SubstrateLocalAccessCert where
 257  /-- Substrate access implies section readout (key link in the chain). -/
 258  section_readout_from_access :
 259    ∀ {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 260      {R_C : Signal8 → Signal8},
 261      ArisesFromSubstrateAccess R_J R_C →
 262        Nonempty (JointSectionReadout R_J R_C)
 263  /-- Substrate access forces channel amplitude-linearity. -/
 264  amplitude_linear_from_access :
 265    ∀ {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 266      {R_C : Signal8 → Signal8},
 267      ArisesFromSubstrateAccess R_J R_C → IsAmplitudeLinear R_C
 268  /-- Density-only collapse under substrate access. -/
 269  density_only_collapse :
 270    ∀ {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 271      {R_C : Signal8 → Signal8},
 272      ArisesFromSubstrateAccess R_J R_C → IsDensityOnly R_C →
 273        ∀ φ, R_C φ = 0
 274  /-- Existence-form no-go for nontrivial classical mediators. -/
 275  no_nontrivial_density_only :
 276    ¬ ∃ (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
 277        (R_C : Signal8 → Signal8),
 278      ArisesFromSubstrateAccess R_J R_C ∧ IsDensityOnly R_C ∧
 279        (∃ φ : Signal8, R_C φ ≠ 0)
 280  /-- Compatibility: factor-product implies substrate access. -/
 281  factorization_implies_access :
 282    ∀ {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 283      {R_M R_C : Signal8 → Signal8},
 284      PureTensorFactorization R_J R_M R_C →
 285        ∀ {ψ₀ : Signal8} {i₀ : Fin 8}, (R_M ψ₀) i₀ ≠ 0 →
 286          ArisesFromSubstrateAccess R_J R_C
 287  /-- Non-vacuous inhabitant: the canonical recognition-coupling. -/
 288  canonical_witness :
 289    ArisesFromSubstrateAccess canonicalCyclicJointOperator recognitionUpdate
 290
 291noncomputable def substrateLocalAccessCert : SubstrateLocalAccessCert where
 292  section_readout_from_access := fun hAccess =>
 293    sectionReadout_of_arisesFromSubstrateAccess hAccess
 294  amplitude_linear_from_access := fun hAccess =>
 295    isAmplitudeLinear_channel_of_arisesFromSubstrateAccess hAccess
 296  density_only_collapse := fun hAccess hDen φ =>
 297    channel_eq_zero_of_density_only_of_arisesFromSubstrateAccess hAccess hDen φ
 298  no_nontrivial_density_only :=
 299    not_exists_nontrivial_density_only_channel_with_substrateAccess
 300  factorization_implies_access := by
 301    intro R_J R_M R_C hFact ψ₀ i₀ hχ
 302    exact arisesFromSubstrateAccess_of_pureTensorFactorization
 303      (R_J := R_J) (R_M := R_M) (R_C := R_C)
 304      hFact (ψ₀ := ψ₀) (i₀ := i₀) hχ
 305  canonical_witness :=
 306    canonicalCyclicJointOperator_arisesFromRecognitionProbe
 307
 308theorem substrateLocalAccessCert_inhabited :
 309    Nonempty SubstrateLocalAccessCert :=
 310  ⟨substrateLocalAccessCert⟩
 311
 312/-! ## §8. One-statement substrate locality theorem -/
 313
 314/-- **SUBSTRATE LOCALITY ONE-STATEMENT (Session 113).** Under the substrate
 315measurement-access principle on the joint substrate `Signal8 ⊗[ℂ] Signal8`,
 316the channel response is automatically amplitude-linear and any density-only
 317response collapses to zero. The principle is non-vacuously inhabited by the
 318canonical recognition-coupling. Section readout (Session 111) is no longer
 319an assumption; it is a derived consequence of substrate locality + joint
 320linearity. The factor-product theorem (Sessions 85-88) is also a corollary.
 321
 322This sits one level deeper in the substrate axiomatisation than Session
 323111. The remaining unconditional step is to derive the
 324`ArisesFromSubstrateAccess` proposition itself from T0-T8 alone, i.e.,
 325to show that every operational recognition observable on the joint
 326substrate must be of induced form. That is substrate semantics and is the
 327next session-scale target. -/
 328theorem substrate_local_access_one_statement :
 329    (∀ {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 330       {R_C : Signal8 → Signal8},
 331       ArisesFromSubstrateAccess R_J R_C →
 332         Nonempty (JointSectionReadout R_J R_C)) ∧
 333    (∀ {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 334       {R_C : Signal8 → Signal8},
 335       ArisesFromSubstrateAccess R_J R_C → IsAmplitudeLinear R_C) ∧
 336    (∀ {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
 337       {R_C : Signal8 → Signal8},
 338       ArisesFromSubstrateAccess R_J R_C → IsDensityOnly R_C →
 339         ∀ φ, R_C φ = 0) ∧
 340    (¬ ∃ (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
 341         (R_C : Signal8 → Signal8),
 342       ArisesFromSubstrateAccess R_J R_C ∧ IsDensityOnly R_C ∧
 343         (∃ φ : Signal8, R_C φ ≠ 0)) ∧
 344    ArisesFromSubstrateAccess canonicalCyclicJointOperator recognitionUpdate :=
 345  ⟨fun hAccess => sectionReadout_of_arisesFromSubstrateAccess hAccess,
 346   fun hAccess => isAmplitudeLinear_channel_of_arisesFromSubstrateAccess hAccess,
 347   fun hAccess hDen φ =>
 348     channel_eq_zero_of_density_only_of_arisesFromSubstrateAccess hAccess hDen φ,
 349   not_exists_nontrivial_density_only_channel_with_substrateAccess,
 350   canonicalCyclicJointOperator_arisesFromRecognitionProbe⟩
 351
 352end AmplitudeLinearForced
 353end QuantumChannel
 354end Gravity
 355end IndisputableMonolith
 356