manyBodyPhysicalChannelResponse_tprod
plain-language theorem explainer
On pure tensors of a finite many-body channel ledger, the many-body physical channel response factors sitewise into the local binary physical responses. Track 2.C many-body integrations cite this to reduce macroscopic channel action to per-site binary data. The proof unfolds the linear-map packaging, applies the Pi-tensor map-on-tprod identity, and matches each factor by the binary linear witness.
Claim. Let $\iota$ be finite. 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$ be its physical channel response (arising from substrate access). Then the induced many-body response sends a pure tensor $\bigotimes_i\varphi(i)$ to $\bigotimes_i R_C(i)(\varphi(i))$.
background
This module closes Gravity Track 2.C unconditionally from T0–T8 substrate semantics: the joint carrier is $\mathrm{JointSubstrate}=\mathrm{Signal}8\otimes{\mathbb{C}}\mathrm{Signal}_8$ (T7 eight-tick factors with matter–channel tensor structure), joint dynamics are $\mathbb{C}$-linear, and operational channel observables arise by substrate-internal measurement access (prepare a matter probe, apply $R_J$, extract a channel coordinate, calibrate by nonzero $\chi$).
A map $R_C$ is a physical channel response of $R_J$ when it arises that way: $R_C\varphi=\chi^{-1}\cdot\mathrm{extractSecond}_{i_0}(R_J(\mathrm{insertFirst},\psi_0,\varphi))$. Binary Track 2.C already forces every such $R_C$ to equal a unique $\mathbb{C}$-linear witness on $\mathrm{Signal}_8$.
The many-body ledger is the Pi-tensor product of sitewise channel factors. The many-body linear map is the Pi-tensor product of those binary linear witnesses; the many-body response is that map viewed as a function. This lemma records how that response acts on definite (pure-tensor) macroscopic configurations.
proof idea
Unfold the many-body response to the underlying many-body linear map (sitewise Pi-tensor of binary linear witnesses). Rewrite with the standard identity that a Pi-tensor product of linear maps sends a pure tensor to the pure tensor of the images. After a one-step congruence and funext on sites, each factor identity is the symmetry of the binary witness application lemma: under the physical-response hypothesis at site $i$, the local $R_C(i)$ agrees with its amplitude-linear witness on $\varphi(i)$.
why it matters
This is the pure-tensor computational content of the many-body lift of Track 2.C. Downstream it is packaged into the many-body amplitude-linearity certificate and into the Track 2.C many-body one-statement, which asserts that sitewise binary physical responses induce an amplitude-linear Pi-tensor response, act sitewise on pure tensors, and inherit local density-only collapse.
Framework-wise it sits on T7 (eight-tick $\mathrm{Signal}_8$ factors) and the joint tensor substrate forced by T0–T8 semantics; amplitude-linearity itself is the discharged structural hypothesis of the density-only no-go. Without sitewise pure-tensor action, many-body integrations could not reduce macroscopic channel evolution to the binary closure already proved per site.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.