extractFirst
plain-language theorem explainer
For each eight-tick coordinate i, a ℂ-linear map from the joint matter-channel substrate Signal8 ⊗ Signal8 back to Signal8 that recovers the matter factor of a pure tensor, scaled by the i-th channel amplitude. Downstream proofs of matter-side amplitude-linearity under pure-tensor factorization cite it to peel off the channel coordinate. Built as TensorProduct.map(id, evalAt i) composed with the right-unit isomorphism.
Claim. For each $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$ uniquely determined on pure tensors by $\psi \otimes \varphi \mapsto (\varphi_i)\,\psi$, where $\varphi_i$ is the $i$-th coordinate of the channel factor.
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 JointSubstrate := Signal8 ⊗[ℂ] Signal8: first factor is the matter ledger, second is the channel ledger; both copies of the eight-tick signal space Fin 8 → ℂ.
Coordinate evaluation evalAt i is the standard projection LinearMap.proj i : Signal8 →ₗ[ℂ] ℂ. Pure-tensor factorization of a joint operator means it acts factorwise: R_J(ψ ⊗ φ) = R_M(ψ) ⊗ R_C(φ). To force amplitude-linearity of R_M from nontriviality of R_C at some coordinate, one needs a linear way to read the matter factor off a joint pure tensor while sampling one channel coordinate.
This definition supplies that readout. The eight-tick index set is the T7 octave period 2^3 from the forcing chain.
proof idea
Definition, not a proof. Compose two standard Mathlib maps: first TensorProduct.map id (evalAt i), which on pure tensors sends ψ ⊗ φ to ψ ⊗ (φ i); then the right-unit isomorphism (TensorProduct.rid ℂ Signal8).toLinearMap, which identifies Signal8 ⊗ ℂ ≃ Signal8 and multiplies by the scalar. The composite is therefore linear on the whole tensor product by the universal property, with no custom lemmas required.
why it matters
Local plumbing for the Track 2.C joint-substrate lift. Its simp lemma extractFirst_tmul records the pure-tensor action extractFirst i (ψ ⊗ φ) = (φ i) • ψ, and that identity is the extraction step inside isAmplitudeLinear_matter_of_pureTensorFactorization: given factorization and a channel coordinate with (R_C φ₀) i₀ ≠ 0, one recovers amplitude-linearity of the matter response R_M.
That matter-side theorem is half of the bilateral forcing that, composed with the Session 85 single-factor dichotomy, yields the Track 2.C closure step channel_eq_zero_of_density_only_of_pureTensorFactorization (no nontrivial density-only channel response under nontrivial matter coupling). Full paper-IV T2 upgrade still needs the joint Schrödinger-linearity lift via PiTensorProduct.map; this def is only the extraction half of the factorization argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.