IsAmplitudeLinear
plain-language theorem explainer
A gravitational-channel response on the eight-tick complex signal space is amplitude-linear when it coincides pointwise with some ℂ-linear operator. Track 2.C cites this predicate as the structural half of the single-factor substrate dichotomy. Amplitude-linear maps preserve coherent superpositions of ledger states. The body is a pure existence Prop over Mathlib linear maps on Fin 8 → ℂ.
Claim. A map $R$ from the eight-tick complex signal space $\mathrm{Signal}_8 = (\mathrm{Fin}\,8 \to \mathbb{C})$ to itself is amplitude-linear if there exists a $\mathbb{C}$-linear operator $L : \mathrm{Signal}_8 \to_{\mathbb{C}} \mathrm{Signal}_8$ such that $R(\psi) = L(\psi)$ for every signal $\psi$.
background
Track 2.C of the quantum-gravity master plan upgrades paper IV's T2 from a modeling assumption to a theorem: the gravitational channel must be forced amplitude-linear from substrate linearity. This module opens that track with a single-factor dichotomy on the canonical eight-tick analytic carrier.
Signal8 is the local abbreviation for Fin 8 → ℂ, identified with the carrier from Foundation.ComplexStructureForcing. That space is the discrete eight-tick octave (period $2^3$) on which candidate channel responses $R : \mathrm{Signal}_8 \to \mathrm{Signal}_8$ are tested.
Amplitude-linearity means $R$ agrees with some Mathlib ℂ-linear map. The companion predicates are phase-equivariance (commutes with arbitrary complex scaling) and density-only (invariant under unit-modulus scalars, i.e. depends only on $|\psi\rangle\langle\psi|$). The module proves these cannot hold simultaneously unless $R \equiv 0$.
proof idea
Pure definition: the predicate is the Prop that there exists a Mathlib linear map $L : \mathrm{Signal}8 \to{\ell[\mathbb{C}]} \mathrm{Signal}_8$ with $R\psi = L\psi$ for all $\psi$. No proof obligations; downstream lemmas unpack the existential via rcases and apply map_smul.
why it matters
This predicate is the structural half of Track 2.C's substrate dichotomy. Downstream, isPhaseEquivariant_of_isAmplitudeLinear shows amplitude-linear responses are phase-equivariant; eq_zero_of_isAmplitudeLinear_isDensityOnly then tests the two conditions at $c = -1$ and forces $R \equiv 0$. The contrapositive not_isDensityOnly_of_isAmplitudeLinear_of_ne_zero is the first Lean substrate-forcing statement of Track 2.C: a nontrivial amplitude-linear channel does not factor through a density-only readout.
The existence form not_exists_nontrivial_isAmplitudeLinear_and_isDensityOnly and the cert bundle Track2CCert.single_factor_dichotomy package the same fact. Later, track2C_channel_isAmplitudeLinear lifts the single-factor dichotomy to a recognition-coupled joint substrate and forces the channel-side response itself to be amplitude-linear. That is the upgrade of paper IV's T2 from MODEL to THEOREM, with zero sorry and no new RS axioms. The eight-tick carrier ties the argument to the T7 octave landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.