physicalChannelAmplitudeLinearCert
plain-language theorem explainer
Packages the unconditional T0-T8 closure of Gravity Track 2.C into one certificate: every physical channel response on the joint substrate is amplitude-linear, density-only responses collapse to zero, the density-only no-go is unconditional, and the canonical cyclic joint dynamics supplies a non-vacuous witness. Gravity-track consumers cite this cert when they need the full package rather than separate lemmas. The body is a pure structure inhabitant wiring six already-proved theorems.
Claim. There is a certificate asserting: (i) every physical channel response $R_C$ arising via substrate access from a $\mathbb{C}$-linear joint dynamics $R_J$ on $\mathrm{Signal}_8\otimes\mathrm{Signal}_8$ is amplitude-linear; (ii) any density-only such $R_C$ is identically zero; (iii) no nontrivial density-only physical channel response exists under T0-T8 substrate semantics; (iv) the canonical T0-T8 joint dynamics with the recognition update inhabits this space non-vacuously, and that update is amplitude-linear and not density-only.
background
Gravity Track 2.C closes the density-only no-go for physical channel responses from T0-T8 substrate semantics alone (zero sorry, no RS-internal axiom). The joint carrier is $\mathrm{JointSubstrate}=\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$, the substrate lift of Schrödinger linearity. Operational channel observables arise by substrate-internal access: prepare a matter probe $\psi_0$, apply $R_J$, extract a channel coordinate $i_0$, and calibrate by a nonzero scalar $\chi$. That composite is the physical channel response $R_C$.
Because $R_C$ is built by composition of $\mathbb{C}$-linear maps on $\mathrm{Signal}_8$, it is amplitude-linear unconditionally. The master structure PhysicalChannelAmplitudeLinearCert records four claims: amplitude-linearity of every physical channel response; collapse of density-only responses to zero; the unconditional no-go (no nontrivial density-only physical channel); and a canonical non-vacuous witness from the cyclic T0-T8 joint operator with the recognition update.
proof idea
Definitional structure inhabitant, not a tactic proof. Each field of the certificate is filled by a named theorem already proved in the module:
- amplitude-linearity field gets the unconditional theorem that every physical channel response is amplitude-linear;
- density-only collapse gets the theorem that any density-only physical channel response is the zero map;
- no-go field gets the theorem that no joint dynamics admits a nontrivial density-only physical channel response;
- canonical witness, canonical amplitude-linearity, and canonical not-density-only get the three theorems showing that the canonical cyclic joint operator with the recognition update is a physical channel response, that this update is amplitude-linear, and that it is not density-only (via nontriviality plus the single-factor dichotomy).
No new reasoning occurs at this site; the cert is pure packaging.
why it matters
This is the single exportable closure object for Track 2.C. Downstream, the many-body certificate reuses it as the binary factor (binary_cert := physicalChannelAmplitudeLinearCert), and an inhabitedness theorem records Nonempty of the cert type so later modules can assume the package without reopening the chain.
Framework landmarks: T7 forces the eight-tick factors on each tensor leg; joint $\mathbb{C}$-linearity is the substrate reading of Schrödinger linearity; substrate-local measurement access forces amplitude-linearity of every physical channel response. Together they retire the last structural hypothesis on the density-only no-go, so the CPTP-classical mediator obstruction is forced by T0-T8 alone. The canonical cyclic witness shows the hypothesis space is not empty: the actual T0-T8 recognition update is a nontrivial amplitude-linear physical channel response and therefore not density-only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.