physicalChannelLinearExtension
plain-language theorem explainer
Constructs the explicit ℂ-linear endomorphism of the eight-tick signal space that witnesses amplitude-linearity of any physical channel response. Given joint dynamics on the matter-channel tensor product and a substrate-access triple (probe, coordinate, calibration), it is the calibrated composite insert-then-evolve-then-extract. Downstream equality with the induced channel is definitional. Citation target for Track 2.C substrate-semantic closure.
Claim. Given a $\mathbb{C}$-linear joint dynamics $R_J$ on the matter-channel substrate $\mathrm{Signal}_8 \otimes_{\mathbb{C}} \mathrm{Signal}_8$ and substrate-access data (matter probe $\psi_0$, channel coordinate $i_0$, nonzero calibration $\chi$), define the physical-channel linear extension as the $\mathbb{C}$-linear map $\mathrm{Signal}_8 \to \mathrm{Signal}_8$ equal to $\chi^{-1} \cdot (\mathrm{extract}_{i_0} \circ R_J \circ \mathrm{insert}_{\psi_0})$.
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 endomorphism $R_J$ of that tensor product, the substrate lift of Schrödinger linearity.
Operational channel observables arise by substrate-local access: prepare a fixed matter probe $\psi_0$, apply $R_J$, extract a channel-side coordinate $i_0$, and calibrate by a nonzero scalar $\chi$. The maps $\mathrm{insertFirst},\psi$ and $\mathrm{extractSecond},i$ are the pure-tensor insertion $\varphi \mapsto \psi \otimes \varphi$ and the dual extraction (lid after mapping the first factor through evaluation at $i$).
Composition of these linear maps with $R_J$, scaled by $\chi^{-1}$, is therefore itself a $\mathbb{C}$-linear endomorphism of $\mathrm{Signal}_8$. That composite is the explicit witness named here.
proof idea
Definitional construction, not a proof. The body is the scalar multiple $\mathrm{access}.\chi^{-1}$ times the LinearMap composite $(\mathrm{extractSecond},\mathrm{access}.i_0) \circ R_J \circ (\mathrm{insertFirst},\mathrm{access}.\psi_0)$. Each piece is already a $\mathbb{C}$-linear map by construction of insertFirst, extractSecond, and the LinearMap type of $R_J$; composition and scalar multiplication preserve linearity. No tactics or lemmas beyond LinearMap.comp and smul.
why it matters
This is the substrate-semantic witness that amplitude-linearity of every physical channel response is forced by joint linearity plus substrate locality, with no extra structural hypothesis. The module status is THEOREM (0 sorry): combining T7 joint carrier, joint $\mathbb{C}$-linearity, and ArisesFromSubstrateAccess yields that the physical response is application of this endomorphism, hence amplitude-linear by composition.
The immediate parent is physicalChannelLinearExtension_eq_inducedChannel, which identifies the extension with the induced channel by rfl. That identification feeds the density-only no-go discharge and the canonical T0-T8 joint-dynamics certificates in the same module. Framework landmarks: T7 eight-tick octave on each tensor factor; Schrödinger-linearity lifted to the joint substrate; Track 2.C closure that retires IsAmplitudeLinear as a free hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.