sectionReadout_of_arisesFromSubstrateAccess
plain-language theorem explainer
If a channel response arises from substrate measurement-access on the joint matter-channel ledger, then it is automatically a nonzero matter-section readout of the joint linear operator. Session 113 cites this as the first link: substrate locality is the axiom, section readout follows. The proof unpacks the access witness and rebuilds the readout structure; the functional equation is the induced-channel identity.
Claim. Let $R_J$ be a $\mathbb{C}$-linear operator on the joint substrate $\mathrm{Signal}_8 \otimes_{\mathbb{C}} \mathrm{Signal}_8$, and let $R_C : \mathrm{Signal}_8 \to \mathrm{Signal}_8$ be a channel response. If $R_C$ arises from substrate access of $R_J$ (there exist access data such that $R_C$ equals the induced channel of those data), then there exists a nonzero matter-section readout of $R_J$ recovering $R_C$.
background
Gravity Track 2.C closes the gap left after Session 111. That session showed: a nonzero matter-section readout of a linear joint operator forces the channel to be amplitude-linear, without needing pure-tensor factorization. What remained was the operational claim that the physical channel is obtained by such a readout.
The joint substrate is $\mathrm{Signal}8 \otimes{\mathbb{C}} \mathrm{Signal}8$ (matter ledger times channel ledger). Substrate access data fix a matter reference $\psi_0$, a channel coordinate $i_0$, and a nonzero calibration $\chi$. The induced channel is $R_C\varphi = \chi^{-1}\cdot\mathrm{extractSecond}{i_0}(R_J(\mathrm{insertFirst},\psi_0,\varphi))$. A channel arises from substrate access when it equals some such induced channel.
A joint section readout is the same operational recipe packaged as a structure: inject $\psi_0$, apply $R_J$, extract coordinate $i_0$, divide by $\chi\neq 0$. The module's claim is that under substrate locality this readout law is definitional, not an extra hypothesis.
proof idea
Term-mode construction. Unpack ArisesFromSubstrateAccess to a witness access : SubstrateAccessData and an equality $R_C = \mathrm{inducedChannel},R_J,\mathrm{access}$. Build a JointSectionReadout by copying $\psi_0$, $i_0$, $\chi$, and $\chi\neq 0$ from that access. The remaining field is the readout identity: for each $\varphi$, apply function congruence to the equality, then simplify with the definition of the induced channel to obtain the section-readout formula. No external lemmas beyond that definitional unfold.
why it matters
First arrow in the Session 113 chain:
substrate access $\Rightarrow$ section readout $\Rightarrow$ amplitude-linearity.
Downstream, isAmplitudeLinear_channel_of_arisesFromSubstrateAccess obtains a readout via this theorem and concludes amplitude-linearity with no pure-tensor, operator-product, or global-readout hypothesis. The certificate substrateLocalAccessCert packages the implication, and substrate_local_access_one_statement quotes it as the first conjunct of the one-statement closure: under substrate measurement-access on $\mathrm{Signal}_8\otimes\mathrm{Signal}_8$, section readout is derived, density-only responses collapse, and the factor-product theorem becomes a corollary. Section readout (Session 111) is retired as an assumption; substrate locality is the substantive axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.