substrate_local_access_one_statement
plain-language theorem explainer
Under substrate locality (measurement access) on the joint ledger Signal8 ⊗ Signal8, every operational channel is a section readout, hence amplitude-linear; any density-only such channel is identically zero. The canonical cyclic joint operator with the recognition update witnesses the principle non-vacuously. Gravity-channel and quantum-channel workers cite this as the Session-113 one-statement packaging. The proof is a five-component term that assembles the sibling lemmas already proved in the module.
Claim. The following hold simultaneously: (i) if a channel $R_C$ arises from substrate access of a joint linear operator $R_J$ on $\mathrm{Signal}_8 \otimes_{\mathbb{C}} \mathrm{Signal}_8$, then there exists a nonzero matter-section readout recovering $R_C$ from $R_J$; (ii) any such $R_C$ is amplitude-linear; (iii) if in addition $R_C$ is density-only, then $R_C\varphi=0$ for every $\varphi$; (iv) no nontrivial density-only channel arises from substrate access; (v) the canonical cyclic joint operator paired with the recognition update arises from substrate access.
background
Gravity Track 2.C treats the joint matter-plus-channel substrate as the binary tensor product $\mathrm{Signal}8 \otimes{\mathbb{C}} \mathrm{Signal}_8$. A channel response $R_C$ is amplitude-linear when it agrees with some $\mathbb{C}$-linear map (preserving coherent superpositions). It is density-only when it is invariant under unit-modulus phase multiplications, the structural footprint of a CPTP-classical readout from $|\psi\rangle\langle\psi|$.
Session 111 introduced nonzero matter-section readout: inject a fixed matter reference $\psi_0$, apply the joint operator $R_J$, extract a channel coordinate $i_0$, and rescale by $\chi\neq 0$. That forced amplitude-linearity once the physical channel was assumed to be such a readout. The remaining gap was justifying that assumption.
This module replaces it by substrate locality / measurement-access: every operational channel is obtained as a recognition probe (fix $\psi_0$, run $R_J$, read coordinate $i_0$, normalise by $\chi$). Concretely, $R_C$ arises from substrate access of $R_J$ when $R_C$ equals the induced channel for some access data. The canonical cyclic joint operator (tensor product of cyclic shifts) and the recognition update (projector-after-shift) supply a concrete inhabited instance.
proof idea
Term-mode packaging of five already-proved sibling facts as a single conjunction. The first conjunct applies sectionReadout_of_arisesFromSubstrateAccess: substrate access data induce a JointSectionReadout. The second applies isAmplitudeLinear_channel_of_arisesFromSubstrateAccess, chaining access to section readout to amplitude-linearity. The third applies channel_eq_zero_of_density_only_of_arisesFromSubstrateAccess pointwise on every $\varphi$. The fourth is the global non-existence lemma not_exists_nontrivial_density_only_channel_with_substrateAccess. The fifth is the witness canonicalCyclicJointOperator_arisesFromRecognitionProbe. No new algebra is done here; the one-statement is pure assembly.
why it matters
Session 113 one-statement for substrate locality. It sits one level deeper than Session 111: section readout is no longer an assumption but a derived consequence of measurement-access plus joint linearity, and the factor-product theorem (Sessions 85-88) becomes a corollary along the same chain.
In the Recognition gravity track this closes the structural implication
SubstrateAccessData → JointSectionReadout → IsAmplitudeLinear,
with the density-only collapse ruling out classical CPTP-style readouts as nontrivial gravitational channels under the principle. The inhabited witness (canonical cyclic joint operator with recognition update) shows the hypothesis space is nonempty, so the forcing is not vacuous.
No downstream consumers are wired yet (used_by is empty). The doc-comment flags the remaining unconditional step: derive ArisesFromSubstrateAccess itself from the T0-T8 forcing chain, i.e. show every operational recognition observable on the joint substrate must be of induced form. That is substrate semantics and the next session-scale target. The eight-tick Signal8 ledger (T7) is the ambient carrier throughout.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.