PhysicalChannelAmplitudeLinearCert
plain-language theorem explainer
Master certificate bundling the unconditional Track 2.C closure: every physical channel response arising from T0–T8 joint-substrate access is amplitude-linear; density-only such responses vanish; a nontrivial density-only response is impossible; and the canonical joint dynamics with the recognition update witnesses the space non-vacuously. Gravity master-theorem and many-body lifts cite it. As a structure it is pure packaging; the inhabiting instance wires the proved lemmas.
Claim. A certificate consisting of: (i) every map $R_C:\mathrm{Signal}_8\to\mathrm{Signal}_8$ that is the physical channel response of a $\mathbb{C}$-linear joint dynamics $R_J$ on $\mathrm{JointSubstrate}=\mathrm{Signal}_8\otimes\mathrm{Signal}_8$ is amplitude-linear; (ii) if such an $R_C$ is density-only then $R_C\equiv 0$; (iii) there is no nontrivial density-only physical channel response; (iv) the canonical T0–T8 joint dynamics has the recognition update as physical channel response; (v) that update is amplitude-linear and not density-only.
background
Track 2.C closes the gravity quantum-channel story under pure T0–T8 substrate semantics (module status: theorem, zero sorry). The joint carrier is $\mathrm{JointSubstrate}=\mathrm{Signal}8\otimes{\mathbb{C}}\mathrm{Signal}_8$, forced by the eight-tick octave (T7) on each factor and the tensor product for matter–channel coupling. Joint dynamics are $\mathbb{C}$-linear endomorphisms $R_J$, the joint lift of Schrödinger linearity.
A function $R_C$ is a physical channel response of $R_J$ when it arises by substrate access: prepare a matter probe $\psi_0$, apply $R_J$, extract a channel coordinate $i_0$, and rescale by a nonzero calibration $\chi$. Explicitly, $R_C\varphi=\chi^{-1}\cdot\mathrm{extractSecond}_{i_0}(R_J(\mathrm{insertFirst},\psi_0,\varphi))$. That composite is a $\mathbb{C}$-linear endomorphism of $\mathrm{Signal}_8$, hence amplitude-linear by construction.
The recognition update (projector-after-shift on structured sectors) is the concrete single-site channel map; the canonical T0–T8 joint dynamics lifts the cyclic shift independently on each tensor factor. Density-only maps are those that depend only on occupation densities, not full amplitudes; the certificate records that no nontrivial such map can be a physical channel response.
proof idea
This declaration is a structure (certificate type), not a proved theorem. It has no proof body: it only names the six propositions that constitute Track 2.C closure.
The inhabiting instance physicalChannelAmplitudeLinearCert fills the fields by direct assignment from sibling lemmas: physicalChannelResponse_isAmplitudeLinear (every substrate-access response is amplitude-linear by composition of linear maps), density_only_physicalChannelResponse_eq_zero and not_exists_nontrivial_density_only_physicalChannelResponse (collapse and no-go), plus the canonical witness lemmas tying canonicalT0T8JointDynamics to recognitionUpdate and verifying that update is amplitude-linear and not density-only. Downstream Nonempty is then immediate from that instance.
why it matters
This is the master packaging of unconditional Track 2.C: amplitude-linearity of the physical channel is forced by T0–T8 alone, retiring the last structural hypothesis that earlier sessions left on the density-only no-go. Framework landmarks in play are T7 (eight-tick / $\mathrm{Signal}_8$) and the joint linear substrate semantics that lift Schrödinger linearity.
Downstream, ManyBodyPhysicalChannelAmplitudeLinearCert consumes a binary copy of this cert sitewise to lift amplitude-linearity to macroscopic many-body responses. The unconditional gravity master theorem packages nonemptiness of this cert (and its many-body sibling) into canonicalAmplitudeLinearManyBodyProp, strengthening the D3 handoff beyond the binary channel. The inhabited instance and physicalChannelAmplitudeLinearCert_inhabited make the certificate a drop-in hypothesis discharge for those parents.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.