amplitudeLinearForcedStructuralCert
plain-language theorem explainer
Packages Track 2.C forcing under the canonical recognition-coupled factorization into a single structural certificate: channel response is amplitude-linear, any density-only response collapses to zero, and the master-theorem hypothesis AmplitudeLinearForcedUnconditional is inhabited. Gravity/quantum-channel workers cite it as the explicit structural witness for MasterTheorem Session 97. Construction is a three-field record filled by projecting track2C_headline on the canonical coupling and attaching the unconditional witness.
Claim. There is an explicit structural certificate whose fields assert: (i) the channel-side response $R_C$ of the canonical recognition-coupled factorization is amplitude-linear; (ii) if that response is density-only then $R_C\varphi=0$ for every eight-tick signal $\varphi$; (iii) the master-theorem hypothesis that amplitude-linearity is forced unconditionally (via the canonical structural Prop) is inhabited.
background
Track 2.C/2.D studies channel-side response maps on eight-tick signals under a recognition-coupled factorizable joint substrate: a named factor-product hypothesis with the recognition update on the matter side. The canonical witness canonicalRecognitionCoupled equips both factors with cyclic shift and sets the matter factor equal to the recognition update by reflexivity.
The upstream headline track2C_headline states that under any such recognition-coupled factorization the channel response is forced amplitude-linear, and any density-only (CPTP-classical) candidate collapses to the zero response. That is paper IV's T2 forced from substrate under the binary-tensor factor-product axiom: a structural theorem, not yet an unconditional lift to arbitrary joint operators.
This module's structure AmplitudeLinearForcedStructuralCert packages those two conclusions on the canonical coupling together with an inhabitant of Gravity.MasterTheorem.AmplitudeLinearForcedUnconditional, so the master theorem can consume a single cert object.
proof idea
One-line record construction. The first field is the left projection of track2C_headline applied to canonicalRecognitionCoupled (amplitude-linearity of $R_C$). The second field is the right projection of the same headline (density-only implies identically zero). The third field is the already-built amplitudeLinearForcedUnconditionalWitness, which wraps the canonical structural Prop as the master-theorem hypothesis input. No additional tactics or lemmas beyond those two projections and the witness def.
why it matters
Closes the structural side of Gravity Track 2.C/2.D for the master theorem: it turns Sessions 85–88 and 94 (recognition-coupled factorization forces amplitude-linearity and density-only collapse) into an inhabitant the Session 97 master theorem can demand. Downstream, amplitudeLinearForcedStructuralCert_inhabited is the one-line Nonempty proof that cites this def, and the module's one-statement theorem packages the same content for citation.
In the Recognition framework this is the gravity/quantum-channel forcing step that pins channel response to amplitude-linear form under the named factor-product substrate, consistent with the eight-tick octave (T7) signal type. It does not yet retire the factor-product hypothesis; the module doc flags fully unconditional Track 2.C/2.D closure (no factorization axiom) as future work. Anti-retreat is satisfied because the cert is pinned to the Session 88 canonical witness with its named FactorizableJointSubstrate hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.