ptaStochasticGWObservableBandWitness
plain-language theorem explainer
Master-theorem witness packing the claim that the RS PTA stochastic GW signature sits in a positive observable band while every inflationary zero-baseline value lies outside it. Gravity auditors cite it when discharging Track 6.B. The body is a one-line structure inhabitant that plugs in the already-proved observable-band separation proposition and its proof.
Claim. An inhabitant of the master-theorem structure for PTA stochastic-GW distinctness from inflation: the proposition that the RS rung-44 signature $\varphi^{-44}$ lies in a positive observable band and every member of the explicit inflationary zero-signature family lies outside that band, together with a proof that this proposition holds.
background
Track 6.B of the gravity master theorem asks for a structural discriminator between the RS PTA stochastic gravitational-wave background and inflationary $n_t$ predictions. The module supplies only the algebraic, theorem-grade half of that discriminator: the RS signature is the same rung-44 positive scale $\varphi^{-44}$ used elsewhere in the gravity/cosmology bridge, while the inflationary baseline class is the explicit zero-signature family.
The master-theorem input is a structure with a proposition field and a proof that the proposition holds. Upstream, the observable-band proposition asserts that the RS signature lies inside a positive band and that every inflationary baseline lies outside it. That proposition is already proved by pairing the RS-in-band lemma with the inflationary-family-out-of-band lemma.
The present declaration strengthens an earlier nonzero structural separation to this explicit positive observable band. It does not attach a PTA dataset.
proof idea
One-line structure constructor. The proposition field is set to the observable-band discriminator (RS signature in the positive band, and every inflationary zero-baseline outside that band). The holds field is the already-proved theorem establishing that discriminator, which is itself the pair of the RS-in-band lemma and the inflationary-family-not-in-band lemma. No new algebra is performed here.
why it matters
Supplies the algebraic inhabitant for Track 6.B of the gravity master theorem (RS PTA stochastic-GW background distinct from inflationary $n_t$ predictions). Downstream, the unconditional master-theorem audit re-exports this witness as the canonical band-route PTA distinctness witness, confirming the older observable-band packing remains valid.
The scale is the phi-ladder rung-44 value $\varphi^{-44}$ shared with the cosmology bridge. The declaration closes only the theorem-grade structural side; dataset sensitivity and channel-specific spectral fitting remain empirical falsifier work, as the module doc states. It does not touch strong-field Track 6.C or other master-theorem legs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.