ptaStochasticGWDistinctFromInflationWitness
plain-language theorem explainer
Packages the structural claim that the RS PTA stochastic GW signature (the positive rung-44 scale φ^{-44}) differs from the inflationary near-zero baseline into the master-theorem hypothesis type. Gravity-track and cosmology bridge authors cite it when discharging PTAStochasticGWDistinctFromInflation. Construction is a two-field structure inhabitant: the Prop and its positivity proof.
Claim. There is an inhabitant of the master-theorem PTA hypothesis asserting that the Recognition Science PTA stochastic gravitational-wave signature is strictly positive, and therefore structurally distinct from the inflationary slow-roll baseline of approximately zero.
background
Gravity Track 6.B isolates the algebraic half of a PTA stochastic-background discriminator. The RS structural signature is the same rung-44 positive scale $\varphi^{-44}$ used across the gravity/cosmology bridge; the inflationary slow-roll proxy is taken as the zero baseline. The module deliberately does not attach PTA datasets or claim observational separation.
The upstream proposition rs_pta_distinct_inflation_prop is simply $0 < \mathrm{rs_pta_phi_signature}$, and the companion theorem proves it by positivity of that signature. The master theorem exposes a structure PTAStochasticGWDistinctFromInflation whose fields are exactly that proposition and a proof it holds. This declaration is the theorem-grade inhabitant of that structure.
proof idea
Two-field structure construction, not a tactic proof. The proposition field is filled by the local (or cosmology-module) discriminator Prop $0 < \mathrm{rs_pta_phi_signature}$. The holds field is filled by the already-proved positivity theorem, which itself is a one-line appeal to positivity of the rung-44 $\varphi$-signature. No further algebraic work occurs here.
why it matters
Closes the master-theorem input slot PTAStochasticGWDistinctFromInflation for Track 6.B. Downstream, ptaStructuralCert records it as master_hypothesis_witness, and pta_structural_one_statement packages positivity, inequality with the zero baseline, the discriminator Prop, and Nonempty of the master-theorem type into a single conjunction.
In the broader RS picture this is pure structural discrimination on the $\varphi$-ladder (rung 44), not a spectral fit. Dataset sensitivity and channel-specific PTA fitting remain empirical falsifier work outside Lean. It does not invoke T5–T8 forcing directly; it sits on the gravity/cosmology bridge that already uses the forced $\varphi$ and the ladder mass/scale formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.