manyBodyPhysicalChannelAmplitudeLinearCert
plain-language theorem explainer
Packages the many-body Track 2.C certificate: any finite sitewise family of physical channel responses is amplitude-linear on the full channel ledger, acts by pure tensors sitewise, and collapses to zero under density-only hypotheses. Gravity theorists citing the unconditional T0–T8 substrate-semantic closure would reference this bundle. The definition is a pure structure assembly of the binary certificate plus three already-proved many-body lemmas.
Claim. There is a many-body certificate consisting of: (i) the binary physical-channel amplitude-linearity certificate; (ii) for every finite index set $\iota$ and every sitewise family of joint dynamics $R_J(i)$ with physical channel responses $R_C(i)$, the induced macroscopic response on the $\Pi$-tensor-product ledger is amplitude-linear; (iii) on pure tensors the response acts by applying the binary channel map at each site; (iv) if every local response is density-only, then every local response is identically zero.
background
Track 2.C closes amplitude-linearity of physical channel responses from T0–T8 substrate semantics alone (no remaining structural hypothesis). The joint substrate is $\mathrm{Signal}8 \otimes{\mathbb{C}} \mathrm{Signal}_8$ (T7 eight-tick factors with tensor coupling). Joint dynamics is a $\mathbb{C}$-linear endomorphism $R_J$ of that carrier; operational channel observables arise by substrate-internal access (prepare a matter probe, apply $R_J$, extract a channel coordinate, calibrate by a nonzero scalar). Composition of those linear maps forces the physical channel response to be amplitude-linear.
The binary certificate already records that every physical channel response is amplitude-linear, that density-only responses vanish, and that no nontrivial density-only physical response exists. The many-body lift indexes those binary data by a finite type $\iota$ and promotes them to the full $\Pi$-tensor-product channel ledger. Upstream lemmas supply sitewise amplitude-linearity, pure-tensor action, and local density-only collapse (each local density-only physical channel is zero by the binary no-go).
proof idea
One-line structure constructor. The binary field is the existing binary Track 2.C certificate. The many-body amplitude-linearity field is discharged by applying the theorem that a sitewise family of physical channel responses induces an amplitude-linear response on the full finite $\Pi$-tensor-product ledger. The pure-tensor field is the theorem that on definite macroscopic configurations the many-body response acts by the binary map at each site. The local density-only field is the sitewise collapse theorem: if every local response is density-only, each vanishes by the binary no-go. No new reasoning; pure packaging.
why it matters
This is the many-body packaging of Gravity Track 2.C's unconditional closure. Downstream, the inhabited theorem cites it to prove the certificate type is nonempty, and the module's many-body one-statement records that the binary physical-channel closure lifts to any finite many-body channel ledger. In the Recognition framework it sits on the T0–T8 forcing chain (especially T7's eight-tick octave that fixes the $\mathrm{Signal}_8$ factors) and on the substrate-semantic reading of joint linearity. It supplies the local no-go payload needed by many-body integrations that would otherwise re-open a density-only loophole at each site. No open sorry remains on this path; the module status is full theorem closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.