ptaSignalModelWitness
plain-language theorem explainer
Packages the RS pulsar-timing-array stochastic GW prediction as a typed MasterTheorem witness of structural distinction from the inflationary null baseline. Cited by the unconditional PTA witness and the five-channel QG signal-model certificate. Construction is a structure instance that feeds the named PTA channel's proved inequality and positive absolute separation into the Track 6.B interface.
Claim. A witness that the Recognition Science PTA stochastic gravitational-wave background is structurally distinct from the inflationary baseline: writing $p$ for the RS PTA prediction and $n$ for the inflationary null baseline on the PTA observation channel, one has $p \neq n$ and $|p-n|>0$.
background
This module equips each observational channel on the quantum-gravity falsifier surface with a typed signal model: an observable, an RS prediction, a GR/inflation/ΛCDM null baseline, current sensitivity, a named future falsifier threshold, and a separation theorem. The five channels are PTA stochastic background, EHT shadow/ring, S-star orbits near Sgr A*, Cassini/Shapiro delay, and ringdown echoes.
The PTA channel carries a concrete RS prediction and an inflationary null baseline, together with proofs that the two values are unequal and that their absolute difference is strictly positive. The MasterTheorem structure PTAStochasticGWDistinctFromInflation is the Track 6.B hypothesis interface: a proposition asserting RS PTA stochastic-GW distinction from inflationary $n_t$ predictions, plus a proof field that the proposition holds. This definition supplies that interface from the named channel model rather than from an ad-hoc band.
proof idea
One-line structure instance. The proposition field is set to the conjunction "PTA RS prediction ≠ null baseline and absolute difference strictly positive." The proof field is the pair of channel lemmas establishing inequality and positive separation. No further tactics or algebraic work.
why it matters
Closes the PTA half of the typed QG signal-model layer: the MasterTheorem Track 6.B interface is no longer an open bare hypothesis but is inhabited by a channel-backed witness. Downstream, canonicalPTADistinctWitness is defined as this object ("canonical theorem-built PTA witness, strengthened to a typed observation-channel signal model with formula-level separation"). It is also a field of the module certificate and feeds the one-statement theorem that five typed channels each carry formula-level RS predictions, null baselines, and proved separation, with nonempty PTA and strong-field MasterTheorem witnesses. In the broader RS gravity program this is the PTA leg of the D5 falsifier surface against inflationary stochastic GW backgrounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.