inducedChannel_isSectionReadout
plain-language theorem explainer
Any channel induced by substrate measurement-access data is automatically a joint section readout of the joint linear operator. Gravity-track authors cite this when retiring the section-readout hypothesis in favour of the substrate-locality principle. The construction simply repackages the access fields and discharges the readout identity by reflexivity.
Claim. Let $R_J$ be a $\mathbb{C}$-linear operator on the joint substrate and let access data consist of a matter probe $\psi_0$, a channel coordinate $i_0\in\{0,\ldots,7\}$, and a calibration $\chi\neq 0$. The induced channel $R_C\varphi=\chi^{-1}\cdot\mathrm{extract}_{i_0}(R_J(\mathrm{insert}(\psi_0,\varphi)))$ is a joint section readout of $R_J$ with those same data.
background
Track 2.C treats operational channel observables on the joint substrate $\mathrm{Signal}_8\otimes\mathrm{Signal}_8$. Substrate measurement-access data are a matter probe state $\psi_0$, a channel-side readout index $i_0$, and a nonzero calibration scalar $\chi$. The induced channel is the operational recipe: insert $\psi_0$ in the first factor, apply the joint operator $R_J$, extract the $i_0$-coordinate of the second factor, and rescale by $\chi^{-1}$.
A joint section readout is the Session-111 structure asserting that a channel response equals that same prepare-apply-extract-normalise formula for some fixed probe, index, and calibration. The module's point is that under substrate locality this formula is the definition of how the physical channel is harvested from $R_J$, so section readout is no longer an extra assumption.
The implication chain in the module doc is: substrate access data imply joint section readout, which (by Session 111) forces the channel to be amplitude-linear.
proof idea
Definitional construction of the joint-section-readout structure, not a tactic proof. The probe, index, calibration, and nonzero certificate are taken verbatim from the access data. The readout field is the function that, for every matter state, asserts equality of the channel action with the induced formula; that equality holds by definition of the induced channel, so it is discharged by rfl.
why it matters
Closes the remaining gap after Session 111's section-readout retirement. Session 111 showed: nonzero matter-section readout of a linear joint operator forces amplitude-linearity. The open assumption was that the physical channel is obtained that way. This definition makes section readout the automatic consequence of substrate access, so the locality principle defines the channel rather than postulating a readout law.
Downstream siblings (ArisesFromSubstrateAccess, sectionReadout_of_arisesFromSubstrateAccess, amplitude-linearity and density-only exclusion lemmas) build on this packaging. In the Recognition chain it sits under the gravity quantum-channel track that feeds the master theorem, converting an operational measurement-access principle into the forced amplitude-linear response used for structural gravity claims. No T0–T8 landmark is proved here; the eight-tick register appears only as the ambient $\mathrm{Signal}_8$ factor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.