isAmplitudeLinear_channel_of_sectionReadout
plain-language theorem explainer
Any channel response recovered as a nonzero matter-section readout of a ℂ-linear joint operator on the joint substrate is amplitude-linear. Gravity Track 2.C cites this to retire the global pure-tensor factorization hypothesis. The proof exhibits the witnessing linear map as the scaled composition extract ∘ R_J ∘ insert and checks it against the readout equation.
Claim. Let $R_J : \mathrm{JointSubstrate} \to_{\mathbb{C}} \mathrm{JointSubstrate}$ be $\mathbb{C}$-linear and $R_C : \mathrm{Signal}_8 \to \mathrm{Signal}_8$. If $R_C$ is a nonzero matter-section readout of $R_J$ (fixed matter reference $\psi_0$, coordinate $i_0$, scalar $\chi \neq 0$ with $R_C(\varphi) = \chi^{-1}\cdot \mathrm{extract}_{i_0}(R_J(\psi_0 \otimes \varphi))$ for all $\varphi$), then $R_C$ is amplitude-linear: there exists a $\mathbb{C}$-linear map $L$ with $R_C(\varphi) = L(\varphi)$ for all $\varphi$.
background
Track 2.C of the gravity quantum-channel development forces the gravitational channel response on the eight-tick signal space Signal8 to be amplitude-linear, meaning it agrees with some ℂ-linear map and therefore preserves coherent superpositions of ledger states. Earlier modules required a global pure-tensor factorization of the joint operator $R_J$ on every pure tensor. That hypothesis is stronger than needed operationally.
A nonzero matter-section readout recovers $R_C$ from a single linear slice of $R_J$: inject a fixed matter reference $\psi_0$ into the first tensor factor, apply $R_J$, extract the channel factor at coordinate $i_0 \in \mathrm{Fin},8$, and rescale by a nonzero $\chi$. The joint operator may still mix matter and channel sectors off that section. The structure JointSectionReadout packages exactly those data and the readout identity.
Upstream, IsAmplitudeLinear R is the existence statement $\exists L$ linear with $R\psi = L\psi$. The maps insertFirst and extractSecond are the pure-tensor insertion and coordinate extraction used to form the slice; their composition with $R_J$ is automatically linear.
proof idea
Term-mode existence proof for IsAmplitudeLinear. Build the witnessing linear map explicitly as
$$L := \chi^{-1}\bullet\bigl((\mathrm{extractSecond},i_0)\circ R_J\circ(\mathrm{insertFirst},\psi_0)\bigr),$$
using the fields of the section-readout hypothesis. Because each of insert, $R_J$, and extract is ℂ-linear, the composite (and its scalar multiple) is linear. For an arbitrary channel state $\varphi$, unfold smul_apply and two comp_apply steps; the resulting expression is exactly the readout identity, so $R_C\varphi = L\varphi$.
why it matters
This is the main structural theorem of the section-readout module: the first direct retirement of full pure-tensor factorization in Track 2.C. Downstream it feeds the density-only collapse (channel_eq_zero_of_density_only_of_sectionReadout), the recognition-section specialization, the recovery of the old pure-tensor forcing theorem as a corollary, the bundled sectionReadoutForcingCert, and the one-shot Track 2.C statement factor_product_retirement_one_statement. Substrate-local access later reduces to the same lemma via a derived section readout.
In the Recognition framework the eight-tick octave (T7) supplies the Signal8 carrier; amplitude-linearity is the coherence requirement that keeps gravitational channel updates compatible with ledger superpositions. Closing the factorization gap means the forcing chain no longer depends on an operationally unmotivated global product structure on the joint substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.