amplitude_linear_forced_one_statement
plain-language theorem explainer
Under the canonical recognition-coupled factorization, the channel response is amplitude-linear, and any density-only response is forced to zero. The master-theorem hypothesis AmplitudeLinearForcedUnconditional is inhabited by that canonical witness. Gravity theorists citing Track 2.C/2.D structural closure use this packaging. The proof is a three-component term built from the Track 2.C headline and the structural witness.
Claim. For the canonical recognition-coupled factorization, the channel-side response $R_C$ is amplitude-linear (agrees with some $\mathbb{C}$-linear map on eight-tick signals). Moreover, if $R_C$ is density-only (invariant under unit-modulus phase multiplications), then $R_C\varphi=0$ for every signal $\varphi$. Finally, the master-theorem structure asserting unconditional amplitude-linear forcing is inhabited.
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 it preserves coherent superpositions of ledger states. It is density-only when invariant under unit-modulus complex scalings: the structural footprint of a CPTP-classical readout from $|\psi\rangle\langle\psi|$ alone.
The local setting is a structural witness module for the master-theorem hypothesis input that would make amplitude-linear forcing unconditional. Until that lift, forcing is structural under a named factor-product joint-substrate axiom with recognition update on the matter side. The canonical recognition-coupled factorization uses cyclic shift on both factors and supplies an explicit channel response $R_C$.
Upstream, track2C_headline states: under any recognition-coupled factorizable joint substrate, the channel-side response must be amplitude-linear, and any density-only candidate collapses to the trivial zero response. The structural witness packages the canonical instance of that Prop into the master-theorem hypothesis structure.
proof idea
Term-mode triple construction. The first two conjuncts are the two projections of track2C_headline applied to the canonical recognition-coupled factorization: amplitude-linearity of $R_C$, and the density-only-implies-zero implication. The third conjunct is a singleton inhabitation of AmplitudeLinearForcedUnconditional by amplitudeLinearForcedUnconditionalWitness, which itself wraps the canonical structural Prop and its proof of holding. No further rewriting or case analysis.
why it matters
Packages Sessions 85–88 and 94 into a single citation surface for Gravity Track 2.C/2.D structural closure. It feeds the master-theorem interface by inhabiting AmplitudeLinearForcedUnconditional: the factor-product joint-substrate axiom is still present as a named structural hypothesis, but the canonical witness makes the hypothesis structure nonempty for downstream gravity assembly.
In framework terms this is paper IV's T2 forced from substrate under the binary-tensor factor-product axiom, on the eight-tick octave signal space. Amplitude-linearity keeps coherent ledger superpositions; density-only collapse to zero rules out classical CPTP readouts as nontrivial channel responses under recognition coupling.
No downstream users are wired yet. The 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) remains open; this declaration does not claim that lift.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.