insertFirst
plain-language theorem explainer
Fixes a matter state ψ and returns the ℂ-linear map that tensors it on the left into the joint matter-plus-channel substrate: φ ↦ ψ ⊗ φ. Gravity Track 2.C proofs cite it to inject a reference matter section before applying a joint operator. The body is the standard Mathlib pure-tensor constructor TensorProduct.mk.
Claim. For a fixed eight-tick signal $\psi$, there is a $\mathbb{C}$-linear map from the channel ledger into the joint substrate $S_8\otimes_{\mathbb{C}}S_8$ sending $\varphi\mapsto \psi\otimes\varphi$.
background
Track 2.C works on the joint matter-plus-channel substrate, the binary tensor product $S_8\otimes_{\mathbb{C}}S_8$ of two copies of the eight-tick ledger Signal8. The first factor is the matter ledger; the second is the channel ledger. Session 85 already ruled out nontrivial single-factor responses that are both amplitude-linear and density-only; this module lifts that dichotomy to the joint setting.
Pure-tensor factorization of a joint operator means $R_J(\psi\otimes\varphi)=R_M(\psi)\otimes R_C(\varphi)$ on elementary tensors. To probe one factor while holding the other fixed, one needs canonical linear insertions of a fixed state into a chosen tensor slot. The companion insertion into the second factor is defined symmetrically.
The eight-tick structure of $S_8$ is the T7 octave from the forcing chain; the joint lift is the substrate on which T0–T8 recognition dynamics act factorwise.
proof idea
One-line definitional wrapper: apply Mathlib's TensorProduct.mk at the fixed first argument $\psi$. That constructor is already $\mathbb{C}$-bilinear in its two arguments, so currying on $\psi$ yields a map $S_8\to_{\ell}(S_8\otimes_{\mathbb{C}}S_8)$ with the stated pure-tensor action. The simp lemma insertFirst_apply is definitional equality to $\psi\otimes\varphi$.
why it matters
This insertion is the standard way Track 2.C builds matter sections of joint operators. Downstream, isAmplitudeLinear_channel_of_pureTensorFactorization uses it (with extraction) to force channel-side amplitude-linearity under nontrivial matter coupling. The section-readout structures JointSectionReadout and RecognitionSectionReadout encode the same inject-apply-extract pattern, and isAmplitudeLinear_channel_of_sectionReadout upgrades the forcing without a global factorization hypothesis.
Physical-channel material also depends on it: canonicalT0T8JointDynamics, the linear extension of the physical channel response, and the amplitude-linearity theorem for that response all sit on the joint substrate built from these insertions. Together with the Session 85 dichotomy, the pure-tensor lift supplies the Track 2.C closure step that a nontrivial density-only channel response cannot survive nontrivial matter coupling. Full paper-IV T2 upgrade still needs the Schrödinger-linearity lift on the joint substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.