isAmplitudeLinear_both_of_pureTensorFactorization
plain-language theorem explainer
Under pure-tensor factorization of a ℂ-linear joint matter-channel operator, bilateral nontriviality of the two factor responses forces both to be amplitude-linear. Gravity Track 2.C cites this as the composite of the two one-sided lifts. The proof is a one-line pairing of the matter-side and channel-side factorization lemmas.
Claim. Let $R_J$ be a $\mathbb{C}$-linear map 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. If there exist $\varphi_0$ and a coordinate $i_C$ with $(R_C\varphi_0)_{i_C}\neq 0$, and $\psi_0$ and $i_M$ with $(R_M\psi_0)_{i_M}\neq 0$, then both $R_M$ and $R_C$ are amplitude-linear (each agrees with some $\mathbb{C}$-linear map on $\mathrm{Signal}_8$).
background
Track 2.C studies gravitational-channel responses on the eight-tick ledger Signal8 (Fin 8 → ℂ). Session 85 closed the single-factor dichotomy: a response that is both amplitude-linear and density-only must vanish identically. Amplitude-linearity means the response agrees with some ℂ-linear map, so it preserves coherent superpositions.
This module lifts that story to the joint matter-plus-channel substrate JointSubstrate := Signal8 ⊗[ℂ] Signal8. Pure-tensor factorization says a joint operator acts factorwise on pure tensors: $R_J(\psi\otimes\varphi)=(R_M\psi)\otimes(R_C\varphi)$. Physically this encodes that the joint ledger is a tensor product of matter and channel ledgers.
The two one-sided theorems already show that nontriviality of one factor forces amplitude-linearity of the other. The present result packages both directions under bilateral nontriviality.
proof idea
Term-mode conjunction. The left conjunct is isAmplitudeLinear_matter_of_pureTensorFactorization applied to the factorization hypothesis and the channel-side nonzero witness $hC$. The right conjunct is the symmetric isAmplitudeLinear_channel_of_pureTensorFactorization with the matter-side nonzero witness $hM$. No further rewriting: the composite is exactly the pair of the two one-sided lifts.
why it matters
This is the composite forward direction named in the module doc for Track 2.C. It sits between the two one-sided pure-tensor lifts and the Track 2.C closure step channel_eq_zero_of_density_only_of_pureTensorFactorization, which composes the channel-side lift with Session 85's eq_zero_of_isAmplitudeLinear_isDensityOnly to rule out a nontrivial density-only channel under nontrivial matter coupling.
In the broader Recognition Gravity program this is the joint-substrate half of upgrading paper IV T2 from MODEL to THEOREM. Full closure still needs the joint recognition operator to be ℂ-linear via the Schrödinger-linearity lift (schrodinger_linear through PiTensorProduct.map). No downstream users yet; the immediate consumer is the density-only collapse theorem in the same module. Zero sorry, no new RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.