SectionReadoutForcingCert
plain-language theorem explainer
Bundles four structural facts that replace global pure-tensor factorization by a weaker nonzero matter-section readout of a joint linear operator. Anyone citing Track 2.C amplitude-linearity without full factorization uses this certificate. The inhabiting instance wires the four proved lemmas into one record; no new mathematics is proved here.
Claim. A certificate packing four claims: (i) if a channel map $R_C$ is recovered as a nonzero matter-section readout of a $\mathbb{C}$-linear joint operator $R_J$, then $R_C$ is amplitude-linear; (ii) any density-only such $R_C$ vanishes identically; (iii) no nontrivial density-only channel admits a section readout; (iv) pure-tensor factorization with a nonzero matter component at some coordinate yields a section readout of the channel factor.
background
Track 2.C studies gravitational-channel responses on the eight-tick ledger Signal8. Earlier work forced amplitude-linearity of the channel factor only under full pure-tensor factorization: the joint operator on the matter-plus-channel substrate $R_J : \mathrm{Signal8}\otimes\mathrm{Signal8}\to\mathrm{Signal8}\otimes\mathrm{Signal8}$ must act as $R_M\otimes R_C$ on every pure tensor.
A response is amplitude-linear when it agrees with some $\mathbb{C}$-linear map (preserving coherent superpositions). It is density-only when invariant under unit-modulus phase multiplications, the footprint of a classical density-matrix readout. The module weakens the hypothesis: it is enough that $R_C$ arise as a nonzero matter-section readout of $R_J$, i.e. fix a matter reference $\psi_0$, coordinate $i_0$, and scalar $\chi\neq 0$, and recover $R_C\varphi=\chi^{-1}\cdot\mathrm{extractSecond}_{i_0}(R_J(\psi_0\otimes\varphi))$. The joint operator may still mix sectors off that slice.
proof idea
This is a pure structure declaration: four named fields of propositional type, no proof body. The inhabiting definition sectionReadoutForcingCert fills each field by direct application of the corresponding proved lemma: isAmplitudeLinear_channel_of_sectionReadout, channel_eq_zero_of_density_only_of_sectionReadout, not_exists_nontrivial_density_only_channel_with_sectionReadout, and sectionReadout_of_pureTensorFactorization. Nonemptiness is then immediate from that instance.
why it matters
This is the master certificate for the section-readout retirement of global pure-tensor factorization in Gravity Track 2.C. Downstream, sectionReadoutForcingCert and sectionReadoutForcingCert_inhabited package the four lemmas as a single STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom). The one-shot Track 2.C theorem then states that global factorization is unnecessary: a nonzero matter-section readout already forces channel amplitude-linearity and collapses density-only responses to zero. That closes the remaining gap left by AmplitudeLinearForcedJoint, AmplitudeLinearForcedSubstrate, and the older AmplitudeLinearForcedCert under the stronger FactorizableJointSubstrate hypothesis. In the broader RS gravity program this pins the channel response to the amplitude-linear class compatible with coherent ledger evolution on the eight-tick octave, without demanding a product structure on every pure tensor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.