manyBodyPhysicalChannelLinearMap
plain-language theorem explainer
Sitewise physical channel responses on a finite family of sites assemble into one ℂ-linear endomorphism of the many-body channel ledger (the Pi-tensor product of Signal8 factors). Gravity Track 2.C citations of many-body amplitude-linearity use this map as the linear witness. Construction is the Pi-tensor product of the binary linear witnesses forced at each site by the physical-channel theorem.
Claim. Given a finite index set $\iota$ and, for each site $i\in\iota$, a $\mathbb{C}$-linear joint dynamics $R_{J,i}$ on $\mathrm{Signal}_8\otimes_{\mathbb{C}}\mathrm{Signal}_8$ together with a channel map $R_{C,i}:\mathrm{Signal}_8\to\mathrm{Signal}_8$ that arises from substrate access of $R_{J,i}$, there is an induced $\mathbb{C}$-linear endomorphism of the many-body channel ledger $\bigotimes_{i\in\iota}^{\Pi}\mathrm{Signal}_8$ obtained by applying, factorwise, the binary amplitude-linear witness of each local physical channel response.
background
This module is the unconditional Track 2.C closure: T0–T8 substrate semantics force amplitude-linearity of every physical channel response, with no remaining RS-internal axiom. The joint substrate is the binary tensor product $\mathrm{JointSubstrate}=\mathrm{Signal}8\otimes{\mathbb{C}}\mathrm{Signal}_8$ (matter factor times channel factor), forced by the T7 eight-tick period on each factor.
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$ when it arises from substrate access: there exist a matter probe $\psi_0$, a channel coordinate $i_0$, and a nonzero calibration $\chi$ such that $R_C\varphi=\chi^{-1}\cdot\mathrm{extractSecond}{i_0}(R_J(\mathrm{insertFirst},\psi_0,\varphi))$. The binary linear witness is the $\mathbb{C}$-linear endomorphism of $\mathrm{Signal}_8$ chosen from that amplitude-linearity theorem.
The many-body channel ledger over a finite site set $\iota$ is the macroscopic ledger on $\iota$, realized as a Pi-tensor product of channel factors. Sitewise families of joint dynamics and channel maps are the natural many-body input.
proof idea
One-line definitional wrapper. For each site $i$, apply the binary physical-channel linear witness to the local hypothesis that $R_{C,i}$ arises from substrate access of $R_{J,i}$; that yields a family of maps $\mathrm{Signal}8\to{\ell}[\mathbb{C}]\mathrm{Signal}_8$. Feed that family to PiTensorProduct.map, which is the unique $\mathbb{C}$-linear endomorphism of the Pi-tensor product acting factorwise. No further tactic work: the linear structure is inherited from the tensor-product universal property and the binary witnesses.
why it matters
This is the linear carrier for the many-body half of Track 2.C. Downstream, the corresponding function-level many-body response is defined by applying this map; the theorem that the many-body response is amplitude-linear packages exactly this endomorphism as the witness; and the pure-tensor action theorem records that on definite macroscopic configurations the map acts by the binary response at each site.
Framework-wise it lifts the single-site T0–T8 argument (joint carrier from T7, joint ℂ-linearity from the Schrödinger-derivation lift, substrate-local operational observables) to a finite collection of channel sites. That is the step from binary amplitude-linearity to macroscopic ledger amplitude-linearity needed for gravity-side channel coupling. It does not itself close the density-only no-go; it supplies the many-body linear object those no-go and certification results consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.