canonicalPTADistinctWitness_bandRoute
plain-language theorem explainer
Canonical zero-argument witness that the Recognition Science PTA stochastic gravitational-wave signal is observationally distinct from a standard inflationary background. Gravity auditors cite it when closing the unconditional master theorem’s PTA input. The body is a one-line alias of the older PTAStructural observable-band witness, retained for audit continuity.
Claim. There is a canonical, theorem-built witness establishing that the Recognition Science stochastic gravitational-wave background relevant to pulsar timing arrays lies in an observable band and is distinct from a standard inflationary GW spectrum.
background
The module Gravity.MasterTheoremUnconditional supplies theorem-built, zero-argument witnesses for the five inputs that the older conditional quantum-gravity master theorem took as hypotheses. The conditional statement remains the audit surface; this file is the canonical route through it.
One of those inputs is the PTA clause: the RS stochastic GW background must be shown distinct from inflation in a form usable by the master theorem. Upstream, PTAStructural already builds an observable-band witness for that distinction. The present declaration is the named canonical handoff of that witness into the unconditional closure surface.
Related scaffolding in the same module covers Regge/EH continuum convergence, discrete Bianchi identities, amplitude linearity, and page-curve witnesses. Ringdown-echo algebra is deliberately quarantined elsewhere and is not consumed here as a closed strong-field witness.
proof idea
One-line definitional wrapper. The term is exactly the upstream structural witness ptaStochasticGWObservableBandWitness from PTAStructural, re-exported at the type PTAStochasticGWDistinctFromInflation expected by the master theorem. No new tactics or lemmas are applied; the audit note records that the older band route remains valid.
why it matters
Closes the PTA leg of the unconditional master-theorem surface: without a named zero-argument witness that RS stochastic GW is band-distinct from inflation, the conditional master theorem cannot be instantiated as a closed gravity claim. The module’s purpose is precisely to install such witnesses for all five former arguments.
Downstream use is currently empty in the graph, so this is a terminal handoff object rather than an intermediate lemma. It sits in the gravity domain alongside page-curve, strong-field, and Regge/EH continuum routes. Framework-wise it supports the RS gravity program’s claim that PTA-scale stochastic backgrounds are not inflationary leftovers but recognition-structured signals, complementary to the continuum and Bianchi D2 witnesses in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.