not_isDensityOnly_of_isAmplitudeLinear_of_ne_zero
plain-language theorem explainer
A nontrivial amplitude-linear response on the eight-tick signal space cannot be density-only. Track 2.C citations use this as the single-factor substrate dichotomy: no nonzero gravitational-channel map can be both ℂ-linear and a CPTP-classical density readout. Proof is a one-line contrapositive of the zero-forcing lemma for maps that are both amplitude-linear and density-only.
Claim. Let $R:\mathrm{Signal}_8\to\mathrm{Signal}_8$ agree with some $\mathbb{C}$-linear map. If $R\psi\neq 0$ for some ledger state $\psi$, then $R$ is not density-only: it fails invariance under unit-modulus complex scalings $c\cdot\psi$ with $\|c\|=1$, so it does not factor through the pure-state density matrix alone.
background
Track 2.C forces amplitude-linearity of the gravitational channel from substrate linearity, upgrading paper IV's T2 from modeling assumption to theorem. This module opens with the single-factor dichotomy on the canonical eight-tick carrier Signal8 (identified with Fin 8 → ℂ from ComplexStructureForcing), the analytic state space tied to the eight-tick octave (T7) and D=3 (T8).
A response $R$ is amplitude-linear when it equals some $\mathbb{C}$-linear map $L$, so it preserves coherent superpositions. It is density-only when $R(c\cdot\psi)=R\psi$ whenever $|c|=1$: the structural footprint of a CPTP-classical readout, since $|\psi\rangle\langle\psi|$ is phase-invariant. The module proves these two properties force $R\equiv 0$ on Signal8.
The sibling zero-forcing lemma states that any map that is both amplitude-linear and density-only vanishes identically. The present statement is the contrapositive seed used in the module doc: a nontrivial amplitude-linear channel response does not factor through a density-only readout.
proof idea
One-line term proof by contradiction. Assume density-only. Apply the upstream sibling eq_zero_of_isAmplitudeLinear_isDensityOnly at the given state $\psi$ to conclude $R\psi=0$, contradicting the nontriviality hypothesis. No further algebraic work; the content lives in the zero-forcing lemma.
why it matters
First Lean substrate-forcing statement of Gravity Track 2.C. It pins the single-channel dichotomy: on Signal8, no nontrivial response can be simultaneously consistent with substrate linearity (as in schrodinger_linear) and with a CPTP-classical density-only readout. The module doc names this the contrapositive form that opens the track; the existence form is the sibling no-go forbidding any nontrivial map that is both amplitude-linear and density-only.
Downstream, Track 2.C must lift the dichotomy from one factor to the joint matter-plus-channel MacroscopicLedger, forcing amplitude-linearity of the gravitational channel from factor-wise recognition-operator linearity. That closes the upgrade of paper IV T2 from MODEL to THEOREM. Framework landmarks in play are the eight-tick carrier (T7) and the complex structure forced on that register. Zero sorry and no new RS axioms; used_by is currently empty, so this is a seed rather than a consumed lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.