track2_many_body_endpoint_holds
plain-language theorem explainer
Fork C's many-body endpoint asserts that any finite sitewise family of binary physical channel responses induces an amplitude-linear response on the many-body Π-tensor-product ledger, acts sitewise on pure tensors, and inherits local density-only collapse. Gravity integration and unconditional master-theorem lanes cite it as the Track 2.C handoff receipt. The proof is a one-line term wrapper of the Track 2.C many-body one-statement.
Claim. For every finite index type $\iota$ and every family of joint-substrate linear maps $R_J(i)$ and classical eight-tick channel maps $R_C(i)$ that form a physical channel response at each site $i\in\iota$, the induced many-body physical channel response on the $\Pi$-tensor product is amplitude-linear, acts sitewise on pure tensors, and inherits the local density-only collapse on each factor.
background
This module is the Track 7 integration-lane receipt for parallel gravity fork handoffs. Fork C is the Track 2.C many-body lift: binary physical channel responses on a joint substrate and an eight-tick classical signal are promoted to a finite many-body ledger built from the $\Pi$-tensor product. The endpoint proposition packages three properties: amplitude-linearity of the induced many-body response, sitewise action on pure tensors, and inheritance of the local density-only collapse.
The upstream Track 2.C one-statement already proves exactly that package: sitewise binary physical responses induce an amplitude-linear $\Pi$-tensor-product response, act sitewise on pure tensors, and inherit density-only collapse on each local channel. The present declaration is the named Fork C handoff surface that integration certificates consume, rather than a new analytic argument.
Related geometry (hinge deficit $2\pi-\sum\theta$, Schläfli data) and gap-derivation constants appear among module dependencies for the broader master-theorem stack, but they are not used in this particular proof term.
proof idea
One-line term proof: the goal is definitionally the Track 2.C many-body one-statement, so the proof is just that theorem applied as a term. No extra tactics, no new hypotheses, and no rewriting beyond the endpoint alias.
why it matters
This is the Fork C receipt that Track 7 integration actually wires in. Downstream, the full A/B/C/D/E/F integration one-statement conjoins it with the Schläfli stationarity reduction, physical residual/Bianchi interface, Page-capacity tick layer, $w(z)$ falsifier bands, falsifier-sensitivity package, and the structural master certificate, while deliberately refusing to assert the fully unconditional discovery theorem. The shorter A/C/F integration receipt and the forkHandoffIntegrationCert instance both record it as the many-body field. The unconditional master-theorem lane also uses it inside the canonical amplitude-linear many-body proposition.
In framework terms it closes the many-body channel lift needed before gravity can treat multi-site recognition ledgers as amplitude-linear objects, consistent with the eight-tick classical signal side of the channel. It does not by itself finish Track 1 displacement-class leaves; the module doc keeps those as the next dependency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.