ptaStochasticGWStructuralCert
plain-language theorem explainer
Bundles the structural PTA stochastic-GW certificate: positivity of the φ-signature log φ, the algebraic discriminator against inflation, and the master-theorem hypothesis witness. Cosmologists and QG auditors cite it to retire the PTA distinct-from-inflation slot from the conditional quantum-gravity master theorem. The construction is a three-field record filled by already-proved positivity and the existing witness def.
Claim. There is a structural certificate packing three facts: (i) $0 < \log\varphi$ for the RS PTA spectral signature; (ii) the discriminator proposition that this signature is strictly positive while the inflationary tensor tilt is approximately zero; (iii) an inhabitant of the master-theorem hypothesis that the RS PTA stochastic GW background is distinct from inflation.
background
Track 6.B of the quantum-gravity master plan asks for a structural discriminator of the pulsar-timing-array stochastic GW background. RS predicts a spectral imprint from the φ-rung primordial structure; inflationary slow-roll instead gives $n_t \approx 0$ via the tensor consistency relation $r = -8 n_t$. This module ships only the algebraic half of that discriminator.
The RS PTA signature is the per-rung phase delay $\log\varphi \approx 0.481$, the same φ-rational invariant used for black-hole echoes from bounce. The discriminator proposition asserts that this signature is strictly positive, hence distinct from inflation's near-zero baseline. Positivity is the theorem $0 < \log\varphi$, proved from $1 < \varphi$.
The certificate structure packages that positivity, the discriminator proposition, and an inhabitant of the master-theorem input PTAStochasticGWDistinctFromInflation, so the conditional master theorem can drop the PTA hypothesis.
proof idea
One-line record construction, not a tactic proof. The three structure fields are filled by name:
- signature positivity is the existing theorem $0 < \log\varphi$ (unfold the signature def, apply
Real.log_posto $1 < \varphi$); - discriminator_holds is the one-line theorem that reduces the discriminator proposition to that same positivity fact;
- master_hypothesis_witness is the already-built inhabitant that pairs the discriminator proposition with its proof for the Gravity.MasterTheorem hypothesis type.
No new algebra is performed at this site.
why it matters
Closes the structural form of Track 6.B (stochastic GW background) in the quantum-gravity master plan: the algebraic φ-signature discriminator is now a concrete certificate, not an open hypothesis. Downstream, ptaStochasticGWStructuralCert_inhabited is the one-line Nonempty proof that cites this def, and the Track 6.B one-statement theorem rests on that inhabitedness.
The packaged witness retires PTAStochasticGWDistinctFromInflation from the hypothesis list of the conditional master theorem rs_quantum_gravity_master_conditional (Session 97). Framework landmarks in play are the golden ratio φ (T6 fixed point) and the shared φ-rational phase delay already used in black-hole echo structure.
Open remainder: the exact RS spectral tilt from the φ-rung primordial ladder is still future physics work; only the structural positivity-vs-zero split is certified here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.