module module

`IndisputableMonolith.Cosmology.PrimordialSpectrum`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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