amplitude_linear_forced_canonical_prop_holds
plain-language theorem explainer
Under the canonical recognition-coupled factorization, the quantum-channel response is forced amplitude-linear, and any density-only response collapses to zero. Gravity master-theorem consumers cite this as the structural discharge of the AmplitudeLinearForcedUnconditional hypothesis input. The proof is a one-line application of the Track 2.C headline theorem to the canonical recognition coupling from Session 88.
Claim. The structural proposition holds: in the canonical recognition-coupled factorization (cyclic shift on both factors), the channel-side response is forced to be amplitude-linear, and every density-only response collapses to zero.
background
Track 2.C/2.D sits inside the gravity quantum-channel program. A RecognitionCoupledFactorization is a named factor-product hypothesis that places the recognition update on the matter side of a joint substrate. Under that hypothesis, Sessions 85–88 show the channel-side response must be amplitude-linear: the output scales with field amplitude rather than with an arbitrary density functional.
The canonical witness canonicalRecognitionCoupled supplies an explicit factorization with cyclic shift on both factors. Session 94's Track 2.D headline strengthens this: under the same factorization the channel is amplitude-linear and any density-only response is forced to zero. The local module packages those structural results as a Prop suitable for the master theorem's hypothesis slot AmplitudeLinearForcedUnconditional (Session 97).
The module is a structural witness only. It does not retire the factor-product hypothesis from a stricter substrate axiom; that unconditional closure remains open.
proof idea
One-line term proof. Apply the Track 2.C headline theorem (track2C_headline) to the canonical recognition-coupled factorization witness (canonicalRecognitionCoupled). That headline already encodes amplitude-linearity of the channel response (and the density-only collapse) under the named factorization, so specializing it to the canonical coupling discharges the structural Prop directly.
why it matters
This theorem is the proved half of the structural witness that inhabits AmplitudeLinearForcedUnconditional on the gravity master theorem (Session 97). Downstream, amplitudeLinearForcedUnconditionalWitness packages the Prop together with this proof as a concrete inhabitant of the master-theorem hypothesis structure, so the conditional master theorem can treat amplitude-linear forcing as discharged on the canonical recognition coupling.
Within Recognition Science this is the gravity-side channel constraint that pairs with the recognition update: once the joint substrate factorizes with recognition on the matter factor, the channel cannot carry a free density-dependent response. The anti-retreat principle is met by pinning the witness to the named Session-88 canonical coupling rather than an abstract existence claim.
Open remainder: fully unconditional Track 2.C/2.D closure, which would eliminate the factor-product hypothesis entirely from the joint-operator side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.