qgChannels
plain-language theorem explainer
Collects the five quantum-gravity falsifier observation channels into one list of typed signal models. Each entry pairs an RS prediction with a GR or inflation null baseline and a proved nonzero separation. Downstream length, separation, and D5 certificate theorems quantify over this list. The body is a five-element list literal of the named channel definitions.
Claim. Define the list of five observation-channel signal models as the PTA stochastic-background channel, the EHT shadow/ring channel, the S-star periapsis channel, the Cassini/Shapiro delay channel, and the ringdown-echo channel, in that order.
background
Module Gravity.QGObservableSignalModels builds typed signal models for the D5 QG falsifier surface. Status is structural: zero sorry, zero RS-internal axioms. Each channel packages a measured observable, an RS prediction, a GR/inflation/ΛCDM null baseline, sensitivity metadata, and a separation proof that the RS value differs from the null by more than the named falsifier threshold.
The carrier type is ObservationChannelSignalModel: channel name, observable string, real RS prediction and null baseline, plus proofs that the two reals are unequal and that their absolute difference is positive. The five concrete channels are: PTA spectral amplitude $h_c$ at nHz with RS value $\varphi^{-44}$ versus inflation zero; EHT shadow-radius fractional deviation $2\varphi^{-44}$ versus Kerr zero; S-star periapsis timing residual $\varphi^{-44}$ versus post-Newtonian GR zero; Cassini/Shapiro residual $3\varphi^{-44}$ versus PPN zero; ringdown echo amplitude ratio $\varphi^{-1}$ versus classical no-echo zero.
proof idea
Definition by list literal. No tactics: the value is exactly the five already-constructed channel terms in fixed order (PTA, EHT, S-star, Cassini, ringdown). Each element is a complete ObservationChannelSignalModel record built upstream with its own inequality proofs.
why it matters
This list is the single enumeration the D5 observation-channel layer quantifies over. qgChannels_length pins the count at five by reflexivity. all_channels_separated states that every member has positive absolute separation between RS prediction and null baseline, discharging via the per-channel separation_pos field. The certificate structure QGObservableSignalModelsCert requires both the length fact and the universal separation fact, and routes PTA and strong-field master-theorem witnesses through the same channel models. The one-statement theorem packages length, separation, and nonempty PTA/strong-field witnesses as the public D5 claim: five typed channels with formula-level RS predictions, null baselines, and proved separation. The rung-44 $\varphi$-ladder scale and the Berry-scale $\varphi^{-1}$ echo ratio sit on the RS constants ladder (phi forced at T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.