ptaStructuralCert_inhabited
plain-language theorem explainer
The PTA structural certificate type is inhabited: the RS stochastic GW signature is positive, algebraically distinct from the zero inflation baseline, and supplies the master-theorem PTA hypothesis. Gravity/cosmology auditors cite it as the theorem-grade package for Track 6.B. The proof is a one-line term inhabitation by the already-built certificate value.
Claim. There exists a PTA structural certificate: a record asserting that the RS PTA stochastic signature $s = \varphi^{-44}$ satisfies $s > 0$, $s \neq 0$ (the inflation-baseline proxy), that the RS-vs-inflation discriminator proposition holds, and that the master-theorem hypothesis ``PTA stochastic GW is distinct from inflation'' is witnessed.
background
Track 6.B isolates the algebraic half of the PTA stochastic-background discriminator. The RS structural signature is the same rung-44 positive scale $\varphi^{-44}$ used across the gravity/cosmology bridge; the inflation baseline is the zero proxy. Module text states explicitly that this is not a dataset attachment and does not claim current observational separation.
The certificate structure bundles four facts: positivity of the RS signature, inequality with the zero inflation baseline, the discriminator proposition, and the master-theorem input PTAStochasticGWDistinctFromInflation. The $\varphi$-ladder and the master gravity theorem supply the ambient scale and the hypothesis slot this inhabitant fills.
Upstream scaffolding (polarized interface counts, Clifford/8-tick bridges, PRC positivity) is ambient Recognition infrastructure; the local content is the PTA-scale comparison only.
proof idea
One-line term proof: inhabit Nonempty PTAStructuralCert by the already-constructed value ptaStructuralCert. No new algebra is performed here; the certificate fields were discharged by sibling lemmas (positivity of $\varphi^{-44}$, inequality with the zero baseline, the discriminator proposition, and the master-theorem witness).
why it matters
Closes the structural one-statement for Track 6.B: the PTA stochastic signature is positive and therefore distinct from the zero inflation-baseline proxy, and the master-theorem PTA input is inhabited. Downstream consumers of MasterTheorem.PTAStochasticGWDistinctFromInflation can treat the hypothesis as theorem-grade rather than open.
In the Recognition framework this is the algebraic discriminator, not an observational claim. Dataset sensitivity and channel-specific spectral fitting remain empirical falsifier work outside Lean. The rung-44 $\varphi$-ladder scale ties the PTA channel to the same self-similar fixed point ($\varphi$) forced at T6 and used throughout the mass and gravity ladders. No used_by edges are recorded yet; the declaration is the package point for the master theorem input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.