manyBodyPhysicalChannelResponse
plain-language theorem explainer
Given a finite family of sites, each equipped with a complex-linear joint matter-channel dynamics and a channel map that arises by substrate access, this definition packages the induced many-body channel response as an ordinary function on the macroscopic channel ledger. Gravity Track 2.C cites it when lifting binary amplitude-linearity to Pi-tensor product ledgers. The body is a one-line forgetful wrapper around the already-constructed linear map.
Claim. Fix a finite index set $\iota$. For each site $i\in\iota$, let $R_J(i)$ be a $\mathbb{C}$-linear endomorphism of the joint substrate $\mathrm{Signal}_8\otimes_{\mathbb{C}}\mathrm{Signal}_8$, and let $R_C(i):\mathrm{Signal}_8\to\mathrm{Signal}_8$ arise from substrate access of $R_J(i)$ (matter probe, channel coordinate, nonzero calibration). The many-body physical channel response is the function on the macroscopic channel ledger over $\iota$ obtained by applying the sitewise $\mathbb{C}$-linear map induced by the family $(R_J,R_C)$.
background
Track 2.C closes unconditional amplitude-linearity of physical channel responses from T0-T8 substrate semantics alone. The joint substrate is the binary tensor product $\mathrm{Signal}8\otimes{\mathbb{C}}\mathrm{Signal}_8$ (matter factor times channel factor), forced by the eight-tick octave (T7) on each factor. Joint dynamics are $\mathbb{C}$-linear endomorphisms of that carrier.
A channel map $R_C$ is a physical channel response of joint dynamics $R_J$ when it arises from substrate access: prepare a matter probe $\psi_0$, apply $R_J$, extract a channel coordinate $i_0$, and rescale by a nonzero calibration $\chi$. That composite is automatically amplitude-linear as a composition of $\mathbb{C}$-linear maps.
The many-body channel ledger is the macroscopic ledger over a finite site family $\iota$ (a $\mathrm{PiTensorProduct}$ of local $\mathrm{Signal}_8$ factors). The sibling linear map builds the sitewise $\mathbb{C}$-linear endomorphism of that ledger from a family of binary physical responses; the present definition is the same object viewed as a bare function.
proof idea
One-line wrapper. The body applies manyBodyPhysicalChannelLinearMap (the sitewise $\mathbb{C}$-linear endomorphism of the macroscopic ledger, which already consumes the binary Track 2.C closure at each site via the physical-response hypotheses) and forgets the LinearMap structure, returning an ordinary function ManyBodyChannelLedger ι → ManyBodyChannelLedger ι. No further algebraic work.
why it matters
This is the functional face of the many-body Track 2.C lift. Downstream, manyBodyPhysicalChannelResponse_isAmplitudeLinear proves the induced map is many-body amplitude-linear; manyBodyPhysicalChannelResponse_tprod records pure-tensor sitewise action; and T0T8_many_body_physical_channel_amplitude_linear_one_statement packages the full one-statement closure (amplitude-linearity, pure-tensor action, local density-only collapse).
The master handoff Track2ManyBodyEndpoint quotes exactly this setup: a finite sitewise family of binary physical responses induces an amplitude-linear response on the many-body ledger. The certificate structure ManyBodyPhysicalChannelAmplitudeLinearCert records the same lift. Framework-wise it sits on T7 (eight-tick Signal8 factors) and the joint-substrate tensor structure that forces binary amplitude-linearity unconditionally, then extends that closure from one site to any finite many-body ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.