all_channels_separated
plain-language theorem explainer
Every channel in the five-channel QG falsifier list has strictly positive absolute gap between its Recognition Science prediction and the GR/inflation null baseline. Gravity and QG auditors cite it when packaging D5 separation. The proof is a one-line term that projects each channel record's built-in positivity field.
Claim. For every observation-channel signal model $c$ in the five-channel QG list (PTA, EHT, S-star, Cassini, ringdown), $|\mathrm{RS}(c) - \mathrm{null}(c)| > 0$, where $\mathrm{RS}(c)$ is the RS-predicted value or band and $\mathrm{null}(c)$ is the GR / inflation / $\Lambda$CDM baseline.
background
This module equips the QG falsifier surface (D5) with typed signal models. Each ObservationChannelSignalModel carries an observable, an RS prediction, a GR/inflation/ΛCDM null baseline, current sensitivity, a named 2026–2035 falsifier threshold, and a separation theorem asserting that the RS value and the null baseline differ by more than that threshold.
The five channels are collected as a fixed list: PTA stochastic background, EHT shadow/ring, S-star orbits near Sgr A*, Cassini/Shapiro delay, and ringdown echoes. The list is the universe over which the universal separation claim is quantified.
Local status is structural: zero sorry and no RS-internal axioms. Upstream gravity master theorems and structural PTA/strong-field modules supply the per-channel separation facts that each record stores as a field; this theorem only lifts those facts to the whole list.
proof idea
One-line term proof. Introduce an arbitrary channel $c$ in the five-channel list and discard membership; return the channel's own separation_pos field, which already asserts $0 < |\mathrm{rsPrediction} - \mathrm{nullBaseline}|$. No extra algebra or case split on channel identity is required.
why it matters
This is the universal separation leg of the D5 observation-channel package. Downstream, the certificate record plugs it in as all_separated, and the one-statement theorem conjoins list length five, this separation claim, and nonempty PTA and strong-field master-theorem witnesses.
In the Recognition framework it turns per-channel structural distinctness (RS prediction off the GR/inflation baseline) into a single list-level fact auditors can cite without opening each channel. It does not itself derive the mass ladder, $J$-cost, or T0–T8 forcing; it only packages already-proved channel separations for the QG falsifier surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.