sectionReadoutForcingCert_inhabited
plain-language theorem explainer
The section-readout forcing certificate is inhabited: there is a packaged witness that any channel recovered as a nonzero matter-section readout of a joint linear substrate is amplitude-linear, that density-only responses under that readout vanish, and that no nontrivial density-only channel admits such a readout. Gravity Track 2.C cites this as the one-shot structural certificate retiring global pure-tensor factorization. The proof is a one-line inhabitant from the bundled certificate definition.
Claim. The type of section-readout forcing certificates is nonempty. Such a certificate asserts: (i) every channel response $R_C$ recovered as a nonzero matter-section readout of a $\mathbb{C}$-linear joint substrate operator $R_J$ is amplitude-linear; (ii) if that channel is also density-only, then $R_C\varphi=0$ for all $\varphi$; (iii) no nontrivial density-only channel admits a section readout.
background
Track 2.C of the gravity quantum-channel development forces amplitude-linearity of the physical channel response without assuming full pure-tensor factorization of the joint operator. Earlier modules showed that if a joint map factorizes on pure tensors, the channel factor is amplitude-linear; the factor-product hypothesis is stronger than needed operationally.
A weaker principle suffices: the physical channel is recovered by a nonzero matter-section readout $\varphi \mapsto \chi^{-1}\cdot\mathrm{extractSecond}_{i_0}(R_J(\psi_0\otimes\varphi))$ for fixed matter reference $\psi_0$, coordinate $i_0$, and nonzero scalar $\chi$. Because this is a linear slice of a $\mathbb{C}$-linear joint operator, amplitude-linearity of the channel is automatic; the joint map may still mix sectors off that section.
SectionReadoutForcingCert packages three consequences of that readout principle: section readout forces amplitude-linearity; density-only responses under section readout collapse to zero; and no nontrivial density-only channel admits a section readout. The companion definition sectionReadoutForcingCert fills those fields from the module's main lemmas.
proof idea
One-line term proof: inhabit Nonempty SectionReadoutForcingCert by the explicit witness sectionReadoutForcingCert. That definition already wires the three certificate fields to isAmplitudeLinear_channel_of_sectionReadout, channel_eq_zero_of_density_only_of_sectionReadout, and not_exists_nontrivial_density_only_channel_with_sectionReadout. No further tactic work is required.
why it matters
This is the TRACK 2.C one-shot theorem in section-readout form. It certifies that global pure-tensor factorization is not required to force channel amplitude-linearity: a nonzero matter-section readout of the joint linear substrate is enough, and under that principle density-only responses collapse. Factorization theorems become corollaries because factorization implies section readout.
In the Recognition gravity stack this retires the remaining Track 2.C gap flagged in the module status (structural theorem, zero sorry, closed 2026-05-22). It sits downstream of the joint and substrate forcing modules and packages their section-readout weakening into a single inhabitability fact that later gravity or quantum-channel developments can cite without reopening the factorization hypothesis. No further used_by edges are recorded yet; the declaration is the terminal certificate of this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.