extractSecond_tmul
plain-language theorem explainer
On the joint matter-channel substrate Signal8 ⊗ Signal8, extracting the second factor at slot i from a pure tensor ψ ⊗ φ returns the scalar (ψ i) times φ. Anyone proving amplitude-linearity or substrate-access from pure-tensor factorization cites this as the evaluation identity for the second-factor probe. The proof is a one-line simp unfolding the linear-map definition against TensorProduct.map_tmul and lid_tmul.
Claim. For every slot $i \in \{0,\ldots,7\}$ and signals $\psi,\varphi \in \mathrm{Signal}_8$, the second-factor extraction map satisfies $\mathrm{extract}_2(i)(\psi \otimes \varphi) = (\psi_i)\,\varphi$.
background
Track 2.C lifts the single-factor amplitude-linear forcing of Session 85 from Signal8 to the joint matter-plus-channel substrate JointSubstrate := Signal8 ⊗[ℂ] Signal8. Pure tensors ψ ⊗ φ model product states of a matter factor and a channel factor; the eight coordinates are the eight-tick octave slots.
The second-factor probe extractSecond i is the ℂ-linear map that composes evaluation of the first factor at coordinate i with the left-unit isomorphism of the tensor product: it sends a pure tensor to the second factor scaled by the i-th amplitude of the first. Its sibling extractFirst plays the symmetric role.
This identity is the pure-tensor evaluation law for that probe. Downstream forcing arguments use it to pull a nontrivial matter (or channel) coordinate out of a factorized joint response and reduce to single-factor amplitude-linearity.
proof idea
One-line term-mode simp. Unfold extractSecond (TensorProduct.map of evalAt i with id, then left-unit), then apply TensorProduct.map_tmul and TensorProduct.lid_tmul to reduce (evalAt i ψ) • φ to (ψ i) • φ.
why it matters
This simp lemma is the computational hinge for the channel-side Track 2.C forward direction: isAmplitudeLinear_channel_of_pureTensorFactorization uses it to read off the channel response after a nontrivial matter coordinate is fixed. The same identity feeds sectionReadout_of_pureTensorFactorization and arisesFromSubstrateAccess_of_pureTensorFactorization, which show that pure-tensor factorization implies the weaker section-readout and substrate-access interfaces.
It also appears in the calculation that the universal substrate-access operator induces its witness linear map (universalSubstrateAccessOperator_inducedChannel). In the broader program this supports the Track 2.C closure step: under the binary-tensor model, no joint substrate with nontrivial matter coupling admits a nontrivial density-only channel response. Full paper-IV T2 upgrade still needs the joint Schrödinger-linearity lift; this lemma is infrastructure, not that closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.