inducedChannel_apply
plain-language theorem explainer
Unfolds the induced channel of a substrate access: prepare fixed matter probe ψ₀, apply the joint operator R_J, extract channel coordinate i₀, and rescale by χ⁻¹. Anyone working the measurement-access principle or section-readout chain cites this equality. The proof is pure definitional reflexivity (rfl), so simp can fire it.
Claim. Let $R_J$ be a $\mathbb{C}$-linear operator on the joint substrate $\mathrm{Signal}_8 \otimes \mathrm{Signal}_8$, and let access data consist of a matter probe $\psi_0$, a channel coordinate $i_0 \in \{0,\ldots,7\}$, and a nonzero calibration $\chi \in \mathbb{C}$. For every channel signal $\varphi$, the induced channel satisfies $$R_C(\varphi) = \chi^{-1}\,\mathrm{extract}_{i_0}\bigl(R_J(\psi_0 \otimes \varphi)\bigr).$$
background
Gravity Track 2.C closes the gap left after Session 111: section readout was still an assumption on the physical channel. The module replaces that assumption by substrate locality / measurement-access. Operational channels on the joint ledger are harvested by a single recognition probe.
The joint substrate is Signal8 ⊗[ℂ] Signal8 (matter factor first, channel factor second). insertFirst ψ is the linear map φ ↦ ψ ⊗ φ. extractSecond i pulls the second factor after evaluating the first factor at coordinate i. Substrate access data packages a matter probe ψ₀, a readout index i₀, and a nonzero calibration χ.
The induced channel is defined exactly by that probe recipe: χ⁻¹ times extractSecond i₀ of R_J applied to insertFirst ψ₀ φ. This theorem is the pointwise unfolding of that definition.
proof idea
One-line definitional proof: rfl. The right-hand side is literally the body of inducedChannel, so the equality holds by reduction. Marked @[simp] so downstream rewrites can open the induced channel without manual unfolding.
why it matters
This is the computational face of the substrate-access principle that Session 113 installs. Once the induced channel is known pointwise, the next lemma (inducedChannel_isSectionReadout) shows it is automatically a JointSectionReadout of R_J, with no extra hypothesis. That feeds the Session 111 chain: section readout forces amplitude-linearity of the operational channel, and pure-tensor factorization is no longer required as a separate assumption.
In the module implication ladder, SubstrateAccessData → JointSectionReadout → IsAmplitudeLinear. The present equality is the definitional hinge that makes the first arrow hold by construction rather than by postulate. It sits inside the gravity quantum-channel track that retires structural hypotheses from the master theorem list; no direct T0–T8 landmark is invoked here, only the joint-ledger measurement model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.