RecognitionSectionReadout
plain-language theorem explainer
A recognition-section readout packages a joint linear operator and channel map so the channel is recovered by injecting a fixed matter reference, applying the joint map, extracting at one of eight coordinates, and normalizing by the recognition-update component there. The matter section is the substrate recognition update, not an arbitrary scalar. Track 2.C cites this to force amplitude-linearity without global pure-tensor factorization. Pure structure data plus a nontriviality side condition.
Claim. For a $\mathbb{C}$-linear joint operator $R_J$ on the two-factor eight-tick substrate and a channel map $R_C$, a recognition-section readout consists of a matter reference $\psi_0$ and a coordinate $i_0\in\{0,\ldots,7\}$ such that the substrate recognition update of $\psi_0$ is nonzero at $i_0$, and for every channel state $\varphi$, $R_C(\varphi)$ equals the inverse of that component times the $i_0$-extraction of $R_J$ applied to the pure tensor $\psi_0\otimes\varphi$.
background
Track 2.C forces the physical channel response $R_C$ to be amplitude-linear without assuming the joint operator factorizes on every pure tensor. Earlier modules needed a global factor-product hypothesis; this module weakens that to a single nonzero matter-section readout: inject a fixed matter reference into the first factor, apply the joint map, extract the channel factor at one coordinate, and rescale by a nonzero scalar.
The general package is a joint-section readout: data $(\psi_0,i_0,\chi)$ with $\chi\neq 0$ and the readout identity for every channel state. The recognition-section variant specializes $\chi$ to the $i_0$-component of the substrate recognition update of $\psi_0$. That update is the concrete projector-after-shift operator on eight-tick signals (the eight-tick octave of the forcing chain).
Upstream helpers insert a fixed matter state as a pure tensor into the joint substrate and extract the second factor scaled by the chosen first-factor coordinate. The joint substrate is the tensor product of two eight-tick signal spaces.
proof idea
Definitional structure, not a proved theorem. Fields record the matter reference, the extraction coordinate, the side condition that the recognition update is nonzero at that coordinate, and the pointwise readout identity that recovers $R_C$ from $R_J$.
The companion coercion to a joint-section readout is a one-line field map: copy $\psi_0$ and $i_0$, set the scalar $\chi$ to the recognition-update component at $i_0$, reuse the nontriviality proof as $\chi\neq 0$, and reuse the same readout identity. Downstream amplitude-linearity then follows by applying the general section-readout forcing lemma to that coercion.
why it matters
This is the weaker Track 2.C replacement for the old global pure-tensor factorization assumption: the matter section is forced to be the actual substrate recognition update rather than an arbitrary factor. It feeds three parent results in the same module: recognition-section forcing (any such channel response is amplitude-linear), density-only collapse (a density-only response under this readout is identically zero), and the nonexistence statement that no nontrivial density-only channel arises from a recognition-section readout of a linear joint substrate.
Framework landmarks: the eight-tick signal space is the T7 octave; the recognition update is the concrete projector-after-shift dynamics on that octave. Closing this structural gap lets Track 2.C force amplitude-linearity from an operational linear slice of the joint operator, while still allowing matter-channel mixing off the readout section. The module reports structural closure with zero sorry and no RS-internal axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.