ptaDistinctFromInflationWitness
plain-language theorem explainer
Packages the structural PTA discriminator (strict positivity of the RS φ-signature log φ) as an inhabitant of the master-theorem hypothesis that RS stochastic GW spectra differ from inflationary n_t ≈ 0. Cosmologists and quantum-gravity auditors cite it to discharge Track 6.B from the conditional master theorem. Construction is a two-field structure instance wiring the local proposition and its positivity proof.
Claim. There is an inhabitant of the master-theorem structure asserting that the RS PTA stochastic gravitational-wave signature is distinct from inflation: the carried proposition is $0 < \log\varphi$, and that inequality is proved.
background
Track 6.B of the quantum-gravity master plan asks for a structural discriminator between the RS prediction for a pulsar-timing-array stochastic GW background and the inflationary slow-roll baseline. In this module the RS signature is the per-rung phase delay $\log\varphi\approx 0.481$, the same $\varphi$-rational invariant used for black-hole echo timing. Inflation is proxied by $n_t\approx 0$ from the tensor consistency relation $r=-8n_t$.
The local proposition asserts only the algebraic half of that discriminator: $0<\log\varphi$. Its proof is the positivity theorem for the signature. The master theorem in Gravity.MasterTheorem exposes a structure with a proposition field and a holds field; filling both fields retires the PTA hypothesis from the conditional master list.
Upstream, the Gravity.PTAStructural twin uses a slightly stronger conjunction (positivity and inequality to a zero baseline). Here the cosmology track keeps the minimal form $0<\mathrm{signature}$.
proof idea
Pure structure construction, not a tactic proof. The master structure needs two fields: a proposition and a proof that it holds. The first field is set to the local discriminator proposition $0<\log\varphi$. The second field is filled by the already-proved positivity theorem for that signature (itself a one-line appeal to $0<\log\varphi$). No new algebra is done at this site.
why it matters
This witness is the object that actually retires Track 6.B from the conditional quantum-gravity master theorem. Downstream it is plugged into the structural certificate, the Track 6.B one-statement (positivity, discriminator, and Nonempty of the master structure), and the deeper/partial master theorems that take the PTA hypothesis as a concrete argument rather than an open assumption.
In framework terms it is the algebraic half of the φ-rung primordial GW claim: RS forces a strictly positive spectral signature tied to $\varphi$, while inflation sits at a near-zero tensor tilt. The module status is structural closure (0 sorry); the remaining obligation is empirical match to NANOGrav/EPTA and derivation of the exact RS spectral tilt from the φ-ladder, not this inhabitant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.