SpectralIndexCert
SpectralIndexCert packages two numerical bounds on the RS spectral index: membership in (0.955, 0.957) and absolute deviation from the Planck value 0.965 below 0.015. Cosmologists formalizing Recognition Science predictions would cite the structure to certify agreement between the J-cost gap-45 formula and CMB data. The definition is a direct record bundling the upstream theorems nsRS_band and nsRS_near_planck.
claimA structure asserting that the Recognition Science spectral index satisfies $0.955 < n_s < 0.957$ and $|n_s - 0.965| < 0.015$, where $n_s = 1 - 2 / g_{45}$ and $g_{45}$ denotes the 45-rung gap parameter.
background
The module derives the inflationary spectral index from the J-cost in Recognition Science cosmology. The RS spectral index is defined noncomputably as $n_s = 1 - 2 / g_{45}$, with $g_{45}$ the gap parameter at rung 45. The Planck reference value is fixed at 0.965. Two upstream theorems establish the open interval (0.955, 0.957) for $n_s$ and its distance to 0.965 being less than 0.015.
proof idea
The structure is populated by direct reference to the two theorems nsRS_band and nsRS_near_planck in its fields. No tactics or reductions occur; the definition simply aggregates the already-proved bounds.
why it matters in Recognition Science
The structure supplies a compact certificate that the gap-45 prediction $n_s = 1 - 2/45$ lies inside the Planck band, feeding directly into the downstream definition spectralIndexCert. It formalizes the module claim that Recognition Science reproduces the observed CMB index $n_s = 0.965$ within 0.015 without extra parameters, closing one step in the A2 cosmology depth.
scope and limits
- Does not derive the gap parameter from the forcing chain T0-T8.
- Does not obtain the spectral index from the Recognition Composition Law.
- Does not include slow-roll corrections beyond the leading 1/gap term.
- Does not compare the prediction to non-Starobinsky inflation models.
formal statement (Lean)
58structure SpectralIndexCert where
59 nsRS_band : (0.955 : ℝ) < nsRS ∧ nsRS < 0.957
60 nsRS_near_planck : |nsRS - nsPlanck| < 0.015
61