isAmplitudeLinear_matter_of_pureTensorFactorization
plain-language theorem explainer
If a ℂ-linear joint operator on the matter–channel tensor product factorizes on pure tensors as R_J(ψ ⊗ φ) = R_M(ψ) ⊗ R_C(φ), and the channel factor is nonzero at some coordinate, then the matter response R_M is amplitude-linear. Track 2.C gravity cites this as the matter-side half of the joint-substrate lift of the Session 85 single-factor dichotomy. The proof builds an explicit witnessing linear map by sandwiching R_J between insert/extract maps and normalizing by the nonzero channel coordinate.
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$. Suppose $R_J(\psi \otimes \varphi) = R_M(\psi) \otimes R_C(\varphi)$ for all pure tensors, and there exist $\varphi_0$ and a coordinate $i_0 \in \{0,\ldots,7\}$ with $(R_C \varphi_0)_{i_0} \neq 0$. Then $R_M$ is amplitude-linear: it coincides with some $\mathbb{C}$-linear map $\mathrm{Signal}_8 \to_{\ell} \mathrm{Signal}_8$.
background
Session 85 closed a single-factor dichotomy on Signal8 (the eight-tick ledger): no nontrivial channel response is both amplitude-linear and density-only. This module lifts that dichotomy to the joint matter-plus-channel substrate
$$\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 of a joint operator $R_J$ means it acts factorwise on elementary tensors: $R_J(\psi \otimes \varphi) = R_M(\psi) \otimes R_C(\varphi)$. That is the algebraic content of the joint substrate being a tensor product of independent ledgers. Amplitude-linearity of a response $R : \mathrm{Signal}_8 \to \mathrm{Signal}_8$ means $R$ coincides with some $\mathbb{C}$-linear map (as opposed to an arbitrary set-function of the ledger).
The local setting is Gravity Track 2.C: joint-substrate lift of amplitude-linear forcing, with zero sorry and no new RS-specific axioms. Full paper-IV T2 closure still needs the joint recognition operator to be $\mathbb{C}$-linear via the Schrödinger lift.
proof idea
Term-mode construction of the witnessing linear map. Fix a channel seed $\varphi_0$ and coordinate $i_0$ with $(R_C \varphi_0)_{i_0} \neq 0$. Define
$$L := \bigl((R_C \varphi_0){i_0}\bigr)^{-1} \cdot \bigl(\mathrm{extractFirst}{i_0} \circ R_J \circ \mathrm{insertSecond}_{\varphi_0}\bigr).$$
Here insertSecond embeds $\psi \mapsto \psi \otimes \varphi_0$, and extractFirst i₀ reads the $i_0$-component of the first tensor factor. For arbitrary $\psi$, expand $L\psi$ by LinearMap.smul_apply and two comp_applys, apply insertSecond_apply, invoke pure-tensor factorization, then extractFirst_tmul. The scalar identity smul_smul plus inv_mul_cancel₀ on the nonzero channel coordinate cancels to one_smul, yielding $R_M \psi = L\psi$.
why it matters
Matter-side forward half of Track 2.C. It feeds two parents in the same module: the composite isAmplitudeLinear_both_of_pureTensorFactorization (both factors amplitude-linear under bilateral nontriviality), and the symmetric closure matter_eq_zero_of_density_only_of_pureTensorFactorization (under nontrivial channel coupling, no density-only matter response survives).
Composed with Session 85's single-factor dichotomy, the joint lift is the Track 2.C closure step 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 on the joint substrate.
Paper IV T2 still needs the upgrade from MODEL to THEOREM by combining this lift with schrodinger_linear (joint recognition operator is ℂ-linear via PiTensorProduct.map). That is the next Track 2.C subsession. The eight-tick structure of Signal8 is the T7 octave sitting under the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.