qgObservableSignalModelsCert_inhabited

This module builds typed signal models for the D5 QG falsifier surface. Each channel records an observable, an RS prediction, a GR/inflation/ΛCDM null baseline, current sensitivity, a named 2026–2035 falsifier threshold, and a separation theorem 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 bundles four facts: channel count equals five; every listed channel has strictly positive absolute RS–null gap; a PTA master-theorem witness that the stochastic GW signal is distinct from inflation; and a strong-field master-theorem witness that EHT, S-star, and Cassini RS predictions differ from the GR zero baseline. A concrete value of that structure is already assembled from the channel list length lemma, the all-channels-separated lemma, and the PTA and strong-field signal-model witnesses.

One-line term proof. Nonemptiness is witnessed by the already-constructed certificate value, which fills the four structure fields from the in-module length, separation, PTA-witness, and strong-field-witness definitions. No further tactics or case analysis.

Gives a single inhabited certificate that the QG observation-channel layer is fully populated and separated from null baselines. That is the structural one-statement for D5 signal models: five typed channels, formula-level RS predictions, GR/inflation nulls, and proved separation, with PTA and strong-field master-theorem witnesses routed through the channel models. Downstream consumers can assume the certificate type is nonempty without rebuilding the channel list. No used-by edges are recorded yet; the declaration closes the existence side of the module’s structural theorem (0 sorry, 0 RS-internal axiom) rather than feeding a named parent in this graph snapshot.