tensor_to_scalar_upper_bound

formal source

  49noncomputable def scalar_amplitude_observed : ℝ := 2.1e-9
  50
  51/-- The tensor-to-scalar ratio r < 0.06 (Planck + BICEP/Keck). -/
  52noncomputable def tensor_to_scalar_upper_bound : ℝ := 0.06
  53
  54/-! ## The Power Spectrum -/
  55
  56/-- The primordial power spectrum P(k) = A_s (k/k_*)^(n_s - 1).
  57
  58    - k: wavenumber (inverse length scale)
  59    - k_*: pivot scale (0.05 Mpc⁻¹)
  60    - A_s: amplitude at pivot
  61    - n_s: spectral index -/
  62structure PowerSpectrum where
  63  amplitude : ℝ
  64  spectral_index : ℝ
  65  pivot_scale : ℝ
  66  amplitude_pos : amplitude > 0
  67  pivot_pos : pivot_scale > 0
  68
  69/-- Power at wavenumber k. -/
  70noncomputable def power (ps : PowerSpectrum) (k : ℝ) (hk : k > 0) : ℝ :=
  71  ps.amplitude * (k / ps.pivot_scale)^(ps.spectral_index - 1)
  72
  73/-- The observed best-fit spectrum. -/
  74noncomputable def observedSpectrum : PowerSpectrum := {
  75  amplitude := scalar_amplitude_observed,
  76  spectral_index := spectral_index_observed,
  77  pivot_scale := 0.05,  -- Mpc⁻¹
  78  amplitude_pos := by unfold scalar_amplitude_observed; norm_num,
  79  pivot_pos := by norm_num
  80}
  81
  82/-! ## φ-Connection Analysis -/