T0T8ConsistentSubstrate
plain-language theorem explainer
A T0–T8-consistent substrate is the recognition-coupled factorizable joint substrate: matter evolves by the recognition update, the joint space is a binary tensor product, and the joint operator factorizes on pure tensors. Track 2.D gravity theorems cite this type as the ambient hypothesis for the no-classical-mediator and amplitude-linear channel results. The declaration is a one-line type alias with no proof content.
Claim. A T0–T8-consistent substrate is a recognition-coupled factorizable joint substrate: the matter-side operator equals the recognition update (cyclic shift on the eight-tick carrier), the joint space is the binary tensor product, and the joint operator factorizes on pure tensors.
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 the T0–T8 chain. The module status is structural theorem: zero sorry, zero RS-internal axiom.
Upstream, a factorizable joint substrate has a binary tensor-product joint space and a joint operator that splits on pure tensors. Recognition-coupled factorization strengthens that by fixing the matter factor to the recognition update: single-site Schrödinger linearity under T0–T8 forces the matter side to be the cyclic shift on the eight-tick carrier (T7 period $2^3$, T8 spatial dimension $D=3$, T6 $\varphi$-self-similarity).
The present abbreviation names exactly that recognition-coupled structure as the T0–T8-consistent substrate. Downstream no-go statements quantify over this type rather than over an open-ended class of classical mediators.
proof idea
One-line type alias: the name is defined to be identical to the upstream structure of recognition-coupled factorization (factorizable joint substrate plus the equality of the matter operator with the recognition update). No tactics, no lemmas, no proof obligations.
why it matters
This type is the ambient hypothesis for the Track 2.D headline. Downstream, no_classical_mediator_under_T0T8 states that any density-only channel response on such a substrate collapses to the zero map; channel_forced_amplitude_linear_under_T0T8 is the positive complement (the channel must be amplitude-linear). Together they feed no_classical_mediator_one_statement and the master certificate packing both clauses.
The BMV falsifier band reuses the same type to assert uniqueness of the RS amplitude channel under T0–T8. Framework landmarks in play are the forcing chain T0–T8 (especially T6 $\varphi$, T7 eight-tick octave, T8 $D=3$) and the Track 2.C factorization hypothesis. The definition also answers the reviewer objection that Bohmian or Diósi–Penrose substrates sit outside RS: under T0–T8 the substrate is forced, so those alternatives violate at least one forcing step rather than merely choosing a different channel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.