isAmplitudeLinear_channel_of_recognitionSectionReadout
plain-language theorem explainer
Under a recognition-section readout of a joint matter-channel operator, the recovered channel map is amplitude-linear. Track 2.C gravity workers cite this when the matter slice is the substrate recognition update rather than an arbitrary section, and no global pure-tensor factorization is assumed. The proof is a one-line reduction to the general section-readout forcing theorem via the structure coercion.
Claim. Let $R_J$ be a $\mathbb{C}$-linear map on the joint substrate $\mathrm{Signal}_8\otimes_{\mathbb{C}}\mathrm{Signal}_8$, and let $R_C:\mathrm{Signal}_8\to\mathrm{Signal}_8$. Suppose $R_C$ is recovered by a nonzero section readout of $R_J$ whose matter section is the substrate recognition update: for fixed $\psi_0$ and coordinate $i_0$ with $(\mathrm{recognitionUpdate}\,\psi_0)_{i_0}\neq 0$, one has $R_C\varphi=\bigl((\mathrm{recognitionUpdate}\,\psi_0)_{i_0}\bigr)^{-1}\cdot\mathrm{extractSecond}_{i_0}\bigl(R_J(\psi_0\otimes\varphi)\bigr)$. Then $R_C$ is amplitude-linear: it agrees with some $\mathbb{C}$-linear endomorphism of $\mathrm{Signal}_8$.
background
Track 2.C studies when a gravitational channel response on the eight-tick ledger Signal8 must be amplitude-linear, meaning it coincides with a genuine $\mathbb{C}$-linear map and therefore preserves coherent superpositions. The joint substrate is the binary tensor product of two Signal8 factors (matter and channel). Earlier forcing results required pure-tensor factorization of the joint operator on every pure tensor; this module weakens that hypothesis.
A section readout recovers the channel response by fixing a matter reference, applying the joint operator, extracting one channel coordinate, and rescaling by a nonzero scalar. The general theorem already shows any such nonzero section readout forces amplitude-linearity of the channel factor, with no factorization assumption.
Recognition-section readout specializes the matter section to the substrate recognition update (the cyclic shift on the ledger). Nontriviality is the single nonzero coordinate condition on that update at the chosen index. This is the operationally natural matter slice for Recognition Science, replacing the stronger global factor-product hypothesis.
proof idea
One-line term wrapper. The recognition-section hypothesis coerces to an ordinary joint section readout (same joint operator and channel map, matter section specialized to the recognition update). Apply the upstream section-readout forcing theorem, which constructs the witnessing linear map as the inverse-scalar multiple of the corresponding linear slice of the joint operator. No new algebra is done here.
why it matters
This is the recognition-specialized form of section-readout forcing in Gravity Track 2.C. The module's stated goal is to retire the full pure-tensor factorization hypothesis used in AmplitudeLinearForcedJoint, AmplitudeLinearForcedSubstrate, and the bundled AmplitudeLinearForcedCert. Only a nonzero linear slice of the joint operator is needed; the joint map may still mix matter and channel away from that section.
The doc-comment frames it as recognition-section forcing: under the substrate recognition update, any channel response obtained by a nonzero section readout is amplitude-linear, with no global pure-tensor factorization. Sibling results then get density-only collapse and the nonexistence of nontrivial density-only channels under the same readout. No downstream dependents are recorded yet; the declaration closes the recognition instance of the structural theorem (0 sorry, 0 RS-internal axiom). Framework context is the eight-tick octave ledger (Signal8, period $2^3$) on which channel responses act.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.