rs_pta_distinct_inflation_prop
plain-language theorem explainer
Defines the structural PTA discriminator as the conjunction that the RS stochastic signature φ^{-44} is strictly positive and unequal to the pure-inflation zero baseline. Gravity and cosmology bridge authors cite it when packaging the master-theorem input PTAStochasticGWDistinctFromInflation. The body is a two-literal Prop abbreviation over the rung-44 scale and the zero proxy.
Claim. The structural PTA discriminator asserts $0 < \varphi^{-44}$ and $\varphi^{-44} \neq 0$, where $\varphi^{-44}$ is the RS stochastic-background signature at rung 44 and $0$ is the pure-inflation zero-baseline proxy.
background
Gravity Track 6.B isolates the algebraic half of the PTA stochastic-background discriminator. The RS signature is the same positive rung-44 scale $\varphi^{-44}$ used elsewhere in the gravity/cosmology bridge; the inflation side is represented by a pure zero baseline proxy. Module text is explicit that no PTA dataset is attached and that observational separation remains empirical work.
Upstream, rs_pta_stochastic_phi_signature is defined as $\mathrm{Constants.phi}^{(-44)}$, and inflation_zero_stochastic_baseline is the real constant $0$. The cosmology twin module states the same discriminator idea as positivity of the RS PTA signature against an approximately zero slow-roll prediction. Together those two constants turn the discriminator into a pure real inequality pair.
proof idea
Not a proof: a Prop definition. The body is the conjunction of strict positivity of the rung-44 RS signature with inequality against the inflation zero baseline. Downstream theorems discharge it by proving $\varphi^{-44} > 0$ (hence unequal to $0$).
why it matters
This Prop is the named payload of the master-theorem hypothesis input PTAStochasticGWDistinctFromInflation. Downstream, ptaDistinctFromInflationWitness and PTAStochasticGWStructuralCert inhabit that interface and retire the PTA clause from the conditional quantum-gravity master theorem. The Track 6.B one-statement packages positivity, this discriminator, and Nonempty of the master input in one place.
Framework role is structural only: a $\varphi$-ladder scale (rung 44) forced distinct from a zero inflation proxy, not a claim of current NANOGrav/EPTA separation. Empirical spectral fitting stays on the falsifier register.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.