ObservationChannelSignalModel
plain-language theorem explainer
A typed record for one quantum-gravity observation channel: named observable, RS numerical prediction, null (GR/inflation) baseline, and two positivity/separation witnesses that the prediction differs from the baseline. Gravity and QG-phenomenology workers cite it when building the five-channel D5 falsifier matrix. It is a pure structure definition; instances discharge the inequalities by direct arithmetic on φ-powers.
Claim. An observation-channel signal model is a 6-tuple $(N, O, r, b, h_{\neq}, h_{>})$ where $N$ and $O$ are strings (channel name and measured quantity), $r,b\in\mathbb{R}$ are the RS prediction and null baseline, $h_{\neq}$ asserts $r\neq b$, and $h_{>}$ asserts $0<|r-b|$.
background
Module Gravity.QGObservableSignalModels packages the D5 quantum-gravity falsifier surface as typed Lean data. Status is structural: zero sorry, zero RS-internal axioms. Each channel must carry an RS-side number, a GR/inflation/ΛCDM null, and a proof that the two are strictly separated.
The φ-ladder supplies the numerical scale. Cosmology defines scale k := φ^k; several channels use the rung-44 amplitude $φ^{-44}$, while the ringdown channel uses the Berry threshold $φ^{-1}$. Constants live in RS-native units with $c=1$ and $ħ=φ^{-5}$.
The structure is deliberately thinner than the module prose sketch: it records name, observable, prediction, baseline, and the two separation witnesses. Sensitivity bands and named 2026–2035 thresholds appear only in surrounding narrative, not in this type.
proof idea
No proof body: this is a structure declaration. Fields rsPrediction_ne_null and separation_pos are Prop-valued; each concrete channel instance (PTA, EHT, S-star, Cassini, ringdown) fills them with short by-proofs that $φ^{-n}\neq 0$ (or $φ^{-1}\neq 0$) and that the absolute difference is positive. Downstream list qgChannels just assembles the five instances.
why it matters
This type is the common carrier for the five QG falsifier channels that the module collects into qgChannels: PTA stochastic background at $φ^{-44}$, EHT shadow-radius deviation $2φ^{-44}$, S-star periapsis residual $φ^{-44}$, Cassini/Shapiro residual $3φ^{-44}$, and ringdown echo ratio $φ^{-1}$.
Downstream docs make the scientific cut explicit. PTA contrasts a positive RS amplitude against pure inflation's zero background; EHT and S-star contrast positive RS residuals against Kerr/1PN–2PN GR zeros; Cassini does the same for Shapiro delay; ringdown pins the unique RS value $φ^{-1}\approx 0.618$ against classical GR's zero echo amplitude.
In the broader Recognition chain the rung-44 scale and the $φ^{-1}$ Berry threshold sit on the forced φ-ladder (T5–T6). The structure does not itself prove those landmarks; it only forces every published channel to state a separated numerical claim that later certificates (ptaSignalModelWitness, strongFieldSignalModelWitness, QGObservableSignalModelsCert) can audit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.