qg_observable_signal_models_one_statement
plain-language theorem explainer
Five typed QG observation channels (PTA, EHT, S-star, Cassini, ringdown) each separate RS predictions from GR/inflation null baselines by a positive gap. The statement also supplies nonempty master-theorem witnesses for PTA-vs-inflation and strong-field-vs-GR. Gravity auditors cite it as the single D5 packaging of channel models. The proof is a four-component term pairing length, universal separation, and two channel witnesses.
Claim. The list of QG observation-channel signal models has length $5$; every channel $c$ in that list satisfies $0 < |c_{\mathrm{RS}} - c_{\mathrm{null}}|$; and there exist witnesses that the RS PTA stochastic-GW spectrum is distinct from inflationary $n_t$ predictions and that RS strong-field tests are distinct from pure GR.
background
This module builds typed signal models for the QG falsifier surface (D5). Each ObservationChannelSignalModel carries an observable, an RS prediction, a GR/inflation/ΛCDM null baseline, current sensitivity, a named future falsifier threshold (2026–2035), and a proof that RS and null are separated beyond that threshold.
The five channels are PTA stochastic background, EHT shadow/ring, S-star orbits near Sgr A*, Cassini/Shapiro delay, and ringdown echoes, collected as qgChannels. Upstream, all_channels_separated states that every listed channel has positive $|\mathrm{rsPrediction}-\mathrm{nullBaseline}|$. The master-theorem structures PTAStochasticGWDistinctFromInflation (Track 6.B) and StrongFieldTestsDistinctFromGR (Track 6.C) are hypothesis-shaped records whose holds fields are currently open at the master level; this module supplies concrete channel-model witnesses that inhabit them.
Local status is structural: zero sorry, zero RS-internal axioms.
proof idea
Term-mode four-tuple. First component is qgChannels_length (list of five channels). Second is all_channels_separated, which reduces pointwise to each channel's separation_pos. Third wraps ptaSignalModelWitness as a nonempty inhabitant of PTAStochasticGWDistinctFromInflation, using PTA channel inequality and positive separation from the inflationary zero baseline. Fourth wraps strongFieldSignalModelWitness likewise for StrongFieldTestsDistinctFromGR. No further tactics.
why it matters
Packages the D5 observation-channel layer into one citation target: five formula-level RS-vs-null separations plus routing of PTA and strong-field master-theorem witnesses through those models. Downstream use count is presently zero; the declaration is a terminal cert for the module rather than an intermediate lemma.
It sits under Gravity's master-theorem tracks 6.B and 6.C (PTA stochastic GW distinct from inflation; strong-field tests distinct from pure GR). Those master structures remain OPEN as full physics claims; what is proved here is structural inhabitance via named channel models with positive prediction–baseline gaps. In the broader RS gravity program this is the typed falsifier surface for near-term instruments (PTA, EHT, S-stars, Cassini-class delay, ringdown), not a derivation of the mass ladder or forcing chain (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.