channel_eq_zero_of_density_only_of_recognitionSectionReadout
plain-language theorem explainer
A density-only channel response recovered from a recognition-section readout of a linear joint substrate vanishes on every channel state. Gravity Track 2.C cites this to exclude classical density-matrix readouts under the weaker section-readout hypothesis (no full pure-tensor factorization). The proof is a one-line reduction through the general section-readout collapse lemma.
Claim. Let $R_J$ be a $\mathbb{C}$-linear map on the joint matter-channel substrate $\mathrm{Signal}_8 \otimes \mathrm{Signal}_8$ and $R_C$ a map on channel states. Suppose $R_C$ is recovered by a recognition-section readout of $R_J$ (fixed matter reference whose recognition update is nonzero at a chosen coordinate, with $R_C$ the corresponding linear slice). If $R_C$ is density-only, i.e. $R_C(c\cdot\psi)=R_C(\psi)$ whenever $\|c\|=1$, then $R_C(\varphi)=0$ for every channel state $\varphi$.
background
Track 2.C forces the physical channel response to be amplitude-linear without assuming full pure-tensor factorization of the joint operator. Earlier modules needed $R_J$ to act factorwise on every pure tensor. Here it is enough that $R_C$ arises as a nonzero matter section readout: fix a matter reference, a coordinate, and a nonzero scalar, and extract the second factor of $R_J$ applied to the pure tensor of that reference with the channel state.
A recognition-section readout specializes the matter section to the substrate recognition update (cyclic shift). The nontriviality side-condition is that this update is nonzero at the chosen coordinate, so the scalar inverse is well-defined. Density-only means invariance under unit-modulus complex rescaling: the structural footprint of any response computed from the density matrix alone, since $|\psi\rangle\langle\psi|$ is phase-invariant.
The joint substrate is the binary tensor product of two Signal8 ledgers (matter and channel). The upstream collapse lemma already shows that any density-only response recovered by a general nonzero section readout of a linear joint operator is identically zero.
proof idea
One-line term wrapper. Coerce the recognition-section readout hypothesis to an ordinary joint section readout via the structure projection toJointSectionReadout, then apply the upstream theorem that any density-only channel recovered by a nonzero section readout of a linear joint operator vanishes on every state. No new algebra is done here.
why it matters
Closes the density-only half of the recognition-specialized section-readout package in Gravity Track 2.C. The immediate parent is the non-existence theorem: there is no nontrivial density-only channel recoverable from a recognition-section readout of a linear joint substrate. Together with the companion amplitude-linearity result for the same readout class, this retires the stronger pure-tensor factorization hypothesis while still forcing the channel either to be amplitude-linear or to vanish under classical density-only assumptions.
In the Recognition framework this is structural forcing on the quantum channel side of gravity, not a numerical constant claim. It sits downstream of the joint-substrate and density-only dichotomy developed in the AmplitudeLinearForced modules, and supports the Track 2.C structural certificate that the physical readout cannot be a nontrivial CPTP-classical density response once the matter section is the actual recognition update.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.