qgObservableSignalModelsCert
plain-language theorem explainer
assembles a single certificate that the five typed QG observation channels (PTA, EHT, S-star, Cassini, ringdown) each separate RS predictions from null baselines, and packages the PTA and strong-field MasterTheorem witnesses. Gravity and QG-falsifier authors cite it as the inhabited D5 signal-model bundle. The body is a pure structure instance wiring four already-proved fields.
Claim. There exists a certificate asserting: (i) the QG observation-channel list has length $5$; (ii) for every channel $c$ in that list, $0 < |c^{\mathrm{RS}} - c^{\mathrm{null}}|$; (iii) a PTA stochastic gravitational-wave witness that the RS prediction is distinct from the inflationary baseline; (iv) a strong-field witness that EHT, S-star, Cassini (and ringdown) RS predictions are distinct from the GR zero baseline.
background
The module builds typed signal models for the D5 QG falsifier surface. Each channel record carries an observable, an RS prediction (or band), a GR/inflation/ΛCDM null baseline, current sensitivity, a named 2026–2035 falsifier threshold, and a separation proof that RS and null differ by more than that threshold.
The five channels are PTA stochastic background, EHT shadow/ring, S-star orbits near Sgr A*, Cassini/Shapiro delay, and ringdown echoes. The certificate structure demands four fields: exact channel count five, universal positive absolute separation on the channel list, a PTA witness of type “stochastic GW distinct from inflation,” and a strong-field witness of type “strong-field tests distinct from GR.”
Upstream, channel-count is reflexivity on the list length; universal separation is the pointwise separation_pos of each channel; the PTA and strong-field witnesses are thin wrappers that rephrase those inequalities into the MasterTheorem interfaces.
proof idea
One-line structure construction. Field channel_count is filled by the reflexivity theorem that the channel list has length five. Field all_separated is the universal quantification already proved by applying each channel’s positive-separation lemma. Field pta_witness is the pre-built PTA signal-model witness (RS prediction unequal to null and positive absolute gap). Field strong_field_witness is the pre-built strong-field witness (EHT, S-star, Cassini, ringdown each unequal to the GR baseline). No new arithmetic is performed.
why it matters
This definition is the concrete inhabitant that discharges Nonempty for the D5 signal-model certificate, so downstream one-statement summaries can assert that five typed channels carry formula-level RS predictions separated from null baselines. It sits in the Gravity domain as the structural (zero-sorry) packaging of PTA and strong-field MasterTheorem interfaces into a single observation-channel bundle.
Within Recognition Science it operationalizes the QG falsifier surface: each channel’s separation theorem is exactly the claim that RS is observationally distinguishable from GR/inflation on that probe. It does not itself invoke the forcing chain (T0–T8) or the RCL, but it is the gravity-side place where those structural predictions become channel-level, thresholded tests for 2026–2035.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.