module module moderate

`IndisputableMonolith.Cosmology.PrimordialSpectrum`

This module collects the observed parameters of the primordial scalar power spectrum in Recognition Science cosmology, anchoring the framework to Planck 2018 data with n_s ≈ 0.9649. Cosmologists comparing RS-derived fluctuations to CMB spectra would cite these constants. The module is a collection of definitions and numerical anchors with no internal proofs.

claimThe scalar spectral index satisfies $n_s ≈ 0.9649$, the power spectrum takes the form $P(k) = A_s (k/k_0)^{n_s-1}$, and the tensor-to-scalar ratio is bounded above by the supplied observational limit.

background

Recognition Science derives cosmology from the J-cost functional and the phi-ladder of mass scales. The imported Constants module fixes the RS time quantum at τ₀ = 1 tick. The Cost module supplies the J-cost definition used to generate fluctuations. This module translates those structures into the standard cosmological observables for the primordial spectrum.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the observational targets that downstream results such as fluctuations_from_jcost and amplitude_derivation must reproduce. It closes the link between the RS forcing chain (T5–T8) and CMB data by fixing the spectral index near 0.965.

scope and limits

Does not derive n_s from the J-cost equation.
Does not compute the full k-dependence of the power spectrum.
Does not address reheating or post-inflationary evolution.
Does not provide error bars or likelihood functions.

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