channel_eq_zero_of_density_only_of_pureTensorFactorization
plain-language theorem explainer
Under pure-tensor factorization of a ℂ-linear joint operator on the matter-plus-channel substrate, nontrivial matter response plus a density-only channel response forces the channel response to vanish identically. Gravity Track 2.C workers cite this as the joint-substrate closure of the single-factor amplitude-linear/density-only dichotomy. The proof is a one-line composition of the joint lift of amplitude-linearity with the Session 85 single-factor zero theorem.
Claim. Let $R_J$ be a $\mathbb{C}$-linear map on the joint substrate $\mathrm{Signal}_8 \otimes_{\mathbb{C}} \mathrm{Signal}_8$ that factorizes on pure tensors as $R_J(\psi \otimes \varphi) = R_M(\psi) \otimes R_C(\varphi)$. If the matter response is nontrivial at some coordinate ($(R_M \psi_0)_{i_0} \neq 0$) and the channel response $R_C$ is density-only (invariant under unit-modulus phase multiplications), then $R_C \varphi = 0$ for every channel state $\varphi$.
background
Session 85 closed the single-factor dichotomy on Signal8: no nontrivial channel response can be both amplitude-linear and density-only. Density-only means invariance under multiplication by unit-modulus scalars, the structural footprint of a CPTP-classical readout from the density matrix alone. Amplitude-linear responses are phase-equivariant and incompatible with that invariance unless identically zero.
This module lifts that dichotomy to the joint matter-plus-channel substrate modelled as the binary tensor product $\mathrm{JointSubstrate} := \mathrm{Signal}8 \otimes{\mathbb{C}} \mathrm{Signal}_8$. Pure-tensor factorization says the joint operator acts factor-wise: $R_J(\psi \otimes \varphi) = R_M(\psi) \otimes R_C(\varphi)$. The first factor is the matter ledger; the second is the channel ledger.
Upstream, isAmplitudeLinear_channel_of_pureTensorFactorization shows that under pure-tensor factorization and nontrivial matter coupling, the channel-side response is forced amplitude-linear. The single-factor dichotomy eq_zero_of_isAmplitudeLinear_isDensityOnly then kills any density-only candidate.
proof idea
One-line term proof. Apply isAmplitudeLinear_channel_of_pureTensorFactorization to the pure-tensor factorization hypothesis and the nontrivial matter coordinate, obtaining that $R_C$ is amplitude-linear. Feed that together with the density-only hypothesis into eq_zero_of_isAmplitudeLinear_isDensityOnly, which returns $R_C,\varphi = 0$ for arbitrary $\varphi$. No additional algebraic work; the joint lift and the Session 85 dichotomy compose directly.
why it matters
Track 2.C closure step at the joint-substrate level under the binary-tensor model: no joint substrate with nontrivial matter coupling admits a nontrivial density-only channel response. Equivalently, a candidate channel-side CPTP-classical readout collapses to zero.
It feeds the existence-form no-go not_exists_pureTensorFactorization_nontrivial_matter_density_only_channel, which packages the same content as "the hypotheses cannot be simultaneously satisfied." Full Track 2.C closure of paper IV T2 (upgrade from MODEL to THEOREM) still needs the joint recognition operator to be $\mathbb{C}$-linear via the Schrödinger lift (schrodinger_linear and PiTensorProduct.map); that is the next subsession. Zero sorry, zero new RS axioms. The eight-tick carrier Signal8 is the T7 octave substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.