nsRS_gt_zero
plain-language theorem explainer
The theorem establishes that the Recognition Science spectral index exceeds zero. Cosmologists comparing phi-ladder predictions to CMB spectra would cite it to confirm the sign of n_s_RS before interval checks. The proof is a term-mode one-liner that unfolds the definition and applies norm_num to reduce the inequality to a numerical fact.
Claim. $1 - 2/45 > 0$, where the gap parameter at rung 45 is the Recognition Science quantity appearing in the slow-roll formula.
background
The module derives the RS spectral index from the J-cost framework for inflation. The upstream definition states: 'RS spectral index: n_s = 1 - 2/gap45.' Here gap45 evaluates to 45, producing n_s_RS = 1 - 2/45. The local setting quotes Planck 2018 data n_s = 0.965 ± 0.004 and positions the RS value near 0.956 via the gap-45 formula.
proof idea
The proof unfolds nsRS and gap45, then invokes norm_num to confirm the resulting arithmetic inequality holds.
why it matters
The result secures positivity of n_s_RS, a prerequisite for the interval (0.955, 0.957) that the module compares to Planck observations. It supports sibling certificates such as nsRS_band and SpectralIndexCert. In the Recognition framework it anchors the gap-45 step of the eight-tick octave before further use in the phi-ladder or alpha-band constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.