isAmplitudeLinear_iff_arisesFromSubstrateAccess
plain-language theorem explainer
Amplitude-linear channel responses on the eight-tick signal space are exactly those induced by some ℂ-linear joint operator via substrate access. Anyone citing the unconditional Track 2.C closure or the density-only no-go will use this biconditional. The proof is a two-line constructor: reverse direction is the universal-witness construction already proved in-module; forward direction reuses the Session 124 access-implies-linearity lemma.
Claim. For every channel response $R_C : \mathrm{Signal}_8 \to \mathrm{Signal}_8$, $R_C$ is amplitude-linear if and only if there exists a $\mathbb{C}$-linear operator $R_J$ on the joint substrate such that $R_C$ arises from substrate access of $R_J$ (prepare a matter probe, apply $R_J$ once, read a calibrated channel coordinate).
background
Track 2.C studies operational recognition observables on the joint substrate: maps $R_C$ from the eight-tick signal space $\mathrm{Signal}_8$ into itself. Amplitude-linearity means $R_C$ is induced by a $\mathbb{C}$-linear map on that finite-dimensional register (the substrate-semantic minimum any operational channel must satisfy).
Substrate access is the named principle from Session 124: $R_C$ arises from access of a joint operator $R_J$ when one prepares a matter probe state, applies $R_J$ once on $\mathrm{JointSubstrate}$, and reads a channel coordinate with nonzero calibration. Earlier sessions retired bare amplitude-linear forcing first to a factor-product hypothesis, then to per-section readout, then to this locality/measurement-access principle.
This module closes that thread by showing the access principle is forced by substrate semantics itself. The reverse half uses a universal witness: for amplitude-linear $R_C$ with linear witness $L$, the joint operator $\mathrm{id}\otimes L$ under the canonical probe $(\psi_0=1, i_0=0, \chi=1)$ recovers $R_C$.
proof idea
Term-mode constructor on the biconditional.
Left-to-right (amplitude-linear implies exists access): apply the in-module lemma arisesFromSubstrateAccess_of_isAmplitudeLinear, which builds the universal witness $\mathrm{id}\otimes L$ on the joint substrate and checks the canonical recognition probe access.
Right-to-left (access implies amplitude-linear): introduce the existential witness $R_J$ and the access hypothesis, then apply isAmplitudeLinear_channel_of_arisesFromSubstrateAccess from Session 124, which already shows any channel recovered by substrate access is amplitude-linear.
No new algebra; pure packaging of the two directed lemmas into an iff.
why it matters
This is the characterisation step that makes substrate access non-load-bearing on Track 2.C. Downstream, substrateSemanticsUnconditionalCert records it as the characterisation field, and unconditional_substrate_semantics_one_statement packages the full Session 125 one-statement: access is equivalent to amplitude-linearity, so the density-only no-go holds with no separate access hypothesis.
In the Recognition framework this sits in the gravity/quantum-channel layer above the eight-tick octave (T7): operational channel observables on the finite recognition register must be amplitude-linear, and that property alone forces the substrate-access form. The module status is full theorem (zero sorry, zero RS-internal axiom), closing the Sessions 85–124 hypothesis retirement chain.
Parent consumers only need the iff; they no longer thread an independent access assumption into density-only collapse or the unconditional cert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.