isPhaseEquivariant_of_isAmplitudeLinear
plain-language theorem explainer
Any gravitational-channel response on the eight-tick complex signal space that agrees with a ℂ-linear map automatically commutes with arbitrary complex scaling. Gravity Track 2.C cites this as the bridge from amplitude-linearity to phase-equivariance before the density-only clash. The proof unpacks the witnessing linear map and applies its scalar-multiplication law.
Claim. Let $R : \mathrm{Signal}_8 \to \mathrm{Signal}_8$ be a map on the eight-tick complex signal carrier. If $R$ is amplitude-linear (there exists a $\mathbb{C}$-linear map $L$ with $R\psi = L\psi$ for every state $\psi$), then $R$ is phase-equivariant: $R(c\cdot\psi) = c\cdot R\psi$ for every $c\in\mathbb{C}$ and every $\psi$.
background
Track 2.C of the quantum-gravity plan forces amplitude-linearity of the gravitational channel from substrate structure rather than assuming it. The local state space is Signal8, the eight-tick analytic carrier Fin 8 → ℂ from ComplexStructureForcing, the same period-$2^3$ octave that appears as T7 in the forcing chain.
A response $R$ is amplitude-linear when it coincides with some $\mathbb{C}$-linear endomorphism, so it preserves coherent superpositions of ledger states. Phase-equivariance is the weaker structural demand that $R$ commute with every complex scalar action: $R(c\cdot\psi)=c\cdot R\psi$. Density-only responses, by contrast, are invariant under unit-modulus phases and therefore read only the projector $|\psi\rangle\langle\psi|$.
This lemma sits between those two predicates. It converts the existence of a linear witness into the scaling identity needed to pit amplitude-linearity against density-only behavior on a single channel factor.
proof idea
Term-mode unpacking of the amplitude-linearity hypothesis. From IsAmplitudeLinear R one obtains a $\mathbb{C}$-linear map $L$ with $R=L$ pointwise. For arbitrary $c\in\mathbb{C}$ and $\psi$, rewrite both $R(c\cdot\psi)$ and $R\psi$ via that equality, then apply the linear-map identity $L(c\cdot\psi)=c\cdot L\psi$ (map_smul). The resulting chain is exactly phase-equivariance. No extra lemmas beyond the linear-map API are required.
why it matters
This is the first structural step inside the single-factor substrate dichotomy of Track 2.C. The immediate parent is eq_zero_of_isAmplitudeLinear_isDensityOnly, which assumes both amplitude-linearity and density-only behavior and concludes $R\equiv 0$ by testing at the unit-modulus scalar $c=-1$; that proof opens by invoking the present lemma to obtain phase-equivariance.
Together with the contrapositive forms (not_isDensityOnly_of_isAmplitudeLinear_of_ne_zero and the nontrivial nonexistence statement), the dichotomy upgrades paper IV's T2 from a modeling assumption to a theorem: a nontrivial amplitude-linear channel response cannot factor through a density-only readout. Later Track 2.C work lifts the same clash to the joint matter-plus-channel MacroscopicLedger, using factor-wise Schrödinger linearity, so the gravitational channel is forced to be amplitude-linear on the full substrate. Zero sorry and no new RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.