PhysicalChannelResponseOf
plain-language theorem explainer
Under T0–T8 substrate semantics, a channel map is a physical channel response of a ℂ-linear joint dynamics exactly when it arises by substrate access: prepare a matter probe, apply the joint map, extract one channel coordinate, and rescale by a nonzero calibration. Track 2.C proofs of amplitude-linearity and density-only collapse cite this predicate as the operational meaning of “physical response.” The body is a one-line abbreviation of the Session 124 access relation.
Claim. A map $R_C:\mathrm{Signal}_8\to\mathrm{Signal}_8$ is a physical channel response of a $\mathbb{C}$-linear joint dynamics $R_J$ on $\mathrm{JointSubstrate}=\mathrm{Signal}_8\otimes_{\mathbb{C}}\mathrm{Signal}_8$ if there exist a matter probe $\psi_0$, a channel coordinate $i_0$, and a nonzero calibration scalar $\chi$ such that $R_C(\varphi)=\chi^{-1}\cdot\mathrm{extract}_{i_0}\bigl(R_J(\mathrm{insert}(\psi_0,\varphi))\bigr)$ for every channel signal $\varphi$.
background
Track 2.C works on the joint substrate forced by T0–T8: each factor is an eight-tick signal space (T7), and matter–channel coupling is the tensor product $\mathrm{JointSubstrate}=\mathrm{Signal}8\otimes{\mathbb{C}}\mathrm{Signal}_8$. Joint dynamics is a $\mathbb{C}$-linear endomorphism of that carrier, matching the substrate reading of Schrödinger linearity lifted to the joint system.
Operational channel observables are not free maps on $\mathrm{Signal}_8$. The only substrate-internal measurement procedure is: prepare a fixed matter probe, apply the joint dynamics, read one channel-side coordinate, and calibrate by a nonzero scalar. Session 124 packaged that procedure as the access relation; this module renames it so that “physical channel response” is that relation, not an extra axiom.
The surrounding module then combines joint linearity with this access definition: every such response is a composite of $\mathbb{C}$-linear maps on $\mathrm{Signal}_8$, hence amplitude-linear, with no residual structural hypothesis.
proof idea
Definitional abbreviation only. The predicate is definitionally equal to the Session 124 access relation (existence of probe, channel index, and nonzero calibration making the extract–insert sandwich reproduce the channel map). No tactics, no lemmas, no new proof obligations.
why it matters
This is the semantic hinge of unconditional Track 2.C. Downstream, the binary amplitude-linearity theorem and its linear witness extraction take the predicate as hypothesis; the density-only collapse theorem states that any density-only physical response is identically zero; the many-body local collapse and the master handoff endpoint Track2ManyBodyEndpoint quantify over finite families of such responses and inherit sitewise amplitude-linearity plus density-only collapse.
A non-vacuous inhabitant is the canonical T0–T8 joint dynamics (independent cyclic recognition on each factor): its recognition update arises by substrate access, so the hypothesis class is inhabited by actual forced dynamics. Framework landmarks in play are T7 (eight-tick factors) and the joint tensor structure; the module status is full theorem closure (zero sorry) of the former amplitude-linearity hypothesis on the density-only no-go.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.