Track2ManyBodyEndpoint
plain-language theorem explainer
Fork C endpoint proposition: any finite sitewise family of binary physical channel responses (each arising by substrate access from joint dynamics) induces an amplitude-linear map on the many-body Pi-tensor-product ledger, acts factorwise on pure tensors, and collapses under the density-only hypothesis. Integration-lane and unconditional-master consumers cite this Prop as the Track 2 handoff target. It is pure definitional packaging of three conjuncts, not a proved theorem.
Claim. For every finite index type $\iota$, every family of $\mathbb{C}$-linear joint dynamics $R_J(i)$ on $\mathrm{Signal}_8\otimes_{\mathbb{C}}\mathrm{Signal}_8$, and every family of channel maps $R_C(i):\mathrm{Signal}_8\to\mathrm{Signal}_8$ that arise by substrate access from $R_J(i)$, the induced many-body channel response on the $\Pi$-tensor-product ledger is amplitude-linear (agrees with some $\mathbb{C}$-linear endomorphism), acts sitewise on pure tensors, and if every local $R_C(i)$ is density-only then each $R_C(i)$ vanishes identically.
background
Track 7 (this module) is the integration-lane receipt for parallel fork handoffs A–F. Fork C is the Track 2.C many-body / Pi-tensor-product amplitude-linear lift. The module records what the new endpoints prove; it does not upgrade the discovery claim, and leaves Track 1 displacement-class leaves open.
The joint substrate is the binary tensor product $\mathrm{Signal}8\otimes{\mathbb{C}}\mathrm{Signal}_8$ (matter ledger times channel ledger). A map $R_C$ is a physical channel response of a linear joint dynamics $R_J$ when it arises by substrate access: there exist a matter probe, a channel coordinate, and a nonzero calibration scalar extracting $R_C$ from $R_J$. Density-only means phase invariance under unit-modulus scalars, the footprint of a CPTP-classical readout from the density matrix alone.
Many-body amplitude-linearity means the macroscopic channel response agrees with some $\mathbb{C}$-linear endomorphism of the many-body channel ledger. The induced many-body response is the lift of a finite sitewise family of such physical pairs to that ledger.
proof idea
Definitional packaging only: the body is the universal quantification over finite index types and sitewise physical pairs $(R_J(i),R_C(i))$, conjoined with three claims on the induced many-body response—existence of a linear witness (amplitude-linearity), factorwise action on pure tensors, and the density-only collapse to zero. No tactics or lemmas are applied here; the discharging theorem is the separate one-line wrapper that applies the T0–T8 many-body physical-channel amplitude-linear one-statement.
why it matters
This Prop is the Fork C handoff target consumed by the integration certificate and the one-statement receipts for forks A/B/C/D/E/F and A/C/F. Downstream, the unconditional master strengthens the D3 amplitude-linear proposition to include this many-body Pi-tensor-product endpoint alongside the binary physical-channel certificates.
In the Recognition framework it sits on the quantum-channel side of gravity: T0–T8 substrate semantics force physical channel responses, and the many-body lift extends single-site amplitude-linearity to finite sitewise families on the macroscopic ledger. The eight-tick signal space is the local ledger carrying the T7 octave structure.
It does not close the discovery theorem. Remaining open work is on Track 1 displacement-class Schläfli leaves; this endpoint only records the Track 2.C many-body lift for the integration lane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.