ptaChannel
plain-language theorem explainer
The PTA channel packages RS's prediction for the nanohertz stochastic gravitational-wave background as a typed observation-channel signal model: spectral amplitude h_c equals φ^{-44}, against a pure-inflation null of zero. Anyone citing the QG falsifier matrix or the PTA-vs-inflation distinctness witness uses this record. The two side conditions are short positivity arguments from φ > 0 and integer powers.
Claim. The PTA observation channel is the signal model with name "PTA stochastic background", observable equal to the spectral amplitude $h_c$ at $f \sim \mathrm{nHz}$, RS prediction $\varphi^{-44}$, and null baseline $0$, together with proofs that $\varphi^{-44} \neq 0$ and $0 < |\varphi^{-44} - 0|$.
background
This module builds typed signal models for the five channels on the quantum-gravity falsifier surface (PTA, EHT, S-star, Cassini, ringdown). Each model is an ObservationChannelSignalModel: a named channel, a measured observable string, an RS real prediction, a GR/inflation/ΛCDM null baseline, and two proofs that the prediction is strictly separated from the null.
The PTA entry targets the stochastic gravitational-wave background at nanohertz frequencies. Recognition Science places the amplitude on the φ-ladder at rung 44, so the predicted spectral amplitude is $\varphi^{-44} > 0$. Pure inflation supplies a zero stochastic background at the relevant band, which is the null baseline here.
Constants come from the RS constants bundle (phi is the golden ratio forced at T6). The surrounding Master Theorem and PTA structural imports supply the broader claim that RS PTA is distinct from inflation; this definition only freezes the numerical channel data those witnesses consume.
proof idea
Field assignments are direct: name and observable are string literals; rsPrediction is Constants.phi ^ (-44); nullBaseline is 0.
rsPrediction_ne_null assumes equality to zero, invokes zpow_pos phi_pos (-44) (positive base to any integer power stays positive), and closes by linarith.
separation_pos rewrites $|\varphi^{-44}-0|$ via sub_zero and abs_of_pos on the same positivity fact, then returns that positive power again. No external PTA lemma is needed beyond φ-positivity and Mathlib integer powers.
why it matters
This is the first of the five QG channels collected in qgChannels. Downstream, ptaSignalModelWitness lifts the two separation proofs into the Master Theorem interface PTAStochasticGWDistinctFromInflation, so the structural claim "RS PTA prediction is distinct from the inflationary zero baseline" is witnessed by a named channel model rather than bare reals.
In the Recognition framework the rung-44 scale is the φ-ladder placement of the nanohertz stochastic background; the prediction $\varphi^{-44}$ is the concrete RS number that must sit above the inflationary null for the D5 falsifier surface. The module status is structural (0 sorry, 0 RS-internal axiom): this definition closes the PTA slot of that surface without adding hypotheses.
It does not itself prove detectability or current sensitivity bounds; those live in sibling fields and future-threshold scaffolding elsewhere in the gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.