NoClassicalMediatorCert
plain-language theorem explainer
Certificate bundle packaging Track 2.D's substrate-internal no-go: under any T0–T8-consistent substrate, a gravitational channel response cannot be a nontrivial density-only (CPTP-classical) map, and is forced to be amplitude-linear. Gravity and quantum-channel auditors cite it as the single inhabited witness that classical mediators are ruled out once the forcing chain fixes the substrate. The structure itself is pure packaging; the fields are filled by the module's core no-go lemmas.
Claim. A certificate recording five facts about T0–T8-consistent substrates (matter side the recognition update, joint operator factorizing on pure tensors): (i) every density-only channel response is identically zero on eight-tick signals; (ii) no such substrate admits a nontrivial density-only response; (iii) every channel response is amplitude-linear (agrees with a $\mathbb{C}$-linear map); (iv) the conjunction of (iii) with the density-only collapse; (v) the class of T0–T8-consistent substrates is nonempty.
background
Track 2.D of the quantum-gravity plan asks whether a classical (density-only) gravitational mediator can sit on a substrate already forced by the T0–T8 chain. The module answers with a substrate-internal no-go: once the matter side is the recognition update and the joint operator factorizes on pure tensors, nontrivial CPTP-classical responses are impossible.
A density-only response is invariant under unit-modulus complex rescaling of the signal; that is the structural footprint of a readout computed from the density matrix alone. An amplitude-linear response agrees with some $\mathbb{C}$-linear map and therefore preserves coherent superpositions of ledger states. The T0–T8-consistent substrate abbreviates a recognition-coupled factorization: eight-tick discreteness (T7), $D=3$ (T8), and $\varphi$-self-similarity (T6) fix the matter side to Signal8 with the cyclic recognition update.
Upstream, Track 2.C already showed that on any recognition-coupled factorizable joint substrate the channel cannot be both nontrivial and density-only. The present certificate simply packages that no-go under the T0–T8 substrate class, together with the positive forcing that the channel is amplitude-linear.
proof idea
This declaration is a structure (certificate type), not a proved theorem: it has no proof body. Its five fields are Prop-valued slots that a later inhabitant must fill. The companion definition noClassicalMediatorCert supplies those fields by direct application of the module lemmas no_classical_mediator_under_T0T8, no_T0T8_substrate_with_nontrivial_classical_mediator, channel_forced_amplitude_linear_under_T0T8, the composite headline, and T0T8ConsistentSubstrate_inhabited. No new algebra occurs at the structure level; it is pure packaging of already-proved no-go and forcing statements.
why it matters
This is the master certificate for Track 2.D partial closure (module status: structural theorem, zero sorry). It feeds noClassicalMediatorCert and the inhabitation theorem noClassicalMediatorCert_inhabited, which in turn support the one-statement Track 2.D headline: under T0–T8 the gravitational channel is amplitude-linear and any density-only response collapses to zero.
Framework landmarks: T7 (eight-tick octave) and T8 ($D=3$) force the matter side onto the recognition substrate; T6 supplies $\varphi$-self-similarity. The certificate answers the reviewer objection that Bohmian or Diósi–Penrose substrates evade RS: both violate at least one of T0–T8 (continuous trajectories vs T2 discreteness; stochastic collapse vs T1 ledger linearity), so they are not T0–T8-consistent substrates at all. Classical mediators are therefore ruled out inside the forced substrate, not merely by external modeling choice.
What remains open is full Track 2 closure beyond the substrate-internal no-go (external channel axioms, quantitative decoherence bounds).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.