IsDensityOnly
plain-language theorem explainer
A channel response on the eight-tick complex signal is density-only when it is invariant under multiplication by any unit-modulus complex scalar. This predicate is the structural footprint of a CPTP-classical density-matrix readout and is the second half of the Track 2.C substrate dichotomy. Anyone proving that nontrivial amplitude-linear gravity channels cannot factor through classical density readouts cites it. The body is a pure universal Prop, not a derived theorem.
Claim. A map $R$ from eight-tick complex signals $\mathrm{Signal}_8 = \mathrm{Fin}\,8 \to \mathbb{C}$ to itself is density-only if, for every $c \in \mathbb{C}$ with $|c|=1$ and every signal $\psi$, one has $R(c\cdot\psi)=R(\psi)$.
background
Track 2.C of the quantum-gravity master plan forces amplitude-linearity of the gravitational channel from substrate structure rather than assuming it. The local state space is the eight-tick analytic carrier $\mathrm{Signal}_8 := \mathrm{Fin},8 \to \mathbb{C}$, the canonical complex signal from ComplexStructureForcing (tied to the eight-tick octave of the forcing chain).
A candidate channel response is a map $R : \mathrm{Signal}_8 \to \mathrm{Signal}_8$. Density-only means $R$ is blind to global $U(1)$ phases: multiplying the input by any unit-modulus complex scalar leaves the output unchanged. That is exactly the invariance of the pure-state density matrix $|\psi\rangle\langle\psi|$ under $\psi \mapsto c\psi$ when $|c|=1$, so any readout computed from the density matrix alone must satisfy the same identity.
The companion predicate is amplitude-linearity: $R$ agrees with some $\mathbb{C}$-linear map, hence preserves coherent superpositions. The module's dichotomy says these two structural conditions cannot hold together unless $R$ is identically zero.
proof idea
Definitional Prop, not a proved statement. The body is the universal quantification $\forall, c\in\mathbb{C},; |c|=1 \Rightarrow \forall,\psi,; R(c\cdot\psi)=R(\psi)$. No tactics, no lemmas, no reduction. Downstream proofs instantiate the quantifiers (typically at $c=-1$) after deriving phase-equivariance from amplitude-linearity.
why it matters
This predicate is one pole of the single-factor substrate dichotomy that opens Track 2.C and upgrades paper IV's T2 from MODEL to THEOREM. The parent theorems eq_zero_of_isAmplitudeLinear_isDensityOnly, not_isDensityOnly_of_isAmplitudeLinear_of_ne_zero, and not_exists_nontrivial_isAmplitudeLinear_and_isDensityOnly all take it as a hypothesis or conclusion: a nontrivial amplitude-linear response cannot be density-only.
Those lemmas feed the master cert Track2CCert.single_factor_dichotomy and the closure theorems track2C_channel_eq_zero_of_density_only and track2C_not_exists_nontrivial_density_only_channel, which rule out CPTP-classical density-matrix readouts for recognition-coupled channels. The many-body handoff Track2ManyBodyEndpoint inherits the local density-only collapse sitewise on pure tensors.
Framework landmark: the eight-tick carrier (T7) supplies the complex signal on which the dichotomy is stated; later work lifts it through the joint MacroscopicLedger to force amplitude-linearity of gravity from recognition-operator linearity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.