module module moderate

`IndisputableMonolith.Cosmology.PrimordialSpectrum`

The Cosmology.PrimordialSpectrum module assembles observed values and phi-based relations for the primordial power spectrum in Recognition Science cosmology. Cosmologists comparing RS predictions to Planck data would cite it. The module organizes declarations around the scalar spectral index without containing proofs.

claim$n_s ≈ 0.9649$ (Planck 2018). The power spectrum $P(k)$ is parameterized via tilt, amplitude, and J-cost fluctuations on the phi-ladder.

background

The module sits in the cosmology domain and imports the RS time quantum τ_{0} = 1 tick from Constants together with the J-cost framework from Cost. It introduces the primordial spectrum through declarations for the observed spectral index, tilt, scalar amplitude, tensor-to-scalar bound, and related phi predictions. The module doc-comment identifies n_s ≈ 0.9649 as the central observational landmark.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the observational anchor for sibling declarations such as phi_prediction_tilt and spectral_tilt_phi_connection. It provides the Planck 2018 scalar index against which Recognition Science phi-ladder predictions are compared. No used_by edges are recorded.

scope and limits

Does not derive n_s from the forcing chain T0-T8.
Does not compute efolds or fluctuation amplitudes from first principles.
Does not address tensor modes beyond the declared upper bound.
Does not include explicit mass-ladder or Berry-threshold calculations.

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