insertFirst_apply
plain-language theorem explainer
Applying the first-factor insertion map at a fixed matter state ψ to a channel state φ recovers the pure tensor ψ ⊗ φ on the joint substrate. Gravity Track 2.C proofs that reduce joint operators along pure tensors cite this as the computational unfolding of that insertion. The equality is definitional: the proof is reflexivity from the tensor-product constructor.
Claim. For any two eight-component complex signals $\psi$ and $\varphi$, the first-factor insertion map at $\psi$, evaluated on $\varphi$, equals the pure tensor $\psi \otimes_{\mathbb{C}} \varphi$ in the joint matter-plus-channel substrate.
background
Track 2.C lifts the single-factor amplitude-linear dichotomy on Signal8 to the joint matter-plus-channel substrate. That substrate is the binary tensor product of two copies of the eight-tick ledger: the first factor is the matter ledger, the second the channel ledger.
First-factor insertion is the $\mathbb{C}$-linear map that freezes a matter state $\psi$ and sends a channel state $\varphi$ to the pure tensor $\psi \otimes_{\mathbb{C}} \varphi$. It is built as the curried tensor-product constructor TensorProduct.mk at $\psi$. Pure-tensor factorization of a joint operator then means the operator acts factorwise on such pure tensors.
This lemma is the pointwise evaluation identity for that insertion map. Downstream amplitude-linearity and substrate-access arguments repeatedly reduce joint expressions by rewriting insertion applications to explicit tensors.
proof idea
One-line term proof by reflexivity. The insertion map is defined as TensorProduct.mk at the frozen matter state, so its application to $\varphi$ is definitionally the pure tensor $\psi \otimes_{\mathbb{C}} \varphi$. No lemmas are invoked beyond that definitional equality; the @[simp] attribute exposes the rewrite to automation.
why it matters
The lemma is the computational hinge for every pure-tensor reduction on the joint substrate. It is used by the channel-side Track 2.C forward theorem: if a joint $\mathbb{C}$-linear operator factorizes on pure tensors and the matter response is nontrivial at some coordinate, then the channel response is amplitude-linear. The same rewrite feeds the section-readout bridge (global factorization implies section readout under nontrivial matter coupling), the substrate-access implication from pure-tensor factorization, and the universal substrate-access operator calculation that recovers the induced channel.
In the paper-IV Track 2.C program this supports the joint-substrate closure step: under the binary-tensor model, no nontrivial density-only channel response survives nontrivial matter coupling. Full upgrade from model to theorem still needs the joint Schrödinger-linearity lift; this simp fact is infrastructure, not that closure itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.