isAmplitudeLinear_channel_of_pureTensorFactorization
plain-language theorem explainer
Under pure-tensor factorization of a ℂ-linear joint operator on the matter-channel tensor product, a nontrivial matter response at one coordinate forces the channel-side response to be amplitude-linear. Gravity Track 2.C cites this as the channel half of the joint-substrate lift of Session 85's single-factor dichotomy. The proof builds an explicit linear witness: insert a fixed matter state, apply the joint map, extract the channel factor at that coordinate, and rescale by the inverse of the nonzero matter entry.
Claim. Let $R_J$ be a $\mathbb{C}$-linear endomorphism of $\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 $\psi_0$ and a coordinate $i_0 \in \{0,\ldots,7\}$ with $(R_M \psi_0)_{i_0} \neq 0$, then $R_C$ is amplitude-linear: it coincides with some $\mathbb{C}$-linear map on $\mathrm{Signal}_8$.
background
Track 2.C lifts the Session 85 single-factor dichotomy on Signal8 (no nontrivial response is both amplitude-linear and density-only) to the joint matter-plus-channel substrate. That substrate is the binary tensor product $J = \mathrm{Signal}8 \otimes{\mathbb{C}} \mathrm{Signal}_8$: first factor is the matter ledger, second is the channel ledger.
Pure-tensor factorization says a joint operator $R_J$ acts on elementary tensors by separate factor responses: $R_J(\psi \otimes \varphi) = R_M(\psi) \otimes R_C(\varphi)$. Physically this is the content of the joint substrate being a tensor product of the two ledgers. Amplitude-linearity of a map $R : \mathrm{Signal}_8 \to \mathrm{Signal}_8$ means $R$ coincides with some $\mathbb{C}$-linear endomorphism (the structural opposite of a density-only, CPTP-classical readout).
The module also supplies the insertion and extraction maps used below: insert a fixed matter (or channel) vector into a pure tensor, and extract a coordinate of one factor as a linear functional on the joint space.
proof idea
Term proof that constructs the linear witness for amplitude-linearity of $R_C$ and checks it equals $R_C$ pointwise.
Fix the nontrivial matter data $(\psi_0, i_0)$. Form the composite linear map $((R_M \psi_0){i_0})^{-1} \cdot \bigl(\mathrm{extractSecond}{i_0} \circ R_J \circ \mathrm{insertFirst}_{\psi_0}\bigr)$. On an arbitrary channel state $\varphi$, unfold scalar multiplication and composition, apply the insertion identity, invoke pure-tensor factorization, then the extraction identity on pure tensors. The resulting scalar product cancels by $z^{-1} z = 1$ from nontriviality, leaving $R_C \varphi$.
why it matters
This is the channel-side forward half of the joint-substrate lift in Gravity Track 2.C (paper IV T2). Its matter-side twin is the symmetric statement with roles reversed; together they feed the composite result that bilateral nontriviality forces both factor responses to be amplitude-linear.
The main parent is the Track 2.C closure step: under pure-tensor factorization, nontrivial matter coupling, and a density-only channel response, the channel collapses to zero. That dichotomy is exactly Session 85's single-factor obstruction lifted through this lemma. A further parent specializes the matter factor to the substrate recognition update and concludes channel amplitude-linearity automatically.
Full upgrade of Track 2.C from MODEL to THEOREM still needs the joint recognition operator to be ℂ-linear via the Schrödinger-linearity lift on the Pi tensor product; this lemma is the factorization half of that program. Zero sorry, no new RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.