matter_eq_zero_of_density_only_of_pureTensorFactorization
plain-language theorem explainer
If a joint recognition operator on Signal8 ⊗ Signal8 factorizes as R_M ⊗ R_C on pure tensors and the channel factor is nontrivial at some coordinate, then any density-only matter response R_M must vanish identically. Gravity Track 2.C cites this as the matter-side symmetric closure of the single-factor amplitude-linear dichotomy. The proof is a one-line composition: lift factorization to amplitude-linearity of R_M, then apply the Session 85 zero dichotomy.
Claim. Let $R_J$ be a $\mathbb{C}$-linear operator on the joint substrate $\mathrm{Signal}_8 \otimes_{\mathbb{C}} \mathrm{Signal}_8$, and let $R_M, R_C : \mathrm{Signal}_8 \to \mathrm{Signal}_8$ satisfy $R_J(\psi \otimes \varphi) = R_M(\psi) \otimes R_C(\varphi)$ for all pure tensors. Suppose some coordinate of $R_C(\varphi_0)$ is nonzero, and suppose $R_M$ is density-only (invariant under unit-modulus phase multiplications). Then $R_M(\psi) = 0$ for every $\psi$.
background
Track 2.C lifts the single-factor substrate dichotomy of Session 85 (AmplitudeLinearForced) to the joint matter-plus-channel substrate. The joint substrate is the binary tensor product $\mathrm{JointSubstrate} := \mathrm{Signal}8 \otimes{\mathbb{C}} \mathrm{Signal}_8$, with the first factor the matter ledger and the second the channel ledger.
Pure-tensor factorization says a joint operator acts factorwise: $R_J(\psi \otimes \varphi) = R_M(\psi) \otimes R_C(\varphi)$. Density-only means $R(c\cdot\psi) = R(\psi)$ whenever $|c|=1$; this is the structural footprint of a CPTP-classical readout from the density matrix alone. Amplitude-linearity is the competing structural condition from the recognition calculus.
Upstream, eq_zero_of_isAmplitudeLinear_isDensityOnly states the single-factor dichotomy: any response that is both amplitude-linear and density-only is identically zero on Signal8, proved by testing the two conditions at the unit-modulus scalar $c=-1$. The sibling lift isAmplitudeLinear_matter_of_pureTensorFactorization shows that nontrivial channel coupling forces the matter factor to be amplitude-linear.
proof idea
One-line term proof composing two prior results. First apply isAmplitudeLinear_matter_of_pureTensorFactorization to the pure-tensor factorization hypothesis and the nontrivial channel coordinate $(R_C\varphi_0)_{i_0}\neq 0$, obtaining that $R_M$ is amplitude-linear. Feed that together with the density-only hypothesis into eq_zero_of_isAmplitudeLinear_isDensityOnly, which returns $R_M\psi=0$ for arbitrary $\psi$.
why it matters
Symmetric matter-side closure of the Track 2.C no-go on the binary-tensor joint substrate. The module already records the channel-side twin channel_eq_zero_of_density_only_of_pureTensorFactorization as the primary Track 2.C closure step; this theorem is the dual statement under nontrivial channel coupling: no density-only matter response survives.
Together with the bilateral composite isAmplitudeLinear_both_of_pureTensorFactorization, it pins the structural content of pure-tensor factorization: nontrivial coupling on either factor forces amplitude-linearity on the other, and density-only then collapses that factor to zero. The module doc frames the remaining Track 2.C work as combining this lift with schrodinger_linear (joint recognition is $\mathbb{C}$-linear via PiTensorProduct.map) to upgrade paper IV T2 from MODEL to THEOREM. Zero sorry, no new RS axioms. Currently unused downstream; it stands as the matter-side twin of the channel no-go.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.