isAmplitudeLinear_channel_of_arisesFromSubstrateAccess
plain-language theorem explainer
Substrate locality alone forces any operational channel harvested from a linear joint operator to be amplitude-linear. Track 2.C and BMV uniqueness arguments cite this as the middle link of the access-to-linearity chain. The proof obtains a section-readout witness from the access hypothesis and hands it to the Session 111 section-readout linearity theorem.
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$ (i.e., equals the induced channel for some access data: fixed matter reference, one joint application, coordinate extraction, nonzero calibration), then $R_C$ is amplitude-linear: there exists a $\mathbb{C}$-linear map $L$ with $R_C\psi = L\psi$ for every $\psi$.
background
The joint substrate is the binary tensor product $\mathrm{Signal}8 \otimes{\mathbb{C}} \mathrm{Signal}_8$: first factor matter ledger, second factor channel ledger. A response $R$ on $\mathrm{Signal}_8$ is amplitude-linear when it agrees with some $\mathbb{C}$-linear map, so it preserves coherent superpositions of ledger states.
Substrate access encodes the measurement-access principle: every operational channel on the joint substrate is harvested by fixing a matter reference state $\psi_0$, applying the joint operator once, extracting a channel coordinate $i_0$, and normalising by a calibration scalar $\chi \neq 0$. The induced formula is automatically a joint section readout. The proposition "arises from substrate access" asserts existence of such access data with $R_C$ equal to that induced channel.
This module (Gravity Track 2.C) sits after Session 111, which proved that a nonzero matter-section readout of a linear joint operator is forced amplitude-linear. The remaining gap was that the physical channel is operationally a section readout; substrate locality supplies that as a definition rather than an extra hypothesis.
proof idea
Two-step term proof, no tactics beyond obtain/exact. From the access hypothesis, sectionReadout_of_arisesFromSubstrateAccess produces a JointSectionReadout witness (first link of the module chain: access data define an induced channel that is a section readout by construction). Then isAmplitudeLinear_channel_of_sectionReadout (Session 111, imported from AmplitudeLinearForcedSectionReadout) converts that witness into amplitude-linearity of $R_C$.
why it matters
Middle arrow of the Track 2.C chain: substrate access $\Rightarrow$ section readout $\Rightarrow$ amplitude-linear. Downstream, physicalChannelResponse_isAmplitudeLinear is a one-line application of this theorem, giving unconditional T0–T8 substrate-semantic amplitude-linearity for every physical channel response of linear joint dynamics. The package theorems substrate_local_access_one_statement and substrateLocalAccessCert record it as the amplitude-linear-from-access clause; the sibling density-only collapse and the BMV uniqueness statement rs_amplitude_channel_unique both depend on it. SubstrateSemanticsUnconditional uses it for one direction of the iff between amplitude-linearity and substrate access.
Relative to the forcing chain, the result sits on the gravity/quantum-channel side once joint dynamics are already $\mathbb{C}$-linear (substrate-semantic content of the Schrödinger derivation under T0–T8). It retires pure-tensor factorization and global readout as independent assumptions: locality plus joint linearity suffice. Module status is structural closure (0 sorry).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.