extractFirst_tmul
plain-language theorem explainer
On the joint substrate Signal8 tensor Signal8, the first-factor extractor at coordinate i sends a pure tensor ψ ⊗ φ to the scalar (φ i) times ψ. Cited by anyone deriving amplitude-linearity of a matter-side factor response from a pure-tensor factorization of a joint operator. Proof is a one-line simp through the extractor definition, map_tmul, and rid_tmul.
Claim. For every index $i \in \{0,\ldots,7\}$ and signals $\psi,\varphi \in \mathbb{C}^{8}$, the first-factor extractor at $i$ applied to the pure tensor $\psi \otimes \varphi$ equals $(\varphi_{i})\,\psi$.
background
Track 2.C lifts the single-factor amplitude-linear dichotomy on Signal8 to the joint matter-plus-channel substrate, modelled as the binary tensor product $J = \mathrm{Signal8} \otimes_{\mathbb{C}} \mathrm{Signal8}$. Session 85 closed the single-factor case: no nontrivial channel response is both amplitude-linear and density-only.
The first-factor extractor is the $\mathbb{C}$-linear map $J \to \mathrm{Signal8}$ that, on pure tensors, recovers the first factor scaled by the $i$-th coordinate of the second. It is assembled as $\mathrm{rid}$ after $\mathrm{map}(\mathrm{id},\mathrm{eval}_{i})$, using the universal property of the tensor product. The eight slots are the T7 eight-tick octave structure.
This identity is the pure-tensor evaluation of that extractor, the computational step needed whenever a joint operator is assumed to factorize as $R_{J}(\psi \otimes \varphi) = R_{M}(\psi) \otimes R_{C}(\varphi)$.
proof idea
One-line simp wrapper. Unfold the extractor definition, apply TensorProduct.map_tmul so that $\mathrm{map}(\mathrm{id},\mathrm{eval}{i})$ sends $\psi \otimes \varphi$ to $\psi \otimes (\varphi{i})$, then TensorProduct.rid_tmul to identify $\psi \otimes c$ with $c,\psi$. No case analysis or induction.
why it matters
Direct input to isAmplitudeLinear_matter_of_pureTensorFactorization, the Track 2.C forward direction on the matter side: if a $\mathbb{C}$-linear joint operator factorizes on pure tensors through factor responses $R_{M},R_{C}$, and the channel response is nontrivial at some coordinate $(R_{C}\varphi_{0}){i{0}}\neq 0$, then $R_{M}$ is amplitude-linear. That result, with its channel-side twin, feeds the Track 2.C closure step that no joint substrate with nontrivial matter coupling admits a nontrivial density-only channel response. Full paper-IV T2 upgrade (MODEL to THEOREM) still needs the joint Schrödinger-linearity lift via PiTensorProduct.map. The index set Fin 8 is the T7 eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.