inflation_zero_stochastic_baseline
plain-language theorem explainer
The pure-inflation stochastic baseline is the real constant zero, the structural proxy against which the RS PTA signature is compared. Gravity-track and PTA auditors cite it when stating that the rung-44 RS band is algebraically distinct from a vanishing inflationary background. The body is the literal constant assignment 0.
Claim. The pure-inflation zero-baseline proxy for the PTA structural discriminator is the real number $0$.
background
Track 6.B of the gravity layer isolates the algebraic core of a PTA stochastic-background discriminator. Recognition Science predicts a positive stochastic scale at the same rung-44 height used elsewhere in the gravity/cosmology bridge, namely $\varphi^{-44}$. Pure inflation is represented, for structural comparison only, by a vanishing stochastic amplitude.
Naming that amplitude as an explicit real constant keeps every later inequality and certificate free of bare numeric literals. The module does not load PTA datasets or fit spectra; it only supplies the theorem-grade inhabitant for the master-theorem input that RS stochastic GW is distinct from inflation.
proof idea
One-line definition: the name is bound to the real constant $0$. No lemmas, tactics, or proof obligations.
why it matters
This constant is the comparison point for the whole PTA structural stack. It appears in the inflationary family predicate (values equal to the zero baseline), in the inequality that the RS $\varphi$-rung signature is not that baseline, and in the structural discriminator proposition (positive RS scale and unequal to zero). Those facts assemble into PTAStructuralCert and the one-statement theorem that also inhabits the master-theorem hypothesis PTAStochasticGWDistinctFromInflation.
Within the broader RS forcing picture the rung-44 scale sits on the same $\varphi$-ladder used for masses and other gravity bridges; the zero baseline is the simplest algebraic foil that makes the positivity claim a genuine discriminator rather than a tautology. Empirical PTA separation remains outside Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.