JointSectionReadout
plain-language theorem explainer
A joint section readout packages the operational data that recovers a channel response from a complex-linear joint operator by fixing a matter reference, applying the joint map, extracting one channel coordinate, and rescaling by a nonzero scalar. Gravity Track 2.C cites this as the weaker alternative to pure-tensor factorization when forcing amplitude-linearity. As a structure it carries no proof burden beyond field types and the readout identity.
Claim. A pair $(R_J, R_C)$, with $R_J$ a $\mathbb{C}$-linear endomorphism of the joint substrate $\mathrm{Signal}_8 \otimes \mathrm{Signal}_8$ and $R_C : \mathrm{Signal}_8 \to \mathrm{Signal}_8$ a channel response, admits a nonzero matter-section readout when there exist a fixed matter state $\psi_0$, an index $i_0 \in \{0,\ldots,7\}$, and a scalar $\chi \neq 0$ such that for every channel state $\varphi$, $R_C(\varphi) = \chi^{-1} \cdot \mathrm{extract}_{i_0}\bigl(R_J(\psi_0 \otimes \varphi)\bigr)$.
background
Gravity Track 2.C studies when a physical channel response on the eight-tick signal space must be amplitude-linear. Earlier modules forced that conclusion from a global pure-tensor factorization hypothesis on the joint operator $R_J$ acting on $\mathrm{Signal}_8 \otimes \mathrm{Signal}_8$. That hypothesis is stronger than needed operationally.
The joint substrate is the tensor product of two eight-component complex signals (the eight-tick octave). The map insertFirst embeds a fixed matter state $\psi$ as $\varphi \mapsto \psi \otimes \varphi$. The map extractSecond at coordinate $i$ pulls out the second factor scaled by the $i$-th component of the first factor. Together they define a linear slice of $R_J$.
This module replaces full factorization by a single nonzero section readout: only the operational family $\psi_0 \otimes \varphi$ is constrained. Away from that section, $R_J$ may still mix matter and channel sectors.
proof idea
Definitional structure, not a proved theorem. The fields are a matter reference $\psi_0$, a readout coordinate $i_0 \in \mathrm{Fin},8$, a nonzero complex scalar $\chi$, and the identity that $R_C$ equals the rescaled composition of insert-first, $R_J$, and extract-second. Inhabitation is by exhibiting those data; downstream theorems pattern-match on the structure and use $\chi \neq 0$ plus $\mathbb{C}$-linearity of $R_J$ and the insert/extract maps.
why it matters
This is the central hypothesis interface of Track 2.C's section-readout retirement of pure-tensor factorization. Downstream, isAmplitudeLinear_channel_of_sectionReadout shows any such readout forces amplitude-linearity with no factorization assumption; channel_eq_zero_of_density_only_of_sectionReadout and the existence-form no-go collapse density-only responses to zero. The one-shot theorem factor_product_retirement_one_statement packages both conclusions and recovers the older factorization result as a corollary (factorization implies section readout). RecognitionSectionReadout specializes the matter section to the recognition update, and SectionReadoutForcingCert bundles the master certificate. In the RS gravity channel program this closes the remaining Track 2.C gap: amplitude-linearity of the physical channel follows from an operational linear slice alone, consistent with the eight-tick octave structure of the signal space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.