not_exists_nontrivial_density_only_channel_with_substrateAccess
plain-language theorem explainer
No nontrivial density-only channel response can arise from substrate access of a linear joint operator on Signal8 ⊗ Signal8. Gravity-track workers cite this as the existence-form no-go under the measurement-access principle. The proof is a one-line unpack of the existential and appeal to the pointwise collapse lemma.
Claim. There do not exist a $\mathbb{C}$-linear joint operator $R_J$ on $\mathrm{Signal}_8 \otimes_{\mathbb{C}} \mathrm{Signal}_8$ and a channel map $R_C : \mathrm{Signal}_8 \to \mathrm{Signal}_8$ such that $R_C$ arises from substrate access of $R_J$, $R_C$ is density-only (phase-invariant under unit-modulus scalars), and $R_C$ is nontrivial ($R_C\varphi \neq 0$ for some $\varphi$).
background
Gravity Track 2.C closes the substrate locality / measurement-access principle: every operational channel on the joint substrate is harvested by fixing a matter reference $\psi_0$, applying a linear joint operator $R_J$ once, and reading one channel coordinate, normalised by a calibration scalar $\chi \neq 0$. Under that principle the channel equals the induced map, so section readout is definitional rather than assumed.
ArisesFromSubstrateAccess packages that claim per channel: $R_C$ equals inducedChannel for some access data. IsDensityOnly is the structural footprint of a CPTP-classical readout: $R(c\cdot\psi)=R(\psi)$ whenever $|c|=1$. The joint substrate is the binary tensor product of two Signal8 ledgers (matter and channel).
Upstream, Session 111 already forced amplitude-linearity from nonzero section readout. The remaining gap was that the physical channel is obtained by such a readout; this module derives that from substrate access. The pointwise collapse lemma channel_eq_zero_of_density_only_of_arisesFromSubstrateAccess is the immediate prior: density-only plus substrate access implies $R_C\varphi=0$ for every $\varphi$.
proof idea
Term-mode existence elimination. Unpack the assumed triple $(R_J,R_C)$ together with substrate-access, density-only, and a witness $\varphi$ with $R_C\varphi\neq 0$. Feed access and density-only into channel_eq_zero_of_density_only_of_arisesFromSubstrateAccess at $\varphi$ to obtain $R_C\varphi=0$, contradicting the witness. No further case analysis.
why it matters
This is the existence-form no-go of Session 113's substrate-locality chain. It feeds substrateLocalAccessCert (the density_only_collapse field) and the package theorem substrate_local_access_one_statement, which states that under substrate measurement-access the channel is automatically amplitude-linear and any density-only response collapses to zero.
In the module implication chain, substrate access yields joint section readout, which yields amplitude-linearity; density-only is then incompatible with nontriviality. Section readout (Session 111) is no longer an assumption but a derived consequence. The result blocks classical density-matrix-only gravity channels on the eight-tick joint ledger while leaving amplitude-linear recognition probes intact (the canonical recognition-coupling inhabits the principle non-vacuously).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.