pith. sign in
module module high

IndisputableMonolith.Cosmology.InflationSpectralIndexFromJCost

show as:
view Lean formalization →

The module derives the inflationary spectral index from the J-cost function in Recognition Science cosmology. It defines gap45 as the body-plan ceiling of 45 and builds nsRS with value, bounds, and a certification near the Planck measurement. Cosmologists working on RS-derived inflation models would cite these results to connect J-uniqueness to observable n_s. The module proceeds via a chain of definitions and elementary inequalities.

claim$gap_{45}=45$, $n_s^{RS}$ with $0<n_s^{RS}<1$ and $n_s^{RS}$ in the band near the Planck value, together with the certificate $SpectralIndexCert$ that $n_s^{RS}$ matches the observed spectral index.

background

The module sits in the Cosmology domain and imports the base constants module whose fundamental time quantum is given by τ₀ = 1 tick. It introduces gap45 as the body-plan ceiling equal to 45, a parameter that enters the phi-ladder mass formula. From this it constructs nsRS as the RS-native spectral index obtained from the J-cost, together with its numerical value, strict inequalities, and proximity to the Planck result.

proof idea

This is a definition module, no proofs. It consists of a linear sequence of definitions (gap45, nsRS, nsRS_val) followed by elementary lemmas establishing the bounds nsRS_lt_one, nsRS_gt_zero, nsRS_band and the final certification SpectralIndexCert.

why it matters in Recognition Science

The module supplies the J-cost derivation of the inflationary spectral index to the Recognition Science cosmology framework. It grounds the observable n_s in the forcing chain landmarks T5 (J-uniqueness) and T6 (phi fixed point) and provides the concrete certification that feeds into later cosmological matching arguments.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)