extractSecond
plain-language theorem explainer
Linear map that pulls the channel factor out of a joint matter-channel state on Signal8 ⊗ Signal8, weighting by the i-th coordinate of the matter factor. On pure tensors it returns (ψ i) • φ. Downstream amplitude-linearity and section-readout theorems cite it as the extraction half of a matter-section readout. Defined by composing coordinate projection on the first factor with the left tensor unitor.
Claim. For each coordinate $i \in \{0,\ldots,7\}$, there is a $\mathbb{C}$-linear map $\mathrm{extract}_i : \mathrm{Signal}_8 \otimes_{\mathbb{C}} \mathrm{Signal}_8 \to \mathrm{Signal}_8$ such that on pure tensors $\mathrm{extract}_i(\psi \otimes \varphi) = (\psi_i)\,\varphi$. Equivalently, $\mathrm{extract}_i = \lambda \circ (\mathrm{ev}_i \otimes \mathrm{id})$, where $\mathrm{ev}_i$ is evaluation at coordinate $i$ and $\lambda$ is the left unitor $\mathbb{C}\otimes\mathrm{Signal}_8\to\mathrm{Signal}_8$.
background
Track 2.C lifts the single-factor amplitude-linear dichotomy on Signal8 (Session 85) to the joint matter-plus-channel substrate. The joint substrate is the binary tensor product $J = S \otimes_{\mathbb{C}} S$ with $S = \mathrm{Signal}_8 := \mathrm{Fin},8 \to \mathbb{C}$: first factor is the matter ledger, second is the channel ledger.
Coordinate evaluation $\mathrm{ev}i : S \to{\mathbb{C}} \mathbb{C}$ is ordinary projection onto the $i$-th component. The left unitor identifies $\mathbb{C} \otimes S$ with $S$. Together they give a canonical way to read out the channel factor after probing one matter coordinate.
The module works under pure-tensor factorization of joint operators and under weaker section-readout hypotheses; both need an extraction map of this shape. No new RS axioms; the construction is pure Mathlib tensor algebra.
proof idea
One-line definitional composition, not a tactic proof. Form the tensor-product map $\mathrm{ev}_i \otimes \mathrm{id}_S : S\otimes S \to \mathbb{C}\otimes S$, then post-compose with the linear map underlying the left unitor $\lambda : \mathbb{C}\otimes S \xrightarrow{\sim} S$. The resulting composite is $\mathbb{C}$-linear by construction. The companion simp lemma extractSecond_tmul unfolds TensorProduct.map_tmul and TensorProduct.lid_tmul to recover $(\psi_i),\varphi$ on elementary tensors.
why it matters
Extraction is the readout half of every joint-substrate argument that forces channel amplitude-linearity. It feeds extractSecond_tmul, then isAmplitudeLinear_channel_of_pureTensorFactorization (Track 2.C forward direction on the channel side under pure-tensor factorization and nontrivial matter coupling).
Section-readout variants reuse it: JointSectionReadout and RecognitionSectionReadout recover $R_C$ by inject-matter, apply $R_J$, extract at $i_0$, and rescale; isAmplitudeLinear_channel_of_sectionReadout concludes amplitude-linearity without a global factorization hypothesis. Physical-channel theorems (physicalChannelResponse_isAmplitudeLinear, physicalChannelLinearExtension, canonicalT0T8JointDynamics) inherit the same extraction.
In the broader RS picture this supports the Track 2.C closure of paper IV T2: on the joint substrate, a nontrivial density-only channel response is ruled out once the single-factor dichotomy is lifted, consistent with eight-tick (Fin 8) ledger structure from T7. Full upgrade from MODEL to THEOREM still needs the joint Schrödinger-linearity lift in later subsessions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.