manyBody_local_density_only_collapse
plain-language theorem explainer
If every site in a finite many-body family has a physical channel response that is density-only, then each local channel map sends every eight-tick signal to zero. Gravity Track 2.C many-body lifts cite this as the sitewise no-go payload. The proof is a one-line specialization of the binary unconditional density-only collapse at each index.
Claim. Let $\iota$ be a finite index set. For each site $i$, 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)$. If every $R_C(i)$ is density-only (invariant under unit-modulus phase multiplications), then for every site $i$ and every signal $\varphi$, $R_C(i)(\varphi)=0$.
background
Track 2.C closes 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 ledger times channel ledger), forced by the T7 eight-tick period on each factor. Joint dynamics are $\mathbb{C}$-linear endomorphisms of that carrier.
A map $R_C$ is a physical channel response of joint dynamics $R_J$ when it arises by substrate access: prepare a matter probe, apply $R_J$, extract a channel coordinate, and calibrate by a nonzero scalar. Density-only means $R(c\cdot\psi)=R(\psi)$ whenever $|c|=1$, the structural footprint of a CPTP-classical readout from the pure-state density matrix alone.
The binary no-go already proved in this module states that any density-only physical channel response on the joint substrate is identically zero, by composing unconditional amplitude-linearity with the single-factor substrate dichotomy.
proof idea
One-line term wrapper. Instantiate the binary unconditional collapse density_only_physicalChannelResponse_eq_zero at the chosen site $i$, feeding the sitewise physical-response hypothesis and the sitewise density-only hypothesis, then evaluate on $\varphi$. No many-body algebra is needed beyond pointwise application.
why it matters
This is the local no-go payload for many-body integrations in Gravity Track 2.C. Downstream, manyBodyPhysicalChannelAmplitudeLinearCert packages the binary certificate with the many-body amplitude-linearity lift, and T0T8_many_body_physical_channel_amplitude_linear_one_statement asserts that sitewise binary physical responses induce an amplitude-linear Pi-tensor response, act sitewise on pure tensors, and inherit density-only collapse on each local channel.
Within the Recognition framework it sits on the T0–T8 forcing chain (especially T7’s eight-tick octave that sizes $\mathrm{Signal}_8$) and on the substrate-semantic reading of joint dynamics as $\mathbb{C}$-linear on the matter–channel tensor product. It does not invent a new dichotomy; it exports the binary collapse to finite families so many-body certificates can quote a uniform local vanishing statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.