PTAStochasticGWStructuralCert
plain-language theorem explainer
Certificate packing three fields: positivity of the RS PTA spectral signature log φ, the structural discriminator proposition (signature strictly positive, unlike inflation's near-zero tilt), and an inhabitant of the master-theorem Track 6.B hypothesis. Cosmologists closing the quantum-gravity master plan cite this bundle. Pure structure definition; no proof body.
Claim. A structural certificate for the RS PTA stochastic gravitational-wave discriminator consists of three data: (i) $0 < \log\varphi$ for the RS PTA spectral signature; (ii) the proposition that this signature is strictly positive (hence distinct from the inflationary slow-roll baseline $n_t \approx 0$); (iii) an inhabitant of the master-theorem hypothesis that the RS PTA stochastic-GW background is distinct from inflation.
background
Track 6.B of the quantum-gravity master plan asks for a structural discriminator between the RS prediction for the PTA stochastic GW background (NANOGrav, EPTA) and the inflationary slow-roll baseline. Inflation gives $n_t \approx 0$ via the tensor consistency relation $r = -8 n_t$. 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 appearing in black-hole echo timing (rungPhaseDelay). The discriminator proposition is simply $0 < \log\varphi$. The master-theorem structure PTAStochasticGWDistinctFromInflation packages a proposition together with a proof that it holds; inhabiting it retires Track 6.B from the conditional master theorem hypothesis list.
This module ships only the algebraic positivity discriminator. Deriving the exact RS spectral tilt from φ-rung primordial structure remains future work.
proof idea
No proof: this is a structure declaration. Its three fields are typed as (1) the inequality $0 < \mathrm{rs_pta_phi_signature}$, (2) the proposition rs_pta_distinct_inflation_prop (definitionally that same inequality), and (3) an instance of the master-theorem hypothesis structure PTAStochasticGWDistinctFromInflation. Downstream, the concrete inhabitant fills the fields with rs_pta_phi_signature_pos, rs_pta_distinct_inflation_prop_holds, and ptaDistinctFromInflationWitness.
why it matters
This certificate is the typed payload for Track 6.B structural closure. Downstream, ptaStochasticGWStructuralCert inhabits it, and ptaStochasticGWStructuralCert_inhabited records Nonempty of the type, feeding the one-statement Track 6.B summary.
The third field is the operational payoff: ptaDistinctFromInflationWitness supplies Gravity.MasterTheorem.PTAStochasticGWDistinctFromInflation, retiring that hypothesis from rs_quantum_gravity_master_conditional (Session 97). Within the forcing chain, the signature rests on φ as the self-similar fixed point (T6) and on the same log-φ phase delay used in the black-hole echo sector.
What remains open is the full physics derivation of the RS PTA spectral shape from φ-rung primordial structure; only the structural positivity band is closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.