insertSecond_apply
plain-language theorem explainer
Evaluating the second-factor insertion map at a free eight-tick signal yields the pure tensor with that signal in the first factor and the fixed signal in the second. Joint-substrate arguments in Track 2.C cite this as the computational form of channel insertion. The equality is definitional: reflexivity from the flipped tensor-product constructor.
Claim. For eight-tick signals $\varphi,\psi$, the $\mathbb{C}$-linear insertion of a fixed second factor $\varphi$ into the joint substrate $S_8\otimes_{\mathbb{C}}S_8$ sends $\psi$ to the pure tensor $\psi\otimes_{\mathbb{C}}\varphi$.
background
Track 2.C lifts the single-factor amplitude-linear dichotomy on Signal8 (Session 85) to the joint matter-plus-channel substrate. That substrate is the binary tensor product $S_8\otimes_{\mathbb{C}}S_8$: first factor matter ledger, second factor channel ledger.
Insertion maps build pure tensors as linear maps in one factor. The second-factor insertion fixes a channel state $\varphi$ and returns the map $\psi\mapsto\psi\otimes_{\mathbb{C}}\varphi$, implemented as the flipped bilinear constructor of the tensor product. The companion first-factor insertion swaps roles.
These maps are the elementary pure-tensor builders used when a joint operator is assumed to factorize as $R_J(\psi\otimes\varphi)=R_M(\psi)\otimes R_C(\varphi)$.
proof idea
One-line term proof by rfl. Unfolding the second-factor insertion (flipped TensorProduct.mk partially applied to the fixed signal) is definitionally the pure tensor $\psi\otimes_{\mathbb{C}}\varphi$, so the equality holds by reflexivity. Marked @[simp] for automatic rewriting.
why it matters
Feeds the Track 2.C forward direction on the matter side: if a joint $\mathbb{C}$-linear operator factorizes on pure tensors and the channel response is nontrivial at some coordinate, then the matter response is amplitude-linear. The insertion map turns free matter states into joint pure tensors so the factorization hypothesis can be applied pointwise.
That matter-side lemma, with its channel-side twin and the density-only collapse, is the joint-substrate lift that closes Track 2.C under the binary-tensor model (paper IV T2, MODEL toward THEOREM). Full closure still needs the joint recognition operator to be $\mathbb{C}$-linear via the Schrödinger lift; this simp fact is only the pure-tensor plumbing.
No new RS axioms; zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.