IsPhaseEquivariant
plain-language theorem explainer
Phase-equivariance is the predicate that a channel response R on the eight-tick complex signal space commutes with arbitrary complex scaling: R(c·ψ)=c·R(ψ). Track 2.C gravity work cites it as the bridge from amplitude-linearity to the substrate dichotomy against density-only readouts. The declaration is a pure Prop definition, not a proved statement.
Claim. A map $R$ from the eight-tick complex signal space $\mathrm{Signal}_8$ to itself is phase-equivariant when $R(c\cdot\psi)=c\cdot R(\psi)$ for every $c\in\mathbb{C}$ and every signal $\psi$.
background
Track 2.C of the quantum-gravity plan forces amplitude-linearity of the gravitational channel from substrate structure, upgrading paper IV's T2 from model assumption to theorem. The local setting is a single channel factor on the canonical eight-tick analytic carrier Signal8 (identified with Fin 8 → ℂ from ComplexStructureForcing).
Two competing structural footprints are introduced for a candidate response $R:\mathrm{Signal}_8\to\mathrm{Signal}_8$. Amplitude-linearity means $R$ agrees with some $\mathbb{C}$-linear map, so it preserves coherent superpositions. Density-only means $R$ is invariant under unit-modulus complex scalings, the footprint of a CPTP-classical readout that depends only on the density matrix $|\psi\rangle\langle\psi|$.
Phase-equivariance sits between them: full complex scaling (not just unit modulus) must pass through $R$. The module imports ComplexStructureForcing for the carrier and works with zero sorry and no new RS axioms.
proof idea
Pure definition: the body is the universal quantification $\forall c,\psi,, R(c\bullet\psi)=c\bullet R\psi$. No tactics, no lemmas. Downstream proofs inhabit the predicate by unpacking an amplitude-linear witness $L$ and rewriting with $L.\mathrm{map_smul}$.
why it matters
This predicate is the intermediate structural property used by isPhaseEquivariant_of_isAmplitudeLinear (amplitude-linear responses are phase-equivariant) and then by the substrate dichotomy eq_zero_of_isAmplitudeLinear_isDensityOnly: if $R$ is both amplitude-linear and density-only, testing at the unit-modulus scalar $c=-1$ forces $R\psi=0$ identically.
That dichotomy is the first Lean substrate-forcing statement of Track 2.C. Its contrapositive says a nontrivial amplitude-linear channel response does not factor through a density-only readout. Later Track 2.C work lifts the single-factor fact to the joint matter-plus-channel MacroscopicLedger, composing recognition-operator linearity factor-wise to force amplitude-linearity of the gravitational channel. The eight-tick carrier ties to the T7 octave and the ComplexStructureForcing/Clifford Cl₈ grading background.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.