canonicalPTADistinctWitness
plain-language theorem explainer
Canonical zero-argument witness that the RS pulsar-timing-array stochastic gravitational-wave background is formula-level distinct from the inflationary null baseline. Gravity auditors cite it as the D5 PTA input to the unconditional quantum-gravity master assembly. The definition is a one-line alias of the typed observation-channel signal-model witness.
Claim. A canonical inhabitant of the PTA-distinct-from-inflation structure: the RS PTA channel prediction differs from the inflationary null baseline, and the absolute separation is strictly positive. The structure packages that proposition together with a proof that it holds.
background
The unconditional master-theorem module supplies theorem-built witnesses for the five inputs that the older conditional RS quantum-gravity master accepted as free arguments. One of those inputs is Track 6.B: the claim that the RS stochastic GW background seen in pulsar timing arrays is distinct from standard inflationary $n_t$ predictions.
Upstream, that claim is packaged as a structure with a single proposition field (RS PTA spectrum distinct from inflation) and a proof field that the proposition holds. The signal-model layer strengthens the older band witness by attaching a named observation channel: the RS prediction is unequal to the null baseline and the absolute gap is positive.
Locally this definition simply names that signal-model witness as the canonical PTA input on the zero-argument route through the master theorem.
proof idea
One-line definitional wrapper. The body is exactly the upstream signal-model PTA witness, which already inhabits the PTA-distinct-from-inflation structure by setting the proposition to (RS channel prediction $\neq$ null baseline) and (absolute separation $> 0$), and discharging both conjuncts from the channel lemmas.
why it matters
This is the D5 PTA witness consumed by the scoped unconditional master assembly and by the parallel endpoint-route validity theorem. The non-circularity audit lists its proposition field among the five witness inputs that hold unconditionally, none of which assumes any master clause; the same field appears in the one-statement non-circularity certificate.
In the Recognition gravity program it closes the PTA observable-band slot on the theorem-built route: formula-level separation of the RS stochastic GW background from the inflationary baseline, packaged so the master theorem no longer takes that hypothesis as an external argument. It does not by itself finish the full physical QG framework; it only supplies one audited input among the five.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.