PTAStochasticGWDistinctFromInflation
plain-language theorem explainer
Hypothesis bundle for Track 6.B: the RS pulsar-timing-array stochastic GW background is spectrally distinct from inflationary tensor-tilt predictions. The conditional quantum-gravity master theorem takes an inhabitant of this structure as one of five open inputs. Pure definitional packaging: a named proposition plus a proof field that it holds.
Claim. A record packing a proposition $P$ asserting that the Recognition Science PTA stochastic gravitational-wave background spectrum differs from inflationary $n_t$ predictions, together with a proof that $P$ holds.
background
The Gravity MasterTheorem module authors the twelve-clause quantum-gravity master statement (Track 7.A). Eight clauses are closed from existing theorems; five remain as hypothesis inputs. This structure is the Track 6.B input: RS PTA stochastic-GW spectrum distinct from inflation.
In RS, the PTA spectral signature is tied to $\log\varphi$ (strictly positive), whereas slow-roll inflation predicts a nearly scale-invariant tensor tilt $n_t\approx 0$. The structure does not encode the spectral formula itself; it only packages the distinctness claim as a dischargeable hypothesis for the master conjunction.
Upstream cosmology work (PTAStochasticGWStructural) later supplies the concrete proposition and a witness that inhabits this type, retiring the hypothesis from the conditional master list once Track 6.B closes structurally.
proof idea
No proof body: this is a structure definition with two fields. The first field is an arbitrary proposition standing for the RS-vs-inflation PTA distinctness claim; the second field requires a term of that proposition. Downstream modules inhabit it by assigning a concrete Prop (e.g. positivity of the $\log\varphi$ PTA signature) and a proof of that Prop.
why it matters
One of the five open gates on rs_quantum_gravity_master_conditional. An inhabitant is required alongside classical continuum/Bianchi, unconditional amplitude linearity, Page-curve derivation, and strong-field GR discriminators before the master statement can be assembled.
Downstream, ptaDistinctFromInflationWitness builds an inhabitant, and pta_stochastic_gw_one_statement packages positivity of the RS PTA $\log\varphi$ signature, the distinctness Prop, and nonemptiness of this structure as the Track 6.B one-statement. The structural cert PTAStochasticGWStructuralCert carries the same witness. Empirical match to NANOGrav/EPTA remains a separate falsifier-register obligation, not discharged here.
Framework link: the spectral offset is a $\varphi$-ladder signature (T6 fixed point), not a free inflationary parameter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.