PTAStructuralCert
plain-language theorem explainer
A certificate structure that packages four algebraic facts for the PTA stochastic-GW discriminator: positivity of the RS rung-44 scale φ^{-44}, its inequality with the pure-inflation zero baseline, the structural discriminator proposition, and an inhabitant of the master Track 6.B hypothesis. Gravity and cosmology auditors cite it when wiring the algebraic side of the PTA vs inflation separation. As a structure definition it has no proof body; inhabitants discharge the fields with prior lemmas.
Claim. A certificate consists of four packed facts: (i) $0 < \varphi^{-44}$; (ii) $\varphi^{-44} \neq 0$ (the pure-inflation zero baseline); (iii) the structural discriminator proposition $0 < \varphi^{-44} \land \varphi^{-44} \neq 0$; (iv) an inhabitant of the master Track 6.B hypothesis that the RS PTA stochastic-GW background is distinct from inflationary $n_t$ predictions.
background
Gravity Track 6.B isolates the theorem-grade algebraic core of a PTA stochastic-background discriminator. Recognition Science assigns a structural PTA signature at the rung-44 scale on the $\varphi$-ladder: $\varphi^{-44}$. The pure-inflation slow-roll proxy used here is the zero baseline $0$. Because the RS scale is strictly positive, it is automatically distinct from that baseline.
The local discriminator proposition asserts both positivity and inequality with zero. Upstream, the master gravity theorem exposes an open Track 6.B hypothesis structure whose single field is a proposition that the RS PTA stochastic-GW spectrum differs from inflationary $n_t$ predictions; this module supplies the algebraic inhabitant for that input. No PTA dataset or spectral fit is attached: the content is purely structural.
proof idea
No proof body: the declaration is a structure (record type) with four fields. Field types are the positivity inequality $0 < \varphi^{-44}$, the inequality with the zero baseline, the local discriminator proposition (conjunction of those two facts), and the master Track 6.B hypothesis structure. Downstream, a single noncomputable value fills the fields by applying the positivity lemma, the inequality lemma, the discriminator-holds lemma, and the master-hypothesis witness.
why it matters
This certificate is the typed carrier for the algebraic half of Track 6.B. Downstream, ptaStructuralCert inhabits it and ptaStructuralCert_inhabited proves non-emptiness, giving a one-line structural statement that the PTA stochastic signature is positive and therefore distinct from the inflation zero baseline. That closes the theorem-grade input demanded by the master gravity hypothesis on PTA stochastic GW vs inflation. Framework-wise it sits on the $\varphi$-ladder (rung 44) used across the gravity/cosmology bridge; it does not touch T0–T8 forcing, RCL, or the alpha band. Dataset sensitivity and channel-specific spectral fitting remain open empirical falsifier work outside Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.