density_only_physicalChannelResponse_eq_zero
plain-language theorem explainer
Any density-only physical channel response arising from T0-T8 joint substrate dynamics is identically zero on the eight-tick signal space. Gravity-track authors cite this when ruling out CPTP-classical mediators under substrate semantics alone. The proof is a one-line composition of unconditional amplitude-linearity with the single-factor dichotomy that amplitude-linear plus density-only forces the zero map.
Claim. Let $R_J$ be a $\mathbb{C}$-linear endomorphism of the joint substrate $\mathrm{Signal}_8\otimes_{\mathbb{C}}\mathrm{Signal}_8$, and let $R_C:\mathrm{Signal}_8\to\mathrm{Signal}_8$ be a physical channel response of $R_J$ (arising by substrate access: fixed matter probe, apply $R_J$, extract a channel coordinate, calibrate by nonzero scalar). If $R_C$ is density-only (invariant under unit-modulus phase multiplications), then $R_C\varphi=0$ for every $\varphi\in\mathrm{Signal}_8$.
background
Track 2.C closes unconditional T0-T8 substrate-semantic amplitude-linearity. The joint substrate is $\mathrm{Signal}8\otimes{\mathbb{C}}\mathrm{Signal}_8$, forced by the eight-tick octave (T7) on each factor with tensor-product matter-channel coupling. Joint dynamics are $\mathbb{C}$-linear endomorphisms of that carrier. A physical channel response is any map obtained by substrate-internal measurement access: insert a fixed matter probe, apply the joint map, extract a channel coordinate, and rescale by a nonzero calibration scalar.
Density-only means the response is invariant under $\psi\mapsto c\cdot\psi$ whenever $|c|=1$: the structural footprint of a CPTP-classical readout from the density matrix alone. Amplitude-linearity is $\mathbb{C}$-linearity of the response. Upstream, the single-factor substrate dichotomy states that any map on $\mathrm{Signal}_8$ that is both amplitude-linear and density-only vanishes identically (tested at the unit-modulus scalar $c=-1$).
proof idea
One-line term wrapper. From the physical-channel hypothesis, the module's unconditional amplitude-linearity theorem yields that the channel response is amplitude-linear. That fact and the density-only hypothesis are fed to the single-factor dichotomy (amplitude-linear and density-only implies the zero map on $\mathrm{Signal}_8$), evaluated at the given signal.
why it matters
Density-only collapse half of Track 2.C's unconditional closure. It feeds the existential no-go (no joint dynamics admits a nontrivial density-only physical channel response), the many-body sitewise collapse, the certificate that bundles amplitude-linearity with the no-go, and the one-statement T0-T8 summary. Downstream, the canonical recognition update is shown not density-only by combining a nontrivial witness with this collapse. Framework-wise it discharges the last structural hypothesis on the CPTP-classical mediator no-go from T0-T8 substrate semantics alone (joint carrier from T7, joint linearity lifted from Schrödinger linearity, substrate-local observables), with no remaining RS-internal axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.