eq_zero_of_isAmplitudeLinear_isDensityOnly
plain-language theorem explainer
Any map on the eight-tick signal space that is both amplitude-linear (agrees with a ℂ-linear operator) and density-only (invariant under unit-modulus phases) must vanish identically. Gravity Track 2.C cites this as the single-factor substrate dichotomy forcing nontrivial channel responses off classical density readouts. The proof pits phase equivariance against density invariance at the scalar −1, yielding Rψ = −Rψ and hence Rψ = 0 in the ℂ-module.
Claim. Let $R : (\mathrm{Fin}\,8 \to \mathbb{C}) \to (\mathrm{Fin}\,8 \to \mathbb{C})$. If $R$ agrees with some $\mathbb{C}$-linear map and $R(c\cdot\psi)=R(\psi)$ whenever $\|c\|=1$, then $R(\psi)=0$ for every signal $\psi$.
background
Track 2.C upgrades paper IV's T2 from a modeling assumption to a theorem: the gravitational channel must be amplitude-linear because the recognition substrate is linear. The local state space is the eight-tick analytic carrier Signal8 ≅ Fin 8 → ℂ from ComplexStructureForcing, the same space on which the discrete Schrödinger evolution lives.
Amplitude-linearity means $R$ coincides with some map $L$ in the $\mathbb{C}$-linear endomorphisms of Signal8, so coherent superpositions are preserved. Density-only means $R(c\cdot\psi)=R(\psi)$ for every unit-modulus $c$; that is the structural footprint of a CPTP-classical readout depending only on $|\psi\rangle\langle\psi|$. Amplitude-linear maps are automatically phase-equivariant: $R(c\cdot\psi)=c\cdot R(\psi)$ for all $c\in\mathbb{C}$.
Upstream, schrodinger_linear records that one-tick recognition evolution is $\mathbb{C}$-linear on Signal8. The dichotomy here is the single-channel seed that later lifts, via pure-tensor factorization on the joint matter-plus-channel ledger, to force channel amplitude-linearity from joint substrate linearity.
proof idea
First apply the sibling lemma that amplitude-linearity implies phase equivariance, so $R((-1)\cdot\psi)=(-1)\cdot R(\psi)$. Density-only at the same scalar (using $|-1|=1$) gives $R((-1)\cdot\psi)=R(\psi)$. Transitivity yields $R\psi=-R\psi$, hence $(2:\mathbb{C})\cdot R\psi=0$ by rewriting $2\cdot v=v+v$ and cancelling. Since $2\neq 0$ in $\mathbb{C}$ and Signal8 is a NoZeroSMulDivisors $\mathbb{C}$-module (as Fin 8 → ℂ), the scalar-or-vector zero dichotomy forces $R\psi=0$.
why it matters
This is the opening substrate dichotomy of Gravity Track 2.C: on a single channel factor, no nontrivial gravitational response can be both substrate-linear and density-only. The contrapositive not_isDensityOnly_of_isAmplitudeLinear_of_ne_zero is the first Lean substrate-forcing statement of the track; the existence form not_exists_nontrivial_isAmplitudeLinear_and_isDensityOnly packages the no-go.
Downstream, track2CCert wraps this as the single-factor dichotomy field of the master certificate. Joint-substrate lifts (channel_eq_zero_of_density_only_of_pureTensorFactorization, the symmetric matter form, and isAmplitudeLinear_both_of_pureTensorFactorization) use the same clash under pure-tensor factorization to force amplitude-linearity of the gravitational channel from joint recognition linearity (schrodinger_linear composed factor-wise). Section-readout and recognition-update variants reuse the zero conclusion under their respective structural hypotheses.
Framework landmarks: the eight-tick carrier (T7) and complex structure forcing supply Signal8; the result blocks classical density-only gravity channels while preserving coherent ledger superpositions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.