insertSecond
plain-language theorem explainer
Fixes a channel state φ and returns the ℂ-linear embedding of matter signals into the joint substrate by pure tensors on the right: ψ ↦ ψ ⊗ φ. Gravity Track 2.C uses it to probe pure-tensor factorizations of joint operators. The body is the flipped Mathlib tensor-product constructor applied to φ.
Claim. For a fixed channel state $\varphi \in \mathrm{Signal}_8$, there is a $\mathbb{C}$-linear map $\mathrm{insertSecond}(\varphi): \mathrm{Signal}_8 \to \mathrm{Signal}_8 \otimes_{\mathbb{C}} \mathrm{Signal}_8$ given by $\psi \mapsto \psi \otimes \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 $J = \mathrm{Signal}8 \otimes{\mathbb{C}} \mathrm{Signal}_8$: first factor matter ledger, second factor channel ledger.
A pure-tensor factorization of a joint operator $R_J$ means $R_J(\psi \otimes \varphi) = R_M(\psi) \otimes R_C(\varphi)$ on elementary tensors. To extract factor responses and force amplitude-linearity on one side from nontriviality on the other, one needs canonical linear sections that plant a fixed factor state while varying the other.
insertSecond is the right-factor section: hold the channel state fixed and vary matter. Its sibling insertFirst does the symmetric left insertion.
proof idea
One-line definition. TensorProduct.mk ℂ Signal8 Signal8 is the canonical bilinear map $(\psi,\varphi)\mapsto\psi\otimes\varphi$. Flipping it (Mathlib LinearMap.flip) yields a map that is linear in the first argument once the second is fixed; applying that flipped map to $\varphi$ produces the desired $\mathbb{C}$-linear map $\psi\mapsto\psi\otimes\varphi$.
why it matters
Infrastructure for the joint-substrate lift of amplitude-linear forcing. The simp lemma insertSecond_apply records the pure-tensor action. The main consumer is isAmplitudeLinear_matter_of_pureTensorFactorization: if $R_J$ factorizes on pure tensors and the channel response is nontrivial at some coordinate, the matter response is amplitude-linear. That forward direction, with its channel-side twin and the density-only collapse, is the Track 2.C closure step under the binary-tensor model (paper IV T2 upgrade path). Full closure still needs the joint Schrödinger-linearity lift via PiTensorProduct.map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.