module module high

`IndisputableMonolith.Cosmology.PrimordialSpectrum`

The Cosmology.PrimordialSpectrum module supplies definitions for the primordial power spectrum and its observables in Recognition Science cosmology. It encodes the scalar spectral index n_s ≈ 0.9649 matching Planck 2018. Cosmologists comparing RS-derived inflation to CMB data cite these values. The module consists of definitions and constants built on the constants and cost modules.

claimThe scalar spectral index satisfies $n_s \≈ 0.9649$ (Planck 2018). The module introduces the power spectrum $P(k)$ together with the observed spectrum, tilt predictions from the phi-ladder, and the tensor-to-scalar ratio upper bound.

background

The module operates in the cosmology domain and imports the fundamental RS time quantum $\tau_0 = 1$ tick from Constants, described as the fundamental RS time quantum (RS-native). It also imports the Cost module for the J-cost function. The setting uses RS-native units with $c=1$, $\hbar=\phi^{-5}$, and derives fluctuations from the recognition composition law and the phi fixed point. The doc comment identifies $n_s \approx 0.9649$ (Planck 2018) as the central observed value.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the observed spectral index and related quantities that connect the forcing chain (T5 J-uniqueness through T8 D=3) to cosmological data. It supports amplitude_derivation and fluctuations_from_jcost inside the module. No external used_by theorems are recorded, positioning it as the interface between RS fundamentals and observational cosmology.

scope and limits

Does not derive n_s from the J-uniqueness theorem.
Does not include the full inflationary potential or dynamics.
Does not specify the efold number from first principles.
Does not compute the complete CMB angular power spectrum.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (20)

def spectral_index_observed L43
def spectral_tilt_observed L46
def scalar_amplitude_observed L49
def tensor_to_scalar_upper_bound L52
structure PowerSpectrum L62
def power L70
def observedSpectrum L74
def phi_prediction_tilt L94
theorem spectral_tilt_phi_connection L96
def efolds_typical L110
theorem fluctuations_from_jcost L120
theorem amplitude_derivation L133
structure TensorSpectrum L147
def tensor_to_scalar L152
def rs_prediction_r L163
theorem r_prediction L165
def running_observed L202
def fNL_observed L212
def predictions L222
structure SpectrumFalsifier L235