PureTensorFactorization
plain-language theorem explainer
Pure-tensor factorization is the predicate that a ℂ-linear joint operator on the matter-channel tensor product acts on elementary tensors by separate factor maps. Anyone citing the Track 2.C joint-substrate lift, the amplitude-linearity forcing on either factor, or the density-only channel impossibility will invoke it. It is a definitional Prop encoding the physical content of independent matter and channel ledgers, not a proved claim.
Claim. Let $R_J$ be a $\mathbb{C}$-linear endomorphism of 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$. Pure-tensor factorization holds when, for every pair of signals $\psi, \varphi$, one has $R_J(\psi \otimes \varphi) = R_M(\psi) \otimes R_C(\varphi)$.
background
Track 2.C lifts the single-factor amplitude-linear dichotomy of Session 85 from one copy of Signal8 (the eight-tick ledger) to the joint matter-plus-channel substrate. That substrate is the binary tensor product $J := \mathrm{Signal}8 \otimes{\mathbb{C}} \mathrm{Signal}_8$, with the first factor the matter ledger and the second the channel ledger.
A joint response is a $\mathbb{C}$-linear map $R_J : J \to J$. The physical modelling assumption of independent sector dynamics is that $R_J$ does not mix the two ledgers on pure tensors: it acts as a product of a matter map $R_M$ and a channel map $R_C$. The present definition packages exactly that product law as a Prop.
Upstream, the only dependency is the abbreviation of the joint substrate itself. Downstream theorems then combine this factorization with joint linearity and nontriviality hypotheses to push amplitude-linearity (or density-only collapse) onto each factor.
proof idea
Definitional predicate, not a theorem. The body is the universal quantification over pure tensors $\psi \otimes \varphi$, equating the joint action to the elementary tensor of the two factor responses. No lemmas are applied; the Prop is the statement used as a hypothesis elsewhere.
why it matters
This is the structural hypothesis of master-plan §4 Track 2.C step 1: joint substrate as matter ledger tensor channel ledger, with $R_{\mathrm{joint}} = R_{\mathrm{matter}} \otimes R_{\mathrm{channel}}$ and no cross-sector coherence at the operator level.
It is the field of the named structure FactorizableJointSubstrate, and the hypothesis of the joint-substrate forcing theorems: amplitude-linearity of the matter factor, of the channel factor, and of both under bilateral nontriviality; and the Track 2.C closure step that a density-only channel response under nontrivial matter coupling must vanish. The certificate layer reuses it for the master forcing theorem (channel amplitude-linearity under recognition-coupled factorization) and the density-only impossibility theorem.
Full Track 2.C upgrade from MODEL to THEOREM still needs the joint recognition operator to be ℂ-linear via the Schrödinger lift; this definition supplies the factorization half of that package. It sits inside the gravity quantum-channel program that rules out classical density-matrix readouts on the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.