physicalChannelLinearExtension_eq_inducedChannel
plain-language theorem explainer
On the joint matter-channel substrate, the explicit ℂ-linear extension built from a substrate-access triple equals the operational induced channel pointwise. Anyone citing unconditional amplitude-linearity of physical channel responses needs this identification. The proof is pure definitional equality (rfl).
Claim. Let $R_J$ be a $\mathbb{C}$-linear endomorphism of the joint substrate $\mathrm{Signal}_8 \otimes_{\mathbb{C}} \mathrm{Signal}_8$, and let $(\psi_0, i_0, \chi)$ be substrate-access data ($\chi \neq 0$). For every channel signal $\varphi$, the linear extension $\chi^{-1}\cdot(\mathrm{extract}_{i_0}\circ R_J\circ\mathrm{insert}_{\psi_0})$ applied to $\varphi$ equals the induced channel readout of $\varphi$.
background
Track 2.C closes unconditional amplitude-linearity of physical channel responses from T0-T8 substrate semantics alone. The joint carrier is $\mathrm{JointSubstrate} = \mathrm{Signal}8 \otimes{\mathbb{C}} \mathrm{Signal}_8$ (T7 eight-tick factors, matter and channel ledgers). Joint dynamics is a $\mathbb{C}$-linear map $R_J$ on that tensor product.
Operational channel observables arise by substrate-local access: prepare a matter probe $\psi_0$, apply $R_J$, extract channel coordinate $i_0$, and calibrate by nonzero $\chi$. That data is packaged as SubstrateAccessData. The induced channel is the function $\varphi \mapsto \chi^{-1}\cdot\mathrm{extract}{i_0}(R_J(\mathrm{insert}{\psi_0}\varphi))$. The linear extension is the same composite written as a LinearMap $\mathrm{Signal}8\to{\ell}\mathrm{Signal}_8$.
The module's substrate-semantic claim is that every physical channel response is exactly this composite, hence amplitude-linear by composition of $\mathbb{C}$-linear maps.
proof idea
One-line definitional equality. Unfolding the linear extension at $\varphi$ yields $\chi^{-1}\cdot(\mathrm{extract}{i_0}\circ R_J\circ\mathrm{insert}{\psi_0})(\varphi)$, which is definitionally the body of the induced channel. The tactic is rfl; no lemmas are invoked.
why it matters
This identification is the witness bridge inside the unconditional Track 2.C closure: physical channel response equals an explicitly $\mathbb{C}$-linear endomorphism of $\mathrm{Signal}_8$, so amplitude-linearity is forced by joint linearity plus substrate locality, with no extra structural hypothesis. Downstream density-only collapse in the same module composes that forced amplitude-linearity with the single-factor substrate dichotomy to kill nontrivial density-only responses.
Framework landmarks: T7 supplies the eight-tick $\mathrm{Signal}_8$ factors; joint tensor structure and Schrödinger-style joint linearity lift the linear dynamics; substrate-local measurement access is the operational content of a recognition-update probe. The result is a proved bookkeeping step (0 sorry), not a new dynamical law, but it pins the semantic equality the amplitude-linearity certificate relies on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.