SpectralIndexCert
plain-language theorem explainer
The SpectralIndexCert structure bundles two certified numerical bounds on the RS spectral index derived from the gap-45 formula. Researchers comparing Recognition Science inflation models to CMB data cite it to record that the prediction sits inside (0.955, 0.957) and within 0.015 of the Planck central value. The declaration is a plain structure definition whose fields directly reference the already-proved upstream interval and proximity statements.
Claim. Let $n_{s,RS} := 1 - 2/45$ and let $n_{s,Planck} := 0.965$. The structure asserts $0.955 < n_{s,RS} < 0.957$ together with $|n_{s,RS} - n_{s,Planck}| < 0.015$.
background
The module defines the RS spectral index via nsRS := 1 - 2/gap45, where gap45 supplies the effective e-fold count in the slow-roll regime. The reference Planck value is introduced as the constant 0.965. Upstream nsRS_band states that n_s_RS lies in (0.955, 0.957) and nsRS_near_planck states that the absolute deviation from the Planck value is less than 0.015; both are obtained by direct substitution and norm_num.
proof idea
The declaration is a structure definition. Its two fields are literally the statements of the upstream theorems nsRS_band and nsRS_near_planck. No tactics or reductions occur inside the structure itself.
why it matters
SpectralIndexCert supplies the type for the downstream construction spectralIndexCert, which packages an explicit witness of the two bounds. It thereby formalizes the module claim that the RS prediction n_s = 1 - 2/gap45 lies inside the Planck-compatible interval, instantiating the gap-based slow-roll formula in the Recognition Science cosmology setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.