QGObservableSignalModelsCert
plain-language theorem explainer
Certificate structure for the five quantum-gravity observation-channel signal models. It packages exact channel count, strict RS-vs-null separation on every channel, and the two MasterTheorem witnesses (PTA stochastic GW vs inflation; strong-field tests vs GR). Gravity and QG-falsifier work cites it as the typed bundle behind the inhabited cert. The declaration is a pure structure, not a proved theorem.
Claim. A certificate consists of four data: (i) the list of QG falsifier channels has length $5$; (ii) for every channel $c$ in that list, $|\mathrm{RS\_prediction}(c) - \mathrm{null\_baseline}(c)| > 0$; (iii) a witness that the RS PTA stochastic gravitational-wave background is distinct from inflationary $n_t$ predictions; (iv) a witness that RS strong-field predictions (EHT shadow, S-star orbits, Cassini/Shapiro, ringdown) are distinct from pure GR.
background
This module equips each observational channel on the QG falsifier surface with a typed signal model: measured observable, RS prediction or band, GR/inflation/ΛCDM null baseline, current sensitivity, future falsifier threshold (2026–2035), and a separation theorem that RS and null differ by more than that threshold. Status is structural: zero sorry, zero RS-internal axiom.
The five channels collected in qgChannels are PTA stochastic background, EHT shadow/ring, S-star orbits near Sgr A*, Cassini/Shapiro delay, and ringdown echoes. Upstream, PTAStochasticGWDistinctFromInflation and StrongFieldTestsDistinctFromGR are Track 6.B/6.C hypothesis interfaces in the gravity MasterTheorem: each is a Prop-carrying structure whose holds field is currently open at the master level, while this module supplies concrete channel-level witnesses that inhabit them.
Separation is the elementary condition that the absolute difference of RS prediction and null baseline is strictly positive on every listed channel.
proof idea
No proof body: the declaration is a structure (four fields). Inhabitation is deferred to the sibling definition that fills channel_count by the length lemma on the five-channel list, all_separated by the universal separation lemma over that list, pta_witness by the PTA signal-model witness, and strong_field_witness by the strong-field signal-model witness (conjunction of four channel-level RS≠null facts for EHT, S-star, Cassini, ringdown).
why it matters
This is the master cert type for §5 of the QG observable-signal-models module. Downstream, qgObservableSignalModelsCert builds a concrete value of the structure, and qgObservableSignalModelsCert_inhabited records Nonempty of that type, giving the one-statement packaging: five typed channels each carry formula-level RS predictions separated from null baselines.
In the broader Recognition gravity program it sits under the MasterTheorem tracks that demand PTA stochastic GW distinct from inflation and strong-field tests distinct from GR. Those master hypotheses remain open as abstract Props; this cert is the structural surface that ties them to named observational channels (PTA, EHT, S-stars, Cassini, ringdown) rather than free-floating claims. It does not itself close the open Track 6.B/6.C questions; it organizes the channel-level evidence those tracks must eventually discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.