sectionReadoutForcingCert
plain-language theorem explainer
Packages the section-readout forcing results into a single master certificate: any channel recovered as a nonzero matter-section readout of a linear joint operator is amplitude-linear, density-only responses collapse to zero, and pure-tensor factorization implies the weaker readout hypothesis. Gravity Track 2.C cites this as the inhabited witness that global factorization is no longer required. The body is a pure field-by-field assembly of four already-proved lemmas.
Claim. There is a master certificate whose fields assert: (i) every channel response $R_C$ recovered as a nonzero matter-section readout of a $\mathbb{C}$-linear joint operator $R_J$ is amplitude-linear; (ii) any density-only such $R_C$ vanishes identically; (iii) no nontrivial density-only channel arises this way; (iv) pure-tensor factorization of $R_J$ with nontrivial matter response at some coordinate yields a section readout.
background
Gravity Track 2.C studies when a physical channel response on the eight-tick signal space must be amplitude-linear. Earlier modules forced amplitude-linearity only under a global pure-tensor factorization of the joint operator $R_J$ on every pure tensor $\psi \otimes \phi$. That hypothesis is stronger than needed operationally.
A joint section readout means the channel map is recovered by a linear slice: fix a matter reference $\psi_0$, a coordinate $i_0$, and a nonzero scalar $\chi$, and set $R_C(\phi) = \chi^{-1} \cdot \mathrm{extractSecond}_{i_0}(R_J(\psi_0 \otimes \phi))$. The joint operator may still mix sectors off that section.
The structure SectionReadoutForcingCert is the master bundle of four claims: section readout forces amplitude-linearity; density-only responses under readout collapse to zero; no nontrivial density-only readout exists; and pure-tensor factorization implies section readout whenever the matter response is nontrivial at some coordinate. This definition assembles those four proved facts into one inhabited certificate.
proof idea
Field-by-field assembly, no new mathematics. The amplitude-linearity field is the one-line application of isAmplitudeLinear_channel_of_sectionReadout. The density-only collapse field applies channel_eq_zero_of_density_only_of_sectionReadout. The no-go field is exactly not_exists_nontrivial_density_only_channel_with_sectionReadout. The factorization-implies-section field is a short intro that hands the pure-tensor data to sectionReadout_of_pureTensorFactorization.
why it matters
This is the inhabited witness for Track 2.C's section-readout retirement of global pure-tensor factorization. Downstream, sectionReadoutForcingCert_inhabited simply wraps it as Nonempty SectionReadoutForcingCert, which the module presents as the one-shot theorem: global factorization is not needed to force channel amplitude-linearity; a nonzero matter-section readout suffices.
In the Recognition gravity quantum-channel stack, amplitude-linearity of the channel response is the structural gate that rules out density-only (Born-like) alternatives on the eight-tick substrate. By packaging the weaker readout hypothesis, this certificate closes the remaining Track 2.C gap left by AmplitudeLinearForcedJoint, AmplitudeLinearForcedSubstrate, and AmplitudeLinearForcedCert. It sits on the gravity side of the RS forcing chain rather than on T5--T8 themselves, but it is the operational interface those earlier factorization theorems feed into once the pure-tensor assumption is dropped.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.