track2D_headline
plain-language theorem explainer
Under any T0–T8-consistent substrate, the gravitational channel response is forced amplitude-linear, and any density-only response collapses to the zero map. Quantum-gravity and channel theorists cite this as the Track 2.D headline no-go against CPTP-classical mediators. The proof is a two-component term pairing the amplitude-linearity forcing lemma with the classical-mediator no-go.
Claim. Let $F$ be a substrate consistent with the T0–T8 forcing chain (matter side the recognition update, joint substrate the binary tensor product, joint operator factorizing on pure tensors). Then the channel response $R_C$ of $F$ is amplitude-linear: it agrees with some $\mathbb{C}$-linear map on the eight-tick signal space. Moreover, if $R_C$ is density-only, then $R_C\varphi = 0$ for every eight-tick signal $\varphi$.
background
Track 2.D of the quantum-gravity master plan asks whether a nontrivial CPTP-classical (density-only) gravitational channel can live on a substrate forced by T0–T8. The forcing chain pins the matter side to the recognition substrate Signal8 with the cyclic-shift update (T7 eight-tick octave, T8 spatial dimension $D=3$, T6 $\varphi$-self-similarity).
A T0–T8-consistent substrate is exactly a recognition-coupled factorizable joint substrate: matter side is the recognition update, joint state space is the binary tensor product, and the joint operator factorizes on pure tensors. Amplitude-linearity means the channel response agrees with some $\mathbb{C}$-linear map, so it preserves coherent superpositions of ledger states. Density-only means the response depends only on the classical density, the structural signature of a CPTP-classical mediator.
Upstream, Track 2.C already shows that on any such factorizable recognition-coupled substrate the channel cannot be both nontrivial and density-only. The present module lifts that structural no-go onto the T0–T8-forced substrate class.
proof idea
Term-mode pair constructor. The first conjunct is exactly channel_forced_amplitude_linear_under_T0T8 F, which forces amplitude-linearity of $R_C$ on any T0–T8-consistent substrate. The second conjunct is the lambda fun hDen φ => no_classical_mediator_under_T0T8 F hDen φ, which applies the core no-go: under density-only, every signal is sent to zero. No further rewriting; the headline is the conjunction of those two prior results.
why it matters
This is the reviewer-facing Track 2.D headline: under T0–T8, the gravitational channel is amplitude-linear and cannot be a nontrivial classical mediator. It feeds the master certificate noClassicalMediatorCert, which packages the density-only collapse, the nonexistence of a nontrivial classical mediator on any T0–T8 substrate, and the amplitude-linearity forcing into one cert object.
Framework landmarks in play are the T0–T8 forcing chain (especially T7 eight-tick discreteness and T8 with $D=3$) and the Track 2.C binary-tensor factor-product axiom. The module doc uses this to answer the Bohmian / Diósi–Penrose objection: those substrates violate at least one of T0–T8, so they are not counterexamples inside the forced class. Partial closure only: substrate-internal no-go, not a full dynamical quantum-gravity theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.