physicalChannelResponse_isAmplitudeLinear
plain-language theorem explainer
Every physical channel response induced by substrate access of a ℂ-linear joint dynamics on JointSubstrate is amplitude-linear, with no extra structural hypothesis. Gravity-track authors cite this to discharge the last remaining hypothesis on the density-only no-go. The proof is a one-line application of the Session-124 substrate-access linearity lemma.
Claim. If $R_J : \mathrm{JointSubstrate} \to_{\mathbb{C}} \mathrm{JointSubstrate}$ is a $\mathbb{C}$-linear joint dynamics and $R_C : \mathrm{Signal}_8 \to \mathrm{Signal}_8$ arises from substrate access of $R_J$ (i.e., $R_C\varphi = \chi^{-1}\cdot \mathrm{extractSecond}_{i_0}(R_J(\mathrm{insertFirst}_{\psi_0}\varphi))$ for some matter probe $\psi_0$, channel coordinate $i_0$, and nonzero calibration $\chi$), then $R_C$ is amplitude-linear.
background
Track 2.C of the gravity quantum-channel program asks whether operational channel responses on the joint substrate can be density-only. Under T0–T8 substrate semantics the joint carrier is $\mathrm{JointSubstrate} = \mathrm{Signal}8 \otimes{\mathbb{C}} \mathrm{Signal}_8$ (T7 eight-tick factors with tensor coupling), and joint dynamics is forced $\mathbb{C}$-linear, encoded by the LinearMap type of $R_J$ (substrate lift of Schrödinger linearity).
A physical channel response is not an arbitrary map on $\mathrm{Signal}_8$. It is defined substrate-semantically as arising from substrate access: prepare a matter probe $\psi_0$, apply $R_J$, extract a channel-side coordinate $i_0$, and calibrate by a nonzero scalar $\chi$. That predicate is PhysicalChannelResponseOf, an abbreviation of ArisesFromSubstrateAccess.
Amplitude-linearity (IsAmplitudeLinear) is the structural property that $R_C$ coincides with a $\mathbb{C}$-linear endomorphism of $\mathrm{Signal}8$. Session 124 already showed that any channel arising from substrate access of a linear $R_J$ is automatically amplitude-linear, because the induced map is the composite $\chi^{-1}\cdot(\mathrm{extractSecond}{i_0}\circ R_J\circ\mathrm{insertFirst}_{\psi_0})$.
proof idea
One-line term proof. The hypothesis hPhys : PhysicalChannelResponseOf R_J R_C is definitionally ArisesFromSubstrateAccess R_J R_C. Apply isAmplitudeLinear_channel_of_arisesFromSubstrateAccess to hPhys; that upstream lemma constructs the witnessing $\mathbb{C}$-linear map as the calibrated extract–apply–insert composite and concludes IsAmplitudeLinear R_C. No further case split or T0–T8 unfolding is needed at this site.
why it matters
This is the unconditional closure step of Gravity Track 2.C. It removes IsAmplitudeLinear as a free structural hypothesis on the density-only no-go, deriving it from T0–T8 substrate semantics alone (joint linearity plus substrate-local measurement access).
Downstream it feeds the density-only collapse (density_only_physicalChannelResponse_eq_zero), the explicit linear witness extractor (binaryPhysicalChannelLinearWitness), the certificate bundle (physicalChannelAmplitudeLinearCert), the canonical recognition-update instance, and the Session-127 one-statement package T0T8_unconditional_physical_channel_amplitude_linear_one_statement. Framework landmarks in play: T7 eight-tick octave (carrier dimension), joint $\mathbb{C}$-linearity from the Schrödinger derivation lift, and the forcing chain through T0–T8. No open scaffold remains on this edge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.