AmplitudeLinearForcedStructuralCert
plain-language theorem explainer
Certificate structure packaging three props: the canonical recognition-coupled channel response is amplitude-linear; any density-only such response vanishes on every eight-tick signal; and a master-theorem unconditional hypothesis witness is present. Gravity Track 2.C/2.D consumers cite it as the structural cert type. Pure structure definition: field types only, no proof body.
Claim. A structural certificate for amplitude-linear forcing consists of three data: (i) the channel-side response $R_C$ of the canonical recognition-coupled factorization is amplitude-linear (agrees with some $\mathbb{C}$-linear map on eight-tick signals); (ii) if that $R_C$ is density-only (invariant under unit-modulus phase), then $R_C\varphi=0$ for every eight-tick signal $\varphi$; (iii) a witness inhabiting the master-theorem unconditional amplitude-linear forcing hypothesis.
background
Track 2.C/2.D studies gravitational channel responses on eight-tick signals (Signal8). A response is amplitude-linear when it equals some $\mathbb{C}$-linear map, so coherent superpositions of ledger states are preserved. It is density-only when invariant under unit-modulus complex scaling: the structural footprint of a CPTP-classical readout from $|\psi\rangle\langle\psi|$ alone.
The canonical recognition-coupled factorization (Session 88) is an explicit factor-product joint substrate with cyclic shift on both factors and the recognition update on the matter side. Under any such recognition-coupled factorization, Track 2.C/2.D forces the channel-side response to be amplitude-linear, and forces any density-only response to collapse to zero.
The master theorem exposes AmplitudeLinearForcedUnconditional as a hypothesis structure: a bare Prop plus a proof it holds, intended for the day the factor-product axiom is lifted or eliminated. Until that lift, forcing remains structural under the named factorization hypothesis.
proof idea
No proof: this is a structure declaration. The three fields are Prop-typed requirements (plus one nested hypothesis structure). Downstream, amplitudeLinearForcedStructuralCert fills the first two fields from the two projections of track2C_headline applied to canonicalRecognitionCoupled, and supplies the master hypothesis witness separately. Inhabitation is then the trivial constructor packing that value.
why it matters
This is the typed payload for the structural witness that closes Gravity Track 2.C/2.D at the certificate layer (module status: 0 sorry, structural theorem, closure 2026-05-22). Downstream amplitudeLinearForcedStructuralCert and amplitudeLinearForcedStructuralCert_inhabited inhabit it, feeding the one-statement structural headline under the canonical recognition-coupled factorization.
It bridges Sessions 85–88 and 94 (forcing under RecognitionCoupledFactorization, density-only collapse) into the Session 97 master-theorem interface AmplitudeLinearForcedUnconditional. In RS terms it records that the eight-tick channel response, once recognition-coupled, cannot be a nontrivial classical density readout: amplitude linearity is forced, and density-only responses die.
Open remainder (explicit in the module doc): fully unconditional Track 2.C/2.D closure, retiring the factor-product hypothesis from a stricter substrate axiom or eliminating it on the joint-operator side, is future work. This cert still uses the canonical coupling as a specific factor-product witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.