rs_pta_distinct_inflation_prop
plain-language theorem explainer
Defines the structural PTA discriminator as the proposition that the RS spectral signature log φ is strictly positive. Cosmologists and QG auditors cite it when separating the RS φ-rung GW background from the inflationary slow-roll baseline n_t ≈ 0. It is a one-line Prop abbreviation of the positivity claim, not a proved theorem.
Claim. The structural discriminator proposition asserts that the RS PTA spectral signature is strictly positive: $0 < \log\varphi$, where $\varphi$ is the golden ratio. This is the algebraic stand-in for distinctness from the inflationary slow-roll prediction $n_t \approx 0$.
background
Track 6.B of the quantum-gravity master plan asks for a structural discriminator between the RS stochastic GW background and the inflationary slow-roll baseline. Pulsar-timing arrays (NANOGrav, EPTA) report a stochastic background; RS claims a φ-rung primordial imprint, while slow-roll inflation gives a nearly scale-invariant tensor spectrum with $n_t \approx 0$ from the consistency relation $r = -8 n_t$.
The RS signature used here is the per-rung phase delay $\log\varphi \approx 0.481$, the same φ-rational invariant that appears as the black-hole echo rung phase delay. It is defined as Real.log Constants.phi. This module ships only the algebraic positivity of that signature; the full RS spectral tilt from φ-rung structure is deferred.
A sibling Gravity.PTAStructural definition packages positivity together with an explicit inequality against a zero inflation baseline. The cosmology-track form collapses the discriminator to the single inequality $0 < \log\varphi$, which already separates RS from the approximately-zero inflationary proxy.
proof idea
Definitional abbreviation, not a proof. The proposition is identified with the atomic inequality $0 < \mathrm{rs_pta_phi_signature}$, and that signature is itself the real logarithm of the golden ratio. Discharge of the proposition is left to the companion theorem that proves $\log\varphi > 0$; the definition only names the claim.
why it matters
This Prop is the payload field of the master-theorem hypothesis input PTAStochasticGWDistinctFromInflation. The witness ptaDistinctFromInflationWitness packages it with the positivity proof and thereby retires that hypothesis from the conditional quantum-gravity master theorem.
Downstream, the Track 6.B one-statement theorem conjoins signature positivity, this discriminator, and nonemptiness of the master hypothesis type. The structural certificate structure records the same three facts. Parallel Gravity.PTAStructural witnesses reuse the same pattern.
Within the Recognition framework this is the algebraic half of the PTA falsifier band: a positive φ-rational offset against inflation's near-zero tensor tilt. Exact spectral shape and NANOGrav/EPTA match remain separate empirical obligations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.