ManyBodyPhysicalChannelAmplitudeLinearCert
plain-language theorem explainer
Certificate packaging the many-body lift of Gravity Track 2.C: sitewise physical channel responses on a finite index set induce an amplitude-linear macroscopic map on the Pi-tensor channel ledger, pure tensors evolve factorwise, and density-only responses collapse sitewise from the binary no-go. Master-theorem handoffs and the unconditional D3 many-body proposition cite Nonempty of this bundle. The declaration is a structure definition; inhabitance is discharged by a separate constructor.
Claim. A many-body Track 2.C certificate is a record of four facts: (1) a binary physical-channel amplitude-linearity certificate; (2) for every finite index set $\iota$ and families $R_J(i):J\to_{\mathbb{C}} J$, $R_C(i):S\to S$ with each $R_C(i)$ a physical channel response of $R_J(i)$ (substrate-access of joint dynamics on $J=S\otimes_{\mathbb{C}} S$), the induced many-body response is amplitude-linear, i.e. agrees with some $\mathbb{C}$-linear endomorphism of the macroscopic channel ledger; (3) on pure tensors, the many-body response acts sitewise by $R_C(i)$; (4) if every $R_C(i)$ is density-only then each $R_C(i)$ vanishes identically.
background
Track 2.C closes amplitude-linearity of physical channel responses from T0–T8 substrate semantics alone (module status: theorem, zero sorry). The joint substrate is $J = S \otimes_{\mathbb{C}} S$ with $S = \mathrm{Signal8}$ forced by the eight-tick period (T7) on each factor. Joint dynamics is a $\mathbb{C}$-linear endomorphism $R_J$ of $J$. A map $R_C:S\to S$ is a physical channel response of $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. Composition of linear maps then forces $R_C$ amplitude-linear.
Density-only means phase invariance: $R(c\cdot\psi)=R(\psi)$ whenever $|c|=1$, the footprint of a CPTP-classical density-matrix readout. The binary master certificate already records unconditional amplitude-linearity, density-only collapse to zero, and non-vacuous canonical T0–T8 joint dynamics. Many-body amplitude-linearity means the macroscopic response on the finite Pi-tensor channel ledger agrees with some $\mathbb{C}$-linear endomorphism of that ledger.
proof idea
No proof body: this is a structure (certificate interface), not a theorem. The four fields are pure packaging. Field one embeds the binary Track 2.C master certificate. Field two asserts the many-body amplitude-linearity statement for arbitrary finite site sets under the sitewise physical-response hypothesis. Field three records pure-tensor factorwise evolution under the induced many-body response. Field four lifts the binary density-only collapse sitewise. Inhabitance is supplied downstream by a noncomputable constructor that fills the fields from the binary cert and the many-body amplitude-linearity lemma, plus a one-line Nonempty theorem wrapping that constructor.
why it matters
This is the many-body endpoint of Track 2.C that master-theorem integration actually consumes. Fork handoff certificates require Nonempty of this structure alongside the Track 2 many-body endpoint; the A/B/C/D/E/F and A/C/F one-statements both list it explicitly so Track 7 can cite the Pi-tensor lift rather than only the binary physical-channel cert. The unconditional master D3 proposition is strengthened to demand both the binary and this many-body certificate, plus the Track 2 many-body endpoint.
Framework landmarks: T7 eight-tick octave fixes Signal8; joint substrate tensor structure and joint linearity (Schrödinger-derived) force amplitude-linearity of every physical channel response, discharging the last structural hypothesis on the density-only no-go. The many-body lift extends that closure from one site to any finite ledger, which is what gravity-side residual and stationarity handoffs need when channels couple across cells.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.