factor_product_retirement_one_statement
plain-language theorem explainer
Under a nonzero matter-section readout of a joint linear operator, the channel response is amplitude-linear, and any density-only such response vanishes identically; no nontrivial density-only section-readout channel exists. Gravity Track 2.C cites this as the one-shot packaging that retires pure-tensor factorization. The proof is a three-component term assembling the already-proved section-readout lemmas.
Claim. The following hold simultaneously: (i) if a channel map $R_C:\mathrm{Signal}_8\to\mathrm{Signal}_8$ is recovered as a nonzero matter-section readout of a $\mathbb{C}$-linear joint operator $R_J$ on $\mathrm{Signal}_8\otimes\mathrm{Signal}_8$, then $R_C$ is amplitude-linear; (ii) if in addition $R_C$ is density-only, then $R_C\varphi=0$ for every $\varphi$; (iii) no pair $(R_J,R_C)$ admits a section readout for which $R_C$ is density-only and nontrivial.
background
Track 2.C studies gravitational channel responses on the eight-tick ledger Signal8. The joint matter-plus-channel substrate is the binary tensor product $R_J:\mathrm{Signal}8\otimes{\mathbb{C}}\mathrm{Signal}_8\to\mathrm{Signal}8\otimes{\mathbb{C}}\mathrm{Signal}_8$. Earlier modules forced amplitude-linearity of the channel factor only under full pure-tensor factorization of $R_J$.
A weaker operational hypothesis suffices: a nonzero matter-section readout. Fix a matter reference $\psi_0$, a coordinate $i_0\in\mathrm{Fin},8$, and a nonzero scalar $\chi$; recover $R_C\varphi=\chi^{-1}\cdot(\mathrm{extractSecond},i_0)(R_J(\psi_0\otimes\varphi))$. That linear slice already makes $R_C$ amplitude-linear. Amplitude-linearity means $R_C$ agrees with some $\mathbb{C}$-linear map (hence preserves coherent superpositions). Density-only means $R_C(c\cdot\psi)=R_C\psi$ whenever $|c|=1$, the footprint of a CPTP-classical density-matrix readout.
Upstream, isAmplitudeLinear_channel_of_sectionReadout proves the forcing, and channel_eq_zero_of_density_only_of_sectionReadout proves the density-only collapse; the nonexistence statement packages the dichotomy.
proof idea
Term-mode triple. The first conjunct is the function that applies isAmplitudeLinear_channel_of_sectionReadout to any section-readout hypothesis. The second conjunct applies channel_eq_zero_of_density_only_of_sectionReadout to a section readout plus a density-only hypothesis, yielding $R_C\varphi=0$ pointwise. The third conjunct is exactly not_exists_nontrivial_density_only_channel_with_sectionReadout. No new algebra is performed; the declaration is the one-shot conjunction of those three already-proved facts.
why it matters
This is the TRACK 2.C one-shot theorem in section-readout form. It closes the remaining gap named in the module doc: retiring the full pure-tensor factorization hypothesis that earlier certificates (AmplitudeLinearForcedJoint, AmplitudeLinearForcedCert) still carried. Factorization is recovered as a corollary because factorization implies section readout, so the older factor-product theorem sits strictly downstream of this weaker principle.
In the Recognition gravity program the point is structural: a physical channel response obtained by reading a linear joint substrate along one matter section cannot be a nontrivial density-only (classical) map; it must be amplitude-linear. That forces coherent, phase-sensitive channel behavior on the eight-tick ledger without assuming the joint operator splits on every pure tensor. No further used_by edges are recorded yet; the declaration is the packaged closure statement of the section-readout module itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.