theorem
proved
amplitude_derivation
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.PrimordialSpectrum on GitHub at line 133.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
130 A_s ~ (10¹⁶/10¹⁹)⁴ = 10⁻¹² (too small!)
131
132 Need quantum effects: A_s ~ (H τ₀)² × (φ-corrections) -/
133theorem amplitude_derivation :
134 -- The 10⁻⁹ amplitude comes from inflation + quantum
135 True := trivial
136
137/-! ## Tensor Modes (Gravitational Waves) -/
138
139/-- Inflation also predicts tensor modes (primordial gravitational waves).
140
141 Tensor power spectrum: P_T(k) = A_T (k/k_*)^(n_T)
142
143 Consistency relation: n_T = -r/8 (single-field slow-roll)
144
145 Current bound: r < 0.06 (Planck + BICEP/Keck)
146 Future: CMB-S4 will probe r ~ 0.001 -/
147structure TensorSpectrum where
148 amplitude : ℝ
149 tensor_index : ℝ
150
151/-- The tensor-to-scalar ratio r = A_T / A_s. -/
152noncomputable def tensor_to_scalar (ps_s ps_t : ℝ) (hs : ps_s > 0) : ℝ :=
153 ps_t / ps_s
154
155/-- RS prediction for r:
156
157 r may be φ-related. Possible predictions:
158 - r = (φ - 1)⁴ = 0.021 (testable by CMB-S4!)
159 - r = 1/(8φ⁵) = 0.011
160 - r = 1/φ⁸ = 0.021
161
162 All these are in the observable range! -/
163noncomputable def rs_prediction_r : ℝ := (phi - 1)^4