isAmplitudeLinear_channel_of_pureTensorFactorization_via_sectionReadout
plain-language theorem explainer
Under pure-tensor factorization of a joint matter-channel operator, a nonzero matter-section sample forces the channel factor to be amplitude-linear (equal to some ℂ-linear map on Signal8). Gravity Track 2.C cites this to recover the older factorization forcing result from the weaker section-readout theorem. The proof is a one-line composition: build a section readout from the factorization, then apply the general section-readout amplitude-linearity lemma.
Claim. Let $R_J$ be a $\mathbb{C}$-linear operator on the joint substrate $\mathrm{Signal}_8 \otimes_{\mathbb{C}} \mathrm{Signal}_8$, and let $R_M,R_C:\mathrm{Signal}_8\to\mathrm{Signal}_8$. If $R_J$ factorizes on pure tensors as the product of $R_M$ and $R_C$, and if there exist a reference matter state $\psi_0$ and coordinate $i_0\in\{0,\ldots,7\}$ with $(R_M\psi_0)_{i_0}\neq 0$, then $R_C$ is amplitude-linear: there exists a $\mathbb{C}$-linear map $L$ with $R_C\psi=L\psi$ for all $\psi$.
background
Track 2.C studies when a gravitational channel response on the eight-tick ledger Signal8 must be amplitude-linear, meaning it coincides with some ℂ-linear endomorphism and therefore preserves coherent superpositions. The joint matter-plus-channel substrate is the binary tensor product JointSubstrate := Signal8 ⊗[ℂ] Signal8. Pure-tensor factorization says the joint operator acts on pure tensors by separate matter and channel maps $R_M$ and $R_C$.
Earlier modules forced amplitude-linearity of $R_C$ from full factorization on every pure tensor. This module weakens that demand: it is enough that the physical channel response arise as a nonzero matter section readout $\varphi \mapsto \chi^{-1}\cdot\mathrm{extractSecond}_{i_0}(R_J(\psi_0\otimes\varphi))$ for fixed matter reference $\psi_0$, slot $i_0$, and nonzero scalar $\chi$. Such a readout is a linear slice of $R_J$, so the recovered channel map is automatically amplitude-linear even if $R_J$ mixes sectors off that section.
The sibling isAmplitudeLinear_channel_of_sectionReadout is the general forcing lemma for any such readout. The present declaration reconnects the older pure-tensor hypothesis to that weaker infrastructure.
proof idea
One-line term proof. First apply sectionReadout_of_pureTensorFactorization to the factorization hypothesis and the nonzero sample $(R_M\psi_0)_{i_0}\neq 0$; that constructs a concrete nonzero section-readout witness for $R_C$ from the pure-tensor data. Then feed that witness into isAmplitudeLinear_channel_of_sectionReadout, which concludes that any channel recovered as a nonzero section readout of a ℂ-linear joint operator is amplitude-linear. No extra algebraic work is done at this site.
why it matters
Closes the compatibility bridge between the old Track 2.C pure-tensor forcing theorem and the newer section-readout formulation. The module's main structural result is section-readout forcing without global factorization; this corollary shows the classical pure-tensor statement is recovered rather than abandoned, so prior citations under the stronger hypothesis remain valid.
In the Recognition framework this sits in the gravity quantum-channel layer that disciplines how ledger updates couple matter and channel sectors on the eight-tick register (T7 octave). Amplitude-linearity is the coherence-preserving constraint needed before channel responses can be treated as linear operators in the macroscopic ledger and Hamiltonian-emergence story. Downstream use is currently empty in the graph; the declaration is a recovery corollary inside the section-readout closure package rather than a new forcing engine. It does not itself touch mass ladders, $\alpha$, or $D=3$, but it stabilizes the operator hypotheses those gravity tracks inherit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.