channel_eq_zero_of_isAmplitudeLinear_isDensityOnly_unconditional
plain-language theorem explainer
Any amplitude-linear channel response on the eight-tick register that is also density-only must vanish on every signal. Track 2.C gravity cites this as the unconditional density-only collapse: substrate access is no longer an extra hypothesis. The proof is a one-line application of the prior conditional no-go, now free of substrate-access input because amplitude-linearity already forces that access via the universal witness.
Claim. Let $R_C$ map eight-tick signals to eight-tick signals. If $R_C$ is amplitude-linear and density-only, then $R_C(\varphi)=0$ for every signal $\varphi$.
background
Track 2.C studies operational channel responses on the eight-tick recognition register (the finite Signal8 space tied to the T7 octave). An amplitude-linear response is one that is $\mathbb{C}$-linear on amplitudes; a density-only response ignores phase structure and depends only on densities. The joint substrate carries matter-plus-channel data, and substrate access means: prepare a fixed probe, apply one $\mathbb{C}$-linear joint operator, and read a calibrated channel coordinate.
Earlier sessions made the density-only no-go conditional on a substrate-access hypothesis (ArisesFromSubstrateAccess). This module closes that thread: every amplitude-linear channel arises from substrate access of a universal witness of the form $\mathrm{id}\otimes L$ under canonical probe data. Amplitude-linearity and substrate access are therefore equivalent, so the access hypothesis is no longer load-bearing.
The upstream lemma eq_zero_of_isAmplitudeLinear_isDensityOnly already proves vanishing once amplitude-linearity, density-only, and substrate access are all assumed. The present statement drops the access premise because the module supplies it automatically.
proof idea
One-line term proof. Apply the conditional collapse eq_zero_of_isAmplitudeLinear_isDensityOnly to the given amplitude-linearity and density-only hypotheses and the target signal. No extra substrate-access argument appears at the call site; that hypothesis is discharged by the module's universal-witness construction (amplitude-linear channels arise from substrate access), which is why the unconditional wrapper is valid.
why it matters
This is the density-only half of the Session 125 unconditional substrate-semantics closure. It feeds three parents in the same module: the existential no-go not_exists_nontrivial_isAmplitudeLinear_isDensityOnly_unconditional (no nontrivial amplitude-linear density-only channel), the certificate substrateSemanticsUnconditionalCert (field unconditional_density_only_collapse), and the packaged one-statement unconditional_substrate_semantics_one_statement.
In framework terms it finishes retiring the Track 2.C substrate-locality principle: what began as a bare amplitude-linear forcing, then a factor-product hypothesis, then a per-section readout, then a named substrate-access principle, is now a derived equivalence with amplitude-linearity. The eight-tick register (T7) remains the carrier; the result does not reopen T5–T8 forcing, but it removes an RS-internal hypothesis from the gravity quantum-channel chain so the density-only obstruction holds on substrate semantics alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.