manyBodyPhysicalChannelResponse_isAmplitudeLinear
plain-language theorem explainer
Sitewise families of binary physical channel responses, each arising from T0–T8 substrate access of a ℂ-linear joint dynamics, induce an amplitude-linear response on the finite many-body channel ledger (PiTensorProduct). Track 2.C many-body closure and its certificate cite this lift. The proof is a one-line packaging of the already-built linear-map witness with reflexivity.
Claim. Let $\iota$ be a finite index set. For families $R_J(i):\mathrm{JointSubstrate}\to_{\ell}\mathrm{JointSubstrate}$ and $R_C(i):\mathrm{Signal}_8\to\mathrm{Signal}_8$ such that each $R_C(i)$ is the physical channel response of $R_J(i)$ (arises from substrate access: matter probe, channel coordinate, nonzero calibration), the induced many-body response on the macroscopic channel ledger is amplitude-linear: there exists a $\mathbb{C}$-linear endomorphism $L$ of that ledger with $R(\Psi)=L(\Psi)$ for every ledger state $\Psi$.
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⊗channel). Joint dynamics are $\mathbb{C}$-linear endomorphisms of that carrier.
A map $R_C:\mathrm{Signal}_8\to\mathrm{Signal}_8$ is a physical channel response of $R_J$ when it arises from substrate access: prepare a matter probe $\psi_0$, apply $R_J$, extract a channel coordinate $i_0$, and calibrate by a nonzero scalar $\chi$. That composite is $\mathbb{C}$-linear on the channel factor, hence amplitude-linear at one site.
Many-body amplitude-linearity means the macroscopic response on the finite $\mathrm{PiTensorProduct}$ channel ledger agrees with some $\mathbb{C}$-linear endomorphism of that ledger. The many-body response and its linear witness are assembled sitewise from the binary Track 2.C data.
proof idea
Term-mode one-liner. The existential in many-body amplitude-linearity is witnessed by the already-defined sitewise linear map on the macroscopic ledger (each site consumes the binary physical-channel closure). The second component is fun _ => rfl, equating the functional many-body response with that linear map by definition. No further algebraic work.
why it matters
This is the many-body lift of binary Track 2.C amplitude-linearity. It feeds the many-body certificate (which packages binary cert plus this theorem) and the Track 2.C many-body one-statement: sitewise binary physical responses induce an amplitude-linear PiTensorProduct response, act sitewise on pure tensors, and inherit density-only collapse locally.
Framework landmarks: T7 forces the eight-tick $\mathrm{Signal}_8$ factors; joint linearity is the substrate-semantic lift of Schrödinger linearity; substrate-local operational observables force the channel response to be a composite of $\mathbb{C}$-linear maps. Together they discharge the last structural hypothesis on the density-only no-go for any finite many-body ledger, unconditionally from T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.