unconditional_substrate_semantics_one_statement
plain-language theorem explainer
Amplitude-linearity of a gravitational channel response on Signal8 is equivalent to arising from substrate access of some joint linear operator. Every amplitude-linear density-only response vanishes, so no nontrivial such channel exists. The universal witness id⊗L under canonical probe access recovers every amplitude-linear map as an induced channel. Track 2.C gravity workers cite this as the unconditional substrate-access closure. Proof is a four-conjunct term packaging of prior lemmas.
Claim. The following hold jointly: (i) a map $R_C:\mathrm{Signal}_8\to\mathrm{Signal}_8$ is amplitude-linear iff there exists a $\mathbb{C}$-linear operator $R_J$ on the joint substrate $\mathrm{Signal}_8\otimes_{\mathbb{C}}\mathrm{Signal}_8$ such that $R_C$ arises from substrate access of $R_J$; (ii) every amplitude-linear density-only $R_C$ satisfies $R_C\varphi=0$ for all $\varphi$; (iii) no nontrivial amplitude-linear density-only response exists; (iv) for every $\mathbb{C}$-linear $L$ on $\mathrm{Signal}_8$, the channel induced by the universal substrate-access operator of $L$ under canonical access equals $L$.
background
Gravity Track 2.C studies operational channel responses on the eight-tick ledger Signal8. The joint matter-plus-channel substrate is the binary tensor product $\mathrm{Signal}8\otimes{\mathbb{C}}\mathrm{Signal}_8$. A response is amplitude-linear when it agrees with some $\mathbb{C}$-linear map, hence preserves coherent superpositions. It is density-only when invariant under unit-modulus complex scalings: the structural footprint of a CPTP-classical readout from the density matrix alone.
Substrate access encodes the locality/measurement principle: prepare a matter probe state, apply a joint linear operator once, extract a channel coordinate, and calibrate. The induced channel is that operational recipe. Canonical access uses the constant-1 matter probe, channel coordinate 0, and calibration 1. Sessions 85–124 peeled the Track 2.C no-go down to a named substrate-locality hypothesis; this module shows that hypothesis is forced by substrate semantics, via the universal witness $\mathrm{id}\otimes L$.
proof idea
Term-mode proof: a four-tuple of already-proved sibling results, no new tactics.
- First conjunct is the biconditional equating amplitude-linearity with existence of a joint operator from which the response arises via substrate access.
- Second applies the unconditional vanishing lemma: any amplitude-linear density-only response is identically zero on every input.
- Third is the packaged nonexistence statement: there is no nontrivial amplitude-linear density-only channel response.
- Fourth is the universal-witness identity: the channel induced by the universal substrate-access operator of any linear $L$, under canonical access, equals $L$ itself.
Pure packaging of the Session 125 closure lemmas.
why it matters
Session 125 unconditional closure of the Track 2.C substrate-access thread. The module retires the substrate locality / measurement-access principle itself: every amplitude-linear channel response on Signal8 arises from substrate access of the joint operator $\mathrm{id}\otimes L$ under canonical recognition-probe access. Substrate access therefore characterises the amplitude-linear channels and is no longer a separate load-bearing hypothesis on the chain.
Consequently the density-only no-go holds unconditionally for any amplitude-linear response, with no further substrate-access input. The used-by graph is empty: this is a terminal one-statement packaging for the thread. What remains open, per the doc-comment, is deriving amplitude-linearity itself from T0–T8 substrate semantics for the physical channel response on the joint substrate (the next-session target). Within RS gravity this completes the Sessions 85–124 hypothesis-peeling sequence down to the bare operational minimum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.