AmplitudeLinearForcedUnconditional
plain-language theorem explainer
Packages the open Track 2.C/2.D claim that the quantum-channel response is forced amplitude-linear without any factor-product joint-substrate axiom. Gravity and channel workers cite it as one of five named hypothesis inputs to the conditional RS quantum-gravity master theorem. It is a two-field structure (a Prop plus a witness) with no internal proof content; discharge is deferred to the unconditional lift.
Claim. A record consisting of a proposition asserting that the channel response is forced to be linear in amplitude, independent of any factor-product structural axiom on the joint substrate, together with a witness that this proposition holds.
background
The Gravity.MasterTheorem module authors the RS quantum-gravity master statement as a twelve-clause conjunction (Track 7.A). Eight clauses are already discharged from Sessions 89–96 anchors; five remain as hypothesis inputs for still-open tracks. The conditional master theorem takes those five inputs and returns the full master statement.
Amplitude-linear forcing says the quantum gravity channel maps amplitudes linearly. In the present codebase that claim is only STRUCTURAL: it depends on a named factor-product joint-substrate axiom (Sessions 85–88, 94). Track 2.C/2.D is the program to lift that axiom, either by rederiving it from a stricter substrate principle or by eliminating it from the joint-operator side.
This structure is the Lean interface for the unconditional form of that claim. Sibling hypothesis bundles in the same module play the same role for the classical continuum/Bianchi limit, the dynamical Page curve, PTA stochastic GW distinctness, and strong-field GR discriminators.
proof idea
No proof body: the declaration is a structure definition. It exposes a Prop field naming the unconditional amplitude-linear forcing claim and a holds field inhabiting that Prop. Downstream conditional master theorems take an instance as a hypothesis and project the witness when assembling the corresponding clause of the master conjunction. There is no algebraic reduction or tactic script here.
why it matters
This is the Track 2.C/2.D gate on the master theorem. It is consumed by RSQuantumGravityMaster, the conditional master theorem, the one-statement form, and the deeper-partial conditional variants in MasterTheoremDeeperPartial. The master plan treats amplitude-linear forcing (paired with unconditional BMV positivity) as the quantum-channel half of the discovery chain.
Until the factor-product axiom is lifted, the amplitude-linear clause remains STRUCTURAL rather than theorem-grade. Closing Track 2.C/2.D would remove this input from the conditional master theorem and advance the unconditional rs_quantum_gravity_master form. It does not by itself touch T0–T8, the RCL, or the phi ladder; those enter through other closed clauses of the same master conjunction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.