inducedChannel
plain-language theorem explainer
Defines the operational channel harvested from a joint linear operator under substrate locality: fix a matter probe, apply the joint map once, read one channel coordinate, and rescale by a nonzero calibration. Gravity-track arguments cite it as the concrete readout recipe that turns measurement-access data into a map Signal8 → Signal8. The body is a three-line functional definition composing insert, joint action, extract, and scalar inverse.
Claim. Given a $\mathbb{C}$-linear joint operator $R_J$ on $\mathrm{Signal}_8 \otimes_{\mathbb{C}} \mathrm{Signal}_8$ and substrate access data $(\psi_0, i_0, \chi)$ with $\chi \neq 0$, the induced channel is the map $R_C : \mathrm{Signal}_8 \to \mathrm{Signal}_8$ defined by $R_C(\varphi) = \chi^{-1} \cdot \mathrm{extract}_{i_0}\bigl(R_J(\psi_0 \otimes \varphi)\bigr)$.
background
Gravity Track 2.C closes the gap left after section-readout retirement: Session 111 showed that a nonzero matter-section readout of a linear joint operator is forced amplitude-linear, but still assumed the physical channel is obtained that way. This module replaces that assumption by substrate locality / measurement-access: every operational channel observable on the joint substrate is a recognition probe.
The joint substrate is $\mathrm{Signal}8 \otimes{\mathbb{C}} \mathrm{Signal}_8$ (matter ledger $\otimes$ channel ledger). insertFirst embeds a fixed matter state as $\varphi \mapsto \psi \otimes \varphi$. extractSecond pulls the second factor scaled by the $i$-th coordinate of the first. Substrate access data packages a matter probe $\psi_0$, a channel readout index $i_0 \in \mathrm{Fin},8$, and a nonzero calibration $\chi$.
Under the principle, the operational channel is defined by preparing $\psi_0$, running $R_J$ once, reading coordinate $i_0$, and normalising by $\chi$. Section readout then becomes a derived property rather than an extra hypothesis.
proof idea
Definitional, not a proof. The map is the composite
$\varphi \mapsto \chi^{-1}\cdot(\mathrm{extractSecond},i_0)\bigl(R_J(\mathrm{insertFirst},\psi_0,\varphi)\bigr)$.
insertFirst is the pure-tensor insertion linear map; extractSecond is the coordinate-scaled second-factor projection; scalar multiplication by $\chi^{-1}$ is the calibration step. No lemmas are applied beyond those constructors.
why it matters
This is the definitional heart of the substrate-locality chain in Track 2.C: SubstrateAccessData $\Rightarrow$ JointSectionReadout $\Rightarrow$ IsAmplitudeLinear.
ArisesFromSubstrateAccess is literally existence of access data with $R_C$ equal to this induced map. Downstream, inducedChannel_isSectionReadout shows every such channel is automatically a joint section readout; sectionReadout_of_arisesFromSubstrateAccess is the first link of the new derivation; pure-tensor factorization is shown to imply substrate access when the matter side is nontrivial at some coordinate. Physical-channel linear extension is definitionally equal to this induced channel. Unconditional substrate-semantics certificates also route through it.
In RS terms it encodes the recognition-probe measurement recipe on the eight-tick ledger pair: one joint update, one channel coordinate, one calibration. It retires section readout as an assumption and makes amplitude-linearity of the operational channel a consequence of substrate locality alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.