sectionReadout_of_pureTensorFactorization
plain-language theorem explainer
Pure-tensor factorization of a joint matter-channel operator yields a nonzero matter-section readout whenever the matter response is nontrivial at some eight-tick coordinate. Anyone citing the older factorization-based amplitude-linearity theorems can route through this constructor instead. The body is a structure package: fields are the reference state, slot, and scalar, and the readout identity is a short rewrite chain on pure tensors.
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$. Suppose $R_J(\psi\otimes\varphi)=R_M(\psi)\otimes R_C(\varphi)$ on pure tensors. If there exist a matter reference $\psi_0$ and a coordinate $i_0\in\{0,\ldots,7\}$ with $(R_M\psi_0)_{i_0}\neq 0$, then $R_C$ is recovered as the nonzero matter-section readout $$R_C(\varphi)=\chi^{-1}\cdot\mathrm{extract}_{i_0}\bigl(R_J(\psi_0\otimes\varphi)\bigr)$$ with $\chi=(R_M\psi_0)_{i_0}$.
background
Track 2.C studies when a channel response on the eight-tick ledger Signal8 is forced to be amplitude-linear. The joint substrate is the binary tensor product of two copies of Signal8 (matter factor first, channel factor second). Earlier work assumed full pure-tensor factorization: the joint operator acts as separate matter and channel maps on every pure tensor.
That factorization is stronger than needed. The weaker operational hypothesis is a nonzero matter-section readout: fix a matter reference $\psi_0$, a coordinate $i_0$, and a nonzero scalar $\chi$, inject $\psi_0$ into the first factor, apply the joint map, extract the channel factor at $i_0$, and rescale by $\chi^{-1}$. The structure JointSectionReadout packages exactly those data and the identity $R_C\varphi=\chi^{-1}\cdot\mathrm{extract}_{i_0}(R_J(\mathrm{insert}_1(\psi_0,\varphi)))$.
Upstream simp lemmas identify the insertion and extraction maps on pure tensors: insertFirst is pure tensor product, and extractSecond i (\psi\otimes\varphi)=(\psi i)\cdot\varphi.
proof idea
Package a JointSectionReadout from the factorization data. Set the reference state and slot to the given $\psi_0$ and $i_0$, and set $\chi:=(R_M\psi_0)_{i_0}$ with the supplied nonvanishing proof.
The readout identity is proved by rewriting: expand insertion as a pure tensor, apply the factorization hypothesis, apply the extraction lemma on pure tensors (which produces a scalar multiple of $\varphi$), cancel $\chi^{-1}\cdot\chi$ via inv_mul_cancel₀, and finish with one_smul. No induction or case split is required.
why it matters
This definition is the bridge that makes section-readout strictly more general than pure-tensor factorization. Downstream, isAmplitudeLinear_channel_of_pureTensorFactorization_via_sectionReadout recovers the old pure-tensor forcing theorem as a one-line corollary: build the section readout, then apply the section-readout amplitude-linearity theorem.
It also feeds sectionReadoutForcingCert, the structural certificate bundling section-forced amplitude linearity, density-only collapse, and the nonexistence of nontrivial density-only section channels. In the module narrative this retires the full factorization hypothesis for Track 2.C while keeping the older interface as a special case whenever the matter response is nontrivial on some eight-tick slot (the T7 octave period $2^3$).
The joint operator may still mix sectors away from the readout section; only the physical channel slice is constrained.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.