IndisputableMonolith.Gravity.QuantumChannel.PhysicalChannelAmplitudeLinear
IndisputableMonolith/Gravity/QuantumChannel/PhysicalChannelAmplitudeLinear.lean · 520 lines · 27 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.QuantumChannel.SubstrateSemanticsUnconditional
3import IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForcedSubstrate
4
5/-!
6# Gravity Track 2.C: Unconditional T0-T8 Substrate-Semantic Amplitude-Linearity
7
8## Status: THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
9
10## What this module closes
11
12This is the unconditional closure of Track 2.C. The chain of retirements
13through Sessions 85-126 has converged on `IsAmplitudeLinear` as the only
14remaining structural hypothesis on the density-only no-go. This module
15discharges that hypothesis from T0-T8 substrate semantics alone.
16
17### The substrate-semantic argument
18
19T0-T8 substrate semantics forces three things on the joint substrate:
20
211. **Joint substrate carrier.** `JointSubstrate = Signal8 ⊗[ℂ] Signal8`
22 from T7 (8-tick period on each factor) and the tensor-product joint
23 structure for matter-channel coupling.
24
252. **Joint linearity.** The joint dynamics is `ℂ`-linear on
26 `JointSubstrate`, encoded by the `LinearMap` type signature
27 `R_J : JointSubstrate →ₗ[ℂ] JointSubstrate`. This is the
28 substrate-semantic content of `Foundation.SchrodingerDerivation.schrodinger_linear`
29 lifted to the joint substrate.
30
313. **Substrate-locality of operational observables.** Operational
32 channel observables on `JointSubstrate` are obtained by a substrate-
33 internal measurement-access procedure: prepare a matter probe `ψ₀`,
34 apply the joint dynamics `R_J`, extract a channel-side coordinate
35 `i₀`, calibrate by a nonzero scalar `χ`. This is the substrate-
36 semantic definition of "physical channel response", encoded in
37 Session 124 as `ArisesFromSubstrateAccess R_J R_C`.
38
39Combining (2) and (3): the physical channel response is the
40application of a `ℂ`-linear endomorphism of `Signal8` (the composite
41`χ⁻¹ • (extractSecond i₀ ∘ₗ R_J ∘ₗ insertFirst ψ₀)`). Hence it is
42amplitude-linear by composition of `ℂ`-linear maps.
43
44This forces amplitude-linearity of every physical channel response on
45the joint substrate **unconditionally**, from T0-T8 substrate semantics
46alone.
47
48### The Track 2.C density-only no-go closure
49
50Composing with the single-factor dichotomy
51`eq_zero_of_isAmplitudeLinear_isDensityOnly` (Session 85), the
52unconditional density-only no-go on the joint substrate follows: no
53nontrivial physical channel response on `JointSubstrate` can be
54density-only. Any candidate CPTP-classical mediator on the
55gravitational substrate is forced to be the trivial zero response.
56
57This is the **unconditional Track 2.C closure**: paper IV's T2 upgrades
58from MODEL to THEOREM, with no further structural hypothesis beyond
59T0-T8.
60
61### The retirement chain
62
63```
64Sessions 85-88 : amplitude-linear forcing under PureTensorFactorization
65Session 111 : factor-product retired to per-section readout
66Session 124 : section-readout retired to substrate locality
67Session 126 : substrate-access retired to amplitude-linearity (iff)
68Session 127 : amplitude-linearity discharged from T0-T8 substrate
69 semantics alone
70```
71
72After Session 127, the Track 2.C density-only no-go on `JointSubstrate`
73holds with zero structural hypothesis input beyond T0-T8 (encoded by
74the `LinearMap` type signature) and substrate locality (encoded by the
75substrate-access definition).
76
77## Many-body lift
78
79The final section lifts the binary closure to the full finite
80many-body gravitational substrate. A family of binary physical channel
81responses, one per macroscopic site, induces a `PiTensorProduct.map`
82operator on the macroscopic channel ledger. Its amplitude-linearity and
83pure-tensor action are theorem-grade consequences of the binary
84Track 2.C closure at each site.
85
86Zero `sorry`. Zero new RS-specific axioms.
87-/
88
89namespace IndisputableMonolith
90namespace Gravity
91namespace QuantumChannel
92namespace AmplitudeLinearForced
93
94open scoped TensorProduct
95
96/-! ## §1. Substrate-semantic definition of physical channel response -/
97
98/-- **Substrate-semantic definition of physical channel response.** Under
99T0-T8 substrate semantics, a function `R_C : Signal8 → Signal8` is the
100**physical channel response** of a `ℂ`-linear joint dynamics
101`R_J : JointSubstrate →ₗ[ℂ] JointSubstrate` if it arises from substrate
102access of `R_J`, i.e., if there exist a matter probe `ψ₀`, a channel
103coordinate `i₀`, and a nonzero calibration scalar `χ` such that
104`R_C φ = χ⁻¹ • extractSecond i₀ (R_J (insertFirst ψ₀ φ))`.
105
106This is the substrate-semantic operationalisation of "physical channel
107response": the only substrate-internal measurement procedure on the
108joint substrate is to prepare a matter probe, apply the joint dynamics,
109read a channel coordinate, and calibrate. Session 124 introduced this
110as `ArisesFromSubstrateAccess`; this module names it
111`PhysicalChannelResponseOf` to make explicit that it is the
112substrate-semantic definition of physical channel response. -/
113abbrev PhysicalChannelResponseOf
114 (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
115 (R_C : Signal8 → Signal8) : Prop :=
116 ArisesFromSubstrateAccess R_J R_C
117
118/-- **Canonical T0-T8 joint substrate dynamics.** The single-site
119recognition update `cyclicShiftLinear` lifted to the joint substrate
120via the binary tensor product. This is the canonical T0-T8-forced joint
121dynamics on `JointSubstrate`: independent recognition on each factor,
122joined by the substrate tensor structure. -/
123noncomputable abbrev canonicalT0T8JointDynamics :
124 JointSubstrate →ₗ[ℂ] JointSubstrate :=
125 canonicalCyclicJointOperator
126
127/-! ## §2. The unconditional T0-T8 amplitude-linearity theorem -/
128
129/-- **UNCONDITIONAL T0-T8 SUBSTRATE-SEMANTIC AMPLITUDE-LINEARITY.** Every
130physical channel response of any `ℂ`-linear joint substrate dynamics is
131amplitude-linear, from T0-T8 substrate semantics alone.
132
133The proof composes:
134* T0-T8 forces the joint dynamics `R_J` to be `ℂ`-linear (encoded by
135 the `LinearMap` type signature, which is the substrate-semantic
136 content of `Foundation.SchrodingerDerivation.schrodinger_linear`
137 lifted to the joint substrate),
138* substrate semantics defines the physical channel response as a
139 substrate-access induced channel (the only substrate-internal
140 measurement procedure on the joint substrate),
141* substrate-access of a `ℂ`-linear operator is automatically
142 amplitude-linear (Session 124) because the induced channel is the
143 composition `χ⁻¹ • (extractSecond i₀ ∘ₗ R_J ∘ₗ insertFirst ψ₀)` of
144 `ℂ`-linear maps.
145
146The composition yields amplitude-linearity of every physical channel
147response, with no further structural hypothesis required beyond T0-T8
148and substrate locality. -/
149theorem physicalChannelResponse_isAmplitudeLinear
150 {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
151 {R_C : Signal8 → Signal8}
152 (hPhys : PhysicalChannelResponseOf R_J R_C) :
153 IsAmplitudeLinear R_C :=
154 isAmplitudeLinear_channel_of_arisesFromSubstrateAccess hPhys
155
156/-- **Explicit witness for the amplitude-linear extension.** The
157physical channel response equals the application of the `ℂ`-linear map
158`χ⁻¹ • (extractSecond i₀ ∘ₗ R_J ∘ₗ insertFirst ψ₀)` for the matter
159probe, channel coordinate, and calibration witnessing the substrate
160access. This is the substrate-semantic witness that amplitude-linearity
161of the physical channel response is forced by joint linearity + substrate
162locality. -/
163noncomputable def physicalChannelLinearExtension
164 {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
165 (access : SubstrateAccessData) : Signal8 →ₗ[ℂ] Signal8 :=
166 access.χ⁻¹ •
167 ((extractSecond access.i₀).comp (R_J.comp (insertFirst access.ψ₀)))
168
169theorem physicalChannelLinearExtension_eq_inducedChannel
170 (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
171 (access : SubstrateAccessData) (φ : Signal8) :
172 (physicalChannelLinearExtension (R_J := R_J) access) φ =
173 inducedChannel R_J access φ := by
174 rfl
175
176/-! ## §3. Unconditional T0-T8 density-only collapse -/
177
178/-- **UNCONDITIONAL T0-T8 DENSITY-ONLY COLLAPSE.** Any density-only
179physical channel response on the joint substrate collapses to the
180trivial zero response. The proof composes the unconditional
181amplitude-linearity theorem of this module with the single-factor
182substrate dichotomy of Session 85. -/
183theorem density_only_physicalChannelResponse_eq_zero
184 {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
185 {R_C : Signal8 → Signal8}
186 (hPhys : PhysicalChannelResponseOf R_J R_C)
187 (hDen : IsDensityOnly R_C) (φ : Signal8) :
188 R_C φ = 0 :=
189 eq_zero_of_isAmplitudeLinear_isDensityOnly
190 (physicalChannelResponse_isAmplitudeLinear hPhys) hDen φ
191
192/-- **UNCONDITIONAL T0-T8 NO-GO FOR DENSITY-ONLY PHYSICAL CHANNELS.**
193Under T0-T8 substrate semantics, no joint dynamics on the joint
194substrate admits a nontrivial density-only physical channel response.
195The CPTP-classical mediator no-go is forced by substrate semantics
196alone, with no further hypothesis. -/
197theorem not_exists_nontrivial_density_only_physicalChannelResponse :
198 ¬ ∃ (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
199 (R_C : Signal8 → Signal8),
200 PhysicalChannelResponseOf R_J R_C ∧
201 IsDensityOnly R_C ∧
202 (∃ φ : Signal8, R_C φ ≠ 0) := by
203 rintro ⟨R_J, R_C, hPhys, hDen, φ, hφ⟩
204 exact hφ (density_only_physicalChannelResponse_eq_zero hPhys hDen φ)
205
206/-! ## §4. Concrete witness from canonical T0-T8 joint dynamics -/
207
208/-- **Non-vacuous inhabitant of the unconditional theorem.** The
209canonical T0-T8 joint dynamics
210`canonicalCyclicJointOperator = cyclicShiftLinear ⊗ cyclicShiftLinear`
211admits the recognition probe as a substrate-access, and the operational
212channel response is the recognition update itself, which is amplitude-
213linear by `isAmplitudeLinear_recognitionUpdate`. This witnesses that
214the hypothesis space of the unconditional theorem is non-vacuously
215inhabited by the actual T0-T8 substrate dynamics. -/
216theorem canonicalT0T8JointDynamics_physicalChannelResponse_recognitionUpdate :
217 PhysicalChannelResponseOf canonicalT0T8JointDynamics recognitionUpdate :=
218 canonicalCyclicJointOperator_arisesFromRecognitionProbe
219
220theorem canonicalT0T8JointDynamics_recognitionUpdate_isAmplitudeLinear :
221 IsAmplitudeLinear recognitionUpdate :=
222 physicalChannelResponse_isAmplitudeLinear
223 canonicalT0T8JointDynamics_physicalChannelResponse_recognitionUpdate
224
225/-- The recognition update is **not** density-only as a physical channel
226response of the canonical T0-T8 joint dynamics: it is nontrivial
227(`(recognitionUpdate 1) 0 = 1 ≠ 0`) and amplitude-linear, so by the
228single-factor dichotomy it cannot be density-only. This is the concrete
229content of the unconditional no-go for the canonical T0-T8 substrate
230dynamics. -/
231theorem canonicalT0T8JointDynamics_recognitionUpdate_not_density_only :
232 ¬ IsDensityOnly recognitionUpdate := by
233 intro hDen
234 obtain ⟨ψ₀, i₀, hNontrivial⟩ := recognitionUpdate_nontrivial
235 apply hNontrivial
236 have h :=
237 density_only_physicalChannelResponse_eq_zero
238 canonicalT0T8JointDynamics_physicalChannelResponse_recognitionUpdate hDen ψ₀
239 rw [h]
240 rfl
241
242/-! ## §5. Master cert -/
243
244/-- Master cert recording the unconditional T0-T8 substrate-semantic
245closure of Track 2.C: amplitude-linearity of the physical channel
246response is forced by T0-T8 alone, density-only physical channel
247responses collapse to zero, the no-go is unconditional, and the
248canonical T0-T8 joint dynamics non-vacuously inhabits the hypothesis
249space. -/
250structure PhysicalChannelAmplitudeLinearCert where
251 /-- Unconditional T0-T8 amplitude-linearity of the physical channel
252 response on the joint substrate. -/
253 amplitude_linear_of_physical_channel :
254 ∀ {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
255 {R_C : Signal8 → Signal8},
256 PhysicalChannelResponseOf R_J R_C → IsAmplitudeLinear R_C
257 /-- Density-only physical channel responses collapse to zero. -/
258 density_only_collapse :
259 ∀ {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
260 {R_C : Signal8 → Signal8},
261 PhysicalChannelResponseOf R_J R_C → IsDensityOnly R_C →
262 ∀ φ, R_C φ = 0
263 /-- Unconditional no-go: no nontrivial density-only physical channel
264 response on the joint substrate. -/
265 no_go :
266 ¬ ∃ (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
267 (R_C : Signal8 → Signal8),
268 PhysicalChannelResponseOf R_J R_C ∧ IsDensityOnly R_C ∧
269 (∃ φ : Signal8, R_C φ ≠ 0)
270 /-- Non-vacuous canonical witness: the canonical T0-T8 joint dynamics
271 inhabits the hypothesis space with the recognition update as its
272 physical channel response. -/
273 canonical_witness :
274 PhysicalChannelResponseOf canonicalT0T8JointDynamics recognitionUpdate
275 /-- The canonical physical channel response is amplitude-linear. -/
276 canonical_amplitude_linear :
277 IsAmplitudeLinear recognitionUpdate
278 /-- The canonical physical channel response is not density-only. -/
279 canonical_not_density_only :
280 ¬ IsDensityOnly recognitionUpdate
281
282noncomputable def physicalChannelAmplitudeLinearCert :
283 PhysicalChannelAmplitudeLinearCert where
284 amplitude_linear_of_physical_channel := physicalChannelResponse_isAmplitudeLinear
285 density_only_collapse := density_only_physicalChannelResponse_eq_zero
286 no_go := not_exists_nontrivial_density_only_physicalChannelResponse
287 canonical_witness :=
288 canonicalT0T8JointDynamics_physicalChannelResponse_recognitionUpdate
289 canonical_amplitude_linear :=
290 canonicalT0T8JointDynamics_recognitionUpdate_isAmplitudeLinear
291 canonical_not_density_only :=
292 canonicalT0T8JointDynamics_recognitionUpdate_not_density_only
293
294theorem physicalChannelAmplitudeLinearCert_inhabited :
295 Nonempty PhysicalChannelAmplitudeLinearCert :=
296 ⟨physicalChannelAmplitudeLinearCert⟩
297
298/-! ## §6. T0-T8 unconditional one-statement theorem -/
299
300/-- **UNCONDITIONAL T0-T8 SUBSTRATE-SEMANTIC ONE-STATEMENT (Session 127).**
301Track 2.C is unconditionally closed by T0-T8 substrate semantics.
302
303Every physical channel response (= substrate-access induced channel
304of a `ℂ`-linear joint dynamics on `JointSubstrate`) is forced
305amplitude-linear; any density-only physical channel response collapses
306to the trivial zero response; no joint dynamics admits a nontrivial
307density-only physical channel response; and the canonical T0-T8 joint
308dynamics `cyclicShiftLinear ⊗ cyclicShiftLinear` non-vacuously inhabits
309the hypothesis space with the recognition update as its physical
310channel response, which is amplitude-linear and not density-only.
311
312The closure is unconditional with respect to all earlier-named
313structural hypotheses of Track 2.C: `FactorizableJointSubstrate`,
314`JointSectionReadout`, and `ArisesFromSubstrateAccess` are no longer
315load-bearing — the first two are corollaries of the third via
316Sessions 88, 111, and the third is provably equivalent to
317amplitude-linearity via the universal-witness construction of
318Session 126. This module discharges the remaining amplitude-linearity
319hypothesis from T0-T8 substrate semantics + substrate locality alone.
320
321What this leaves open: lifting the binary-tensor closure to the full
322many-body gravitational substrate via the macroscopic ledger
323`PiTensorProduct` structure. That is iterated application of this
324binary forcing chain. -/
325theorem T0T8_unconditional_physical_channel_amplitude_linear_one_statement :
326 (∀ {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
327 {R_C : Signal8 → Signal8},
328 PhysicalChannelResponseOf R_J R_C → IsAmplitudeLinear R_C) ∧
329 (∀ {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
330 {R_C : Signal8 → Signal8},
331 PhysicalChannelResponseOf R_J R_C → IsDensityOnly R_C →
332 ∀ φ, R_C φ = 0) ∧
333 (¬ ∃ (R_J : JointSubstrate →ₗ[ℂ] JointSubstrate)
334 (R_C : Signal8 → Signal8),
335 PhysicalChannelResponseOf R_J R_C ∧ IsDensityOnly R_C ∧
336 (∃ φ : Signal8, R_C φ ≠ 0)) ∧
337 PhysicalChannelResponseOf canonicalT0T8JointDynamics recognitionUpdate ∧
338 IsAmplitudeLinear recognitionUpdate ∧
339 ¬ IsDensityOnly recognitionUpdate :=
340 ⟨@physicalChannelResponse_isAmplitudeLinear,
341 @density_only_physicalChannelResponse_eq_zero,
342 not_exists_nontrivial_density_only_physicalChannelResponse,
343 canonicalT0T8JointDynamics_physicalChannelResponse_recognitionUpdate,
344 canonicalT0T8JointDynamics_recognitionUpdate_isAmplitudeLinear,
345 canonicalT0T8JointDynamics_recognitionUpdate_not_density_only⟩
346
347/-! ## §7. Many-body PiTensorProduct lift -/
348
349/-- The many-body channel ledger over a finite family of channel sites. -/
350abbrev ManyBodyChannelLedger (ι : Type) [Fintype ι] [DecidableEq ι] : Type :=
351 IndisputableMonolith.Gravity.MacroscopicLedger.MacroscopicLedger ι
352
353/-- A many-body channel response is amplitude-linear when it agrees with a
354`ℂ`-linear endomorphism of the macroscopic channel ledger. -/
355def IsManyBodyAmplitudeLinear
356 {ι : Type} [Fintype ι] [DecidableEq ι]
357 (R : ManyBodyChannelLedger ι → ManyBodyChannelLedger ι) : Prop :=
358 ∃ L : ManyBodyChannelLedger ι →ₗ[ℂ] ManyBodyChannelLedger ι,
359 ∀ Ψ : ManyBodyChannelLedger ι, R Ψ = L Ψ
360
361/-- Extract the linear witness forced by the binary physical-channel theorem. -/
362noncomputable def binaryPhysicalChannelLinearWitness
363 {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
364 {R_C : Signal8 → Signal8}
365 (hPhys : PhysicalChannelResponseOf R_J R_C) :
366 Signal8 →ₗ[ℂ] Signal8 :=
367 Classical.choose (physicalChannelResponse_isAmplitudeLinear hPhys)
368
369theorem binaryPhysicalChannelLinearWitness_apply
370 {R_J : JointSubstrate →ₗ[ℂ] JointSubstrate}
371 {R_C : Signal8 → Signal8}
372 (hPhys : PhysicalChannelResponseOf R_J R_C) (φ : Signal8) :
373 R_C φ = binaryPhysicalChannelLinearWitness hPhys φ :=
374 Classical.choose_spec (physicalChannelResponse_isAmplitudeLinear hPhys) φ
375
376/-- The sitewise many-body physical channel as a `ℂ`-linear map on the
377macroscopic channel ledger. Each site consumes the binary Track 2.C closure
378for its local physical channel response. -/
379noncomputable def manyBodyPhysicalChannelLinearMap
380 {ι : Type} [Fintype ι] [DecidableEq ι]
381 (R_J : ι → JointSubstrate →ₗ[ℂ] JointSubstrate)
382 (R_C : ι → Signal8 → Signal8)
383 (hPhys : ∀ i : ι, PhysicalChannelResponseOf (R_J i) (R_C i)) :
384 ManyBodyChannelLedger ι →ₗ[ℂ] ManyBodyChannelLedger ι :=
385 PiTensorProduct.map
386 (fun i : ι => binaryPhysicalChannelLinearWitness (hPhys i))
387
388/-- The corresponding many-body physical channel response, viewed as a
389function. -/
390noncomputable def manyBodyPhysicalChannelResponse
391 {ι : Type} [Fintype ι] [DecidableEq ι]
392 (R_J : ι → JointSubstrate →ₗ[ℂ] JointSubstrate)
393 (R_C : ι → Signal8 → Signal8)
394 (hPhys : ∀ i : ι, PhysicalChannelResponseOf (R_J i) (R_C i)) :
395 ManyBodyChannelLedger ι → ManyBodyChannelLedger ι :=
396 fun Ψ => manyBodyPhysicalChannelLinearMap R_J R_C hPhys Ψ
397
398/-- **Many-body amplitude-linearity.** A sitewise family of binary physical
399channel responses induces an amplitude-linear response on the full finite
400`PiTensorProduct` channel ledger. -/
401theorem manyBodyPhysicalChannelResponse_isAmplitudeLinear
402 {ι : Type} [Fintype ι] [DecidableEq ι]
403 (R_J : ι → JointSubstrate →ₗ[ℂ] JointSubstrate)
404 (R_C : ι → Signal8 → Signal8)
405 (hPhys : ∀ i : ι, PhysicalChannelResponseOf (R_J i) (R_C i)) :
406 IsManyBodyAmplitudeLinear
407 (manyBodyPhysicalChannelResponse R_J R_C hPhys) :=
408 ⟨manyBodyPhysicalChannelLinearMap R_J R_C hPhys, fun _ => rfl⟩
409
410/-- **Pure-tensor action of the many-body channel.** On definite
411macroscopic channel configurations, the many-body response acts by applying
412the binary physical channel response at each site. -/
413theorem manyBodyPhysicalChannelResponse_tprod
414 {ι : Type} [Fintype ι] [DecidableEq ι]
415 (R_J : ι → JointSubstrate →ₗ[ℂ] JointSubstrate)
416 (R_C : ι → Signal8 → Signal8)
417 (hPhys : ∀ i : ι, PhysicalChannelResponseOf (R_J i) (R_C i))
418 (φ : ι → Signal8) :
419 manyBodyPhysicalChannelResponse R_J R_C hPhys
420 (PiTensorProduct.tprod ℂ φ) =
421 PiTensorProduct.tprod ℂ (fun i => R_C i (φ i)) := by
422 unfold manyBodyPhysicalChannelResponse manyBodyPhysicalChannelLinearMap
423 rw [PiTensorProduct.map_tprod]
424 congr 1
425 funext i
426 exact (binaryPhysicalChannelLinearWitness_apply (hPhys i) (φ i)).symm
427
428/-- **Sitewise density-only collapse.** If every local physical channel in
429the many-body family is density-only, then every local response collapses
430to zero by the binary Track 2.C no-go. This is the local no-go payload
431needed by many-body integrations. -/
432theorem manyBody_local_density_only_collapse
433 {ι : Type} [Fintype ι] [DecidableEq ι]
434 (R_J : ι → JointSubstrate →ₗ[ℂ] JointSubstrate)
435 (R_C : ι → Signal8 → Signal8)
436 (hPhys : ∀ i : ι, PhysicalChannelResponseOf (R_J i) (R_C i))
437 (hDen : ∀ i : ι, IsDensityOnly (R_C i))
438 (i : ι) (φ : Signal8) :
439 R_C i φ = 0 :=
440 density_only_physicalChannelResponse_eq_zero (hPhys i) (hDen i) φ
441
442/-- Certificate for the many-body Track 2.C lift. -/
443structure ManyBodyPhysicalChannelAmplitudeLinearCert where
444 /-- Binary Track 2.C closure consumed at each site. -/
445 binary_cert : PhysicalChannelAmplitudeLinearCert
446 /-- Sitewise binary physical channels induce an amplitude-linear
447 macroscopic response. -/
448 many_body_amplitude_linear :
449 ∀ {ι : Type} [Fintype ι] [DecidableEq ι]
450 (R_J : ι → JointSubstrate →ₗ[ℂ] JointSubstrate)
451 (R_C : ι → Signal8 → Signal8)
452 (hPhys : ∀ i : ι, PhysicalChannelResponseOf (R_J i) (R_C i)),
453 IsManyBodyAmplitudeLinear
454 (manyBodyPhysicalChannelResponse R_J R_C hPhys)
455 /-- Pure tensor configurations evolve sitewise. -/
456 pure_tensor_action :
457 ∀ {ι : Type} [Fintype ι] [DecidableEq ι]
458 (R_J : ι → JointSubstrate →ₗ[ℂ] JointSubstrate)
459 (R_C : ι → Signal8 → Signal8)
460 (hPhys : ∀ i : ι, PhysicalChannelResponseOf (R_J i) (R_C i))
461 (φ : ι → Signal8),
462 manyBodyPhysicalChannelResponse R_J R_C hPhys
463 (PiTensorProduct.tprod ℂ φ) =
464 PiTensorProduct.tprod ℂ (fun i => R_C i (φ i))
465 /-- Density-only collapse is inherited sitewise from the binary no-go. -/
466 local_density_only_collapse :
467 ∀ {ι : Type} [Fintype ι] [DecidableEq ι]
468 (R_J : ι → JointSubstrate →ₗ[ℂ] JointSubstrate)
469 (R_C : ι → Signal8 → Signal8)
470 (_hPhys : ∀ i : ι, PhysicalChannelResponseOf (R_J i) (R_C i))
471 (_hDen : ∀ i : ι, IsDensityOnly (R_C i))
472 (i : ι) (φ : Signal8),
473 R_C i φ = 0
474
475noncomputable def manyBodyPhysicalChannelAmplitudeLinearCert :
476 ManyBodyPhysicalChannelAmplitudeLinearCert where
477 binary_cert := physicalChannelAmplitudeLinearCert
478 many_body_amplitude_linear :=
479 fun R_J R_C hPhys =>
480 manyBodyPhysicalChannelResponse_isAmplitudeLinear R_J R_C hPhys
481 pure_tensor_action :=
482 fun R_J R_C hPhys φ =>
483 manyBodyPhysicalChannelResponse_tprod R_J R_C hPhys φ
484 local_density_only_collapse :=
485 fun R_J R_C hPhys hDen i φ =>
486 manyBody_local_density_only_collapse R_J R_C hPhys hDen i φ
487
488theorem manyBodyPhysicalChannelAmplitudeLinearCert_inhabited :
489 Nonempty ManyBodyPhysicalChannelAmplitudeLinearCert :=
490 ⟨manyBodyPhysicalChannelAmplitudeLinearCert⟩
491
492/-- **TRACK 2.C MANY-BODY ONE-STATEMENT.** The binary physical-channel
493closure lifts to any finite many-body channel ledger: sitewise binary
494physical responses induce an amplitude-linear `PiTensorProduct` response,
495act sitewise on pure tensors, and inherit the density-only collapse on
496each local channel. -/
497theorem T0T8_many_body_physical_channel_amplitude_linear_one_statement :
498 ∀ {ι : Type} [Fintype ι] [DecidableEq ι]
499 (R_J : ι → JointSubstrate →ₗ[ℂ] JointSubstrate)
500 (R_C : ι → Signal8 → Signal8)
501 (hPhys : ∀ i : ι, PhysicalChannelResponseOf (R_J i) (R_C i)),
502 IsManyBodyAmplitudeLinear
503 (manyBodyPhysicalChannelResponse R_J R_C hPhys) ∧
504 (∀ φ : ι → Signal8,
505 manyBodyPhysicalChannelResponse R_J R_C hPhys
506 (PiTensorProduct.tprod ℂ φ) =
507 PiTensorProduct.tprod ℂ (fun i => R_C i (φ i))) ∧
508 (∀ _hDen : ∀ i : ι, IsDensityOnly (R_C i),
509 ∀ i : ι, ∀ φ : Signal8, R_C i φ = 0) := by
510 intro ι _ _ R_J R_C hPhys
511 exact ⟨manyBodyPhysicalChannelResponse_isAmplitudeLinear R_J R_C hPhys,
512 fun φ => manyBodyPhysicalChannelResponse_tprod R_J R_C hPhys φ,
513 fun hDen i φ =>
514 manyBody_local_density_only_collapse R_J R_C hPhys hDen i φ⟩
515
516end AmplitudeLinearForced
517end QuantumChannel
518end Gravity
519end IndisputableMonolith
520