rs_pta_observable_band
plain-language theorem explainer
Open real interval centered on the RS PTA stochastic scale φ^{-44}, namely (φ^{-44}/2, 3φ^{-44}/2). Gravity and cosmology workers cite it when stating that the RS stochastic GW signature sits inside a positive observable window while pure inflation zero baselines sit outside. The body is a pure two-sided inequality predicate on ℝ, not a proved theorem.
Claim. A real number $x$ lies in the RS PTA observable band when $\frac{1}{2}\varphi^{-44} < x < \frac{3}{2}\varphi^{-44}$, where $\varphi$ is the golden-ratio fixed point and $\varphi^{-44}$ is the structural RS PTA stochastic-background signature at rung 44.
background
Module Gravity Track 6.B isolates the algebraic part of a PTA stochastic-background discriminator. The structural RS signature is the same positive rung-44 scale $\varphi^{-44}$ used elsewhere in the gravity/cosmology bridge; a pure inflation zero baseline is then structurally distinct from that signature.
Upstream, the stochastic signature is defined as Constants.phi ^ (-44), the phi-ladder value at rung 44. The band is the theorem-facing open window of half-width equal to half that signature, so the signature itself is the midpoint.
The module does not attach a PTA dataset or claim present-day observational separation. Dataset sensitivity and channel-specific spectral fitting remain empirical work; Lean only supplies the algebraic inhabitant for the master-theorem input on PTA stochastic GW distinct from inflation.
proof idea
Definition only: no proof obligations. The predicate is the conjunction of the two strict inequalities $x > s/2$ and $x < 3s/2$ with $s = \varphi^{-44}$. Downstream theorems unfold this def and discharge the inequalities by positivity of $s$ (via nlinarith after the positivity lemma for the signature).
why it matters
Gives the concrete positive window used by the observable-band discriminator. Downstream, the signature is proved to lie inside the band, every explicit inflationary zero-baseline is proved to lie outside it, and those two facts are packaged as the proposition that the RS rung-44 signature is in-band while the inflationary family is entirely out-of-band.
That package is the algebraic core feeding the master-theorem slot PTAStochasticGWDistinctFromInflation. It sits on the gravity/cosmology bridge that reuses the phi-ladder (rung 44 here) rather than introducing a free PTA amplitude. Empirical PTA separation remains open; this def only fixes the structural band geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.