amplitudeLinearForcedUnconditionalWitness
plain-language theorem explainer
Inhabitant of the master-theorem hypothesis structure for amplitude-linear forcing of the quantum-channel response. It packages the structural claim that, under the canonical recognition-coupled factorization, the channel is amplitude-linear and any density-only response vanishes. Gravity-track authors cite it when pre-filling Track 2.C/2.D inputs to the structural master theorem. Construction is a direct structure instance whose fields are the canonical Prop and its already-proved holds lemma.
Claim. There is an inhabitant of the master-theorem hypothesis structure for amplitude-linear forcing whose propositional field is the structural statement that the channel response of the canonical recognition-coupled factorization is amplitude-linear and that any density-only response of that channel is identically zero, together with a proof that this statement holds.
background
Track 2.C/2.D concerns the quantum-channel side of the RS gravity program: under a recognition-coupled factorization (a named factor-product joint substrate with the recognition update on the matter side), the channel-side response is forced to be amplitude-linear, and any density-only response collapses to the zero map. The canonical recognition-coupled witness supplies an explicit factorization with cyclic shift on both factors.
The master theorem (Session 97) exposes a hypothesis structure whose fields are a bare Prop claiming unconditional amplitude-linear forcing, plus a proof that the Prop holds. Until the factor-product axiom is retired from a stricter substrate, that Prop is filled by structural content rather than a fully unconditional derivation.
This module packages Sessions 85–88 and 94 as that structural fill: the Prop asserts amplitude-linearity of the canonical channel response together with density-only collapse to zero, and the holds field is the Track 2.C/2.D headline applied to the canonical coupling.
proof idea
Direct structure instance, not a tactic proof. The propositional field is set equal to the canonical structural Prop (amplitude-linearity of the canonical channel response, and density-only implying the zero response). The holds field is filled by the already-proved theorem that this Prop holds, which itself is a one-line application of the Track 2.C headline to the canonical recognition-coupled factorization.
why it matters
This witness is one of the five structural inputs that let the fully structural master theorem compile with zero open hypothesis arguments. Downstream it is threaded into the structural master cert, the structural master theorem, the one-statement structural master form, and the honest-scope statement that records which witnesses are inhabited versus still dynamical.
Inside the same module it also feeds the Track 2.C/2.D structural one-statement and the local structural cert. The module status is closed structural theorem (zero sorry, zero RS-internal axiom). What remains open is the true unconditional Track 2.C/2.D lift: retiring the factor-product hypothesis entirely, rather than inhabiting it via the canonical recognition coupling. That upgrade is exactly the gap the honest-scope statement flags for the discovery-grade master theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.