pta_structural_one_statement
plain-language theorem explainer
The PTA stochastic background carries a strictly positive Recognition Science φ-ladder signature, algebraically distinct from the pure-inflation zero baseline, and the master-theorem Track 6.B hypothesis is inhabited. Cosmologists comparing RS gravity predictions against inflationary n_t cite this packaging. The proof is a four-component term assembling positivity, inequality, the discriminator proposition, and a witness structure.
Claim. The RS PTA stochastic signature $s=\varphi^{-44}$ satisfies $0<s$, $s\neq 0$ (the inflation zero-baseline proxy), the structural discriminator proposition holds, and the master-theorem input asserting that the RS PTA stochastic-GW spectrum is distinct from inflationary predictions is inhabited.
background
Track 6.B of the gravity bridge isolates the algebraic discriminator between Recognition Science and pure inflation for the pulsar-timing-array stochastic gravitational-wave background. The RS structural signature is the rung-44 positive scale $\varphi^{-44}$ used elsewhere in the gravity/cosmology bridge; the inflation baseline proxy is identically zero.
The structural discriminator proposition asserts that this signature is strictly positive and unequal to the zero baseline. The master theorem packages that claim as a hypothesis structure with a proposition field and a holds proof: "RS PTA stochastic-GW background spectrum distinct from inflationary $n_t$ predictions."
This module supplies only the theorem-grade algebraic inhabitant. Dataset sensitivity and channel-specific spectral fitting remain empirical falsifier work.
proof idea
Term-mode four-tuple, no tactics. Positivity is rs_pta_stochastic_phi_signature_pos; the inequality against the zero baseline is rs_pta_stochastic_phi_signature_ne_inflation_zero; the local discriminator proposition is discharged by rs_pta_distinct_inflation_prop_holds; and Nonempty of the master structure is witnessed by ptaStochasticGWDistinctFromInflationWitness, which fills the structure fields with the local prop and its proof.
why it matters
Closes Track 6.B's structural one-statement: the master-theorem input for PTA stochastic-GW distinctness from inflation is inhabited at the algebraic level. Downstream use sites are currently empty, so this is a leaf packaging for the gravity MasterTheorem chain rather than an intermediate lemma. It does not resolve the observational OPEN status noted on the master hypothesis; it only supplies the Lean inhabitant. The $\varphi^{-44}$ rung ties the PTA channel to the same phi-ladder used for mass and cosmology scales in RS, keeping the gravity bridge on a single discrete scale family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.