ArisesFromSubstrateAccess
plain-language theorem explainer
A channel map on the eight-tick ledger arises from substrate access of a joint linear operator when it equals the induced readout for some probe state, coordinate, and nonzero calibration. Gravity-track authors cite this as the operational content of substrate locality. The body is a one-line existential over access data equating the channel to the induced formula.
Claim. For a $\mathbb{C}$-linear joint operator $R_J$ on $\mathrm{Signal}_8 \otimes_{\mathbb{C}} \mathrm{Signal}_8$ and a channel map $R_C : \mathrm{Signal}_8 \to \mathrm{Signal}_8$, we say $R_C$ arises from substrate access of $R_J$ when there exist a matter probe $\psi_0$, a channel coordinate $i_0 \in \{0,\ldots,7\}$, and a calibration $\chi \neq 0$ such that $R_C\varphi = \chi^{-1}\cdot \pi_{i_0}^{(2)}\bigl(R_J(\psi_0 \otimes \varphi)\bigr)$ for all $\varphi$.
background
Track 2.C closes the gap left after Session 111: amplitude-linearity was forced for nonzero matter-section readouts of a linear joint operator, but the physical channel still had to be assumed to be such a readout. This module replaces that assumption by substrate locality / measurement-access: every operational channel observable on the joint substrate is harvested by one recognition probe.
The joint substrate is the binary tensor product $\mathrm{Signal}8 \otimes{\mathbb{C}} \mathrm{Signal}_8$ (matter ledger times channel ledger). Access data package a matter reference $\psi_0$, a channel-side coordinate $i_0 \in \mathrm{Fin},8$, and a nonzero calibration $\chi$. The induced channel is the operational recipe $R_C\varphi = \chi^{-1}\cdot(\mathrm{extractSecond},i_0)(R_J(\mathrm{insertFirst},\psi_0,\varphi))$.
Under that recipe the channel is automatically a joint section readout, so section readout becomes definitional rather than axiomatic. The implication chain is: access data $\Rightarrow$ section readout $\Rightarrow$ amplitude-linear channel response.
proof idea
Definitional, not a proof. The proposition is the existential $\exists,\mathrm{access}:\mathrm{SubstrateAccessData},; R_C = \mathrm{inducedChannel},R_J,\mathrm{access}$. Unfolding inducedChannel recovers the probe-insert / joint-apply / coordinate-extract / calibrate formula. Downstream lemmas discharge the existential by exhibiting concrete access data (e.g. from pure-tensor factorization with a nontrivial matter coordinate, or from the canonical recognition probe).
why it matters
This is the Lean encoding of the substrate locality principle that Session 113 uses to retire the section-readout hypothesis. Downstream, PhysicalChannelResponseOf is literally an abbreviation for this proposition, so every T0–T8 physical-channel certificate is stated in these terms. It feeds isAmplitudeLinear_channel_of_arisesFromSubstrateAccess and channel_eq_zero_of_density_only_of_arisesFromSubstrateAccess, which close the chain to amplitude-linearity and rule out nontrivial density-only channels.
Parent uniqueness results in the BMV falsifier band (rs_amplitude_channel_unique) compose this with T0–T8-consistent substrate hypotheses to assert that the RS gravitational channel is the amplitude-linear one. The eight-tick octave (T7) appears as the $\mathrm{Fin},8$ readout coordinate; the joint tensor product is the matter-plus-channel ledger forced by the recognition-coupled factorization. Inhabitation is non-vacuous via canonicalCyclicJointOperator_arisesFromRecognitionProbe.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.