spectralIndexCert
plain-language theorem explainer
This definition assembles a certificate structure that bundles the interval membership and Planck proximity bounds for the Recognition Science spectral index. Cosmologists comparing RS inflation models to CMB data would cite the resulting record when documenting numerical agreement with observations. The construction is a direct record instantiation that invokes the upstream band and proximity theorems.
Claim. Define the spectral index certificate as the structure asserting that the Recognition Science spectral index satisfies $0.955 < n_s < 0.957$ and $|n_s - n_{s,Planck}| < 0.015$.
background
In the Recognition Science treatment of inflation the spectral index follows from the J-cost via the gap parameter at rung 45, yielding the explicit form $n_s = 1 - 2/45$. The module documentation records that this value lies in the narrow interval (0.955, 0.957) and remains within 0.015 of the Planck 2018 central value 0.965. The upstream band theorem establishes the interval by substitution into the closed-form expression followed by numerical normalization; the proximity theorem establishes the absolute-difference bound by the same substitution together with the triangle inequality.
proof idea
The definition is a one-line record constructor that populates the first field of SpectralIndexCert with the band theorem and the second field with the proximity theorem.
why it matters
The certificate consolidates the principal numerical prediction of the RS inflation module, confirming that the gap-45 formula produces a spectral index compatible with CMB observations inside the stated tolerances. It directly implements the Lean formalization goal stated in the module documentation. No downstream theorems yet reference the certificate, leaving open its use in larger structure-formation or multi-parameter cosmology statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.