ptaStructuralCert
plain-language theorem explainer
Packages the algebraic PTA stochastic-background discriminator: the RS signature φ^{-44} is positive, unequal to the zero inflation baseline, and supplies the master-theorem witness. Gravity and cosmology auditors cite it as the single certificate inhabitant for Track 6.B. Construction is a four-field structure assembly from prior positivity and inequality lemmas.
Claim. An explicit structural certificate bundling four facts: the RS PTA stochastic signature $S=\varphi^{-44}$ satisfies $0<S$; $S$ differs from the zero inflation-baseline proxy; the algebraic discriminator proposition holds; and the master-theorem hypothesis that the RS PTA stochastic GW background is distinct from inflation is inhabited.
background
Gravity Track 6.B isolates the theorem-grade algebraic half of a PTA stochastic-background discriminator. The RS structural signature is the same rung-44 positive scale $\varphi^{-44}$ used elsewhere in the gravity/cosmology bridge; the inflation proxy is the zero baseline. Because a positive scale cannot equal zero, the two are algebraically distinct.
The certificate structure records four obligations: positivity of the RS signature, inequality with the zero baseline, the bundled discriminator proposition, and an inhabitant of the master-theorem input asserting RS PTA stochastic GW distinctness from inflation. Upstream lemmas already prove positivity via zpow_pos on $\varphi>0$, and the inequality by rewriting any equality into a contradiction with positivity.
The module explicitly does not attach a PTA dataset or claim current observational separation; dataset sensitivity and spectral fitting remain empirical work outside Lean.
proof idea
Four-field structure assembly, not a tactic proof. Each field is filled by a named prior result: positivity of the rung-44 signature; the inequality against the zero inflation baseline; the discriminator proposition (itself the pair of those two facts); and the master-theorem witness def, which packages that same proposition with its proof. No new algebra is performed here.
why it matters
Gives Track 6.B a single named inhabitant of the structural certificate, so downstream code can treat the PTA discriminator as a concrete object rather than four loose lemmas. The immediate parent is the nonemptiness theorem that wraps this def. That certificate is the algebraic input expected by the gravity master theorem's PTA-stochastic-GW-distinct-from-inflation hypothesis.
In the broader RS chain the signature sits on the $\varphi$-ladder (rung 44), the same self-similar scale forced at T6. The module's role is structural separation only: positive RS scale versus zero inflation proxy. Empirical PTA band claims and channel fitting are left open as falsifier work, not discharged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.