pta_stochastic_gw_one_statement
plain-language theorem explainer
Packages the Track 6.B structural discriminator into one conjunction: the RS PTA spectral signature log φ is strictly positive, the inflation-distinctness proposition holds, and the master-theorem hypothesis PTAStochasticGWDistinctFromInflation is inhabited. Cosmologists and QG auditors cite it as the closed algebraic form of the PTA stochastic-GW claim. The proof is a three-component term that assembles positivity of log φ, the discriminator proposition, and the witness structure.
Claim. The following three facts hold simultaneously: (i) $0 < \log\varphi$, where $\log\varphi$ is the RS PTA spectral signature (per-rung phase delay); (ii) the structural discriminator proposition that this signature is strictly positive (hence distinct from the inflationary slow-roll baseline $n_t \approx 0$); (iii) the master-theorem hypothesis structure asserting RS PTA stochastic-GW distinctness from inflation is inhabited.
background
Track 6.B of the quantum-gravity master plan asks for a structural discriminator between the RS prediction for a pulsar-timing-array stochastic gravitational-wave background and the inflationary slow-roll baseline. Inflation, via the tensor consistency relation $r = -8 n_t$, predicts a nearly scale-invariant tensor tilt $n_t \approx 0$. RS instead carries a φ-rational spectral signature.
That signature is defined as the per-rung phase delay $\log\varphi \approx 0.481$, the same invariant that appears as the rung phase delay in the black-hole-echoes-from-bounce sector, transposed here to the primordial GW spectrum. The discriminator proposition is simply the statement $0 < \log\varphi$. Positivity follows from $\varphi > 1$ and the standard positivity of the real logarithm on $(1,\infty)$.
The Gravity master theorem exposes a hypothesis structure PTAStochasticGWDistinctFromInflation (a proposition together with a proof that it holds). An explicit witness packages the local discriminator proposition and its proof into that structure, retiring the PTA clause from the conditional master theorem's open hypothesis list. Empirical match to NANOGrav/EPTA data is deliberately left as a separate falsifier-register obligation.
proof idea
Term-mode triple constructor. The first conjunct is the already-proved positivity theorem for the RS PTA signature: unfold the definition $\log\varphi$ and apply $\log$-positivity on $1 < \varphi$. The second conjunct is the discriminator proposition, which is definitionally $0 < \log\varphi$ and is discharged by that same positivity theorem. The third conjunct is nonemptiness of the master-theorem hypothesis structure; it is witnessed by the structure inhabitant whose fields are exactly the discriminator proposition and its proof. No further rewriting or case analysis is required.
why it matters
This is the one-statement closure of Cosmology Track 6.B in structural form. The master plan requires landing an RS PTA spectral prediction distinct from inflation and recording a falsifier band; the module ships the algebraic half (strict positivity of $\log\varphi$ versus $n_t \approx 0$) and inhabits the corresponding Gravity master-theorem hypothesis, removing it from the conditional master theorem's open list.
Downstream usage is presently empty in the graph: the declaration is a terminal packaging theorem for auditors and for any future unconditional master-theorem assembly that consumes the inhabited hypothesis. Framework landmarks in play are the golden ratio $\varphi$ (T6 fixed point) and the φ-ladder phase structure shared with black-hole echo delays. The exact RS spectral tilt derived from φ-rung primordial structure, and the empirical NANOGrav/EPTA match, remain open; only the structural positivity discriminator is closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.