def
definition
running_observed
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.PrimordialSpectrum on GitHub at line 202.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
199 Consistent with zero, but RS may predict specific value.
200
201 If spectral index is φ-quantized, running may show φ-structure. -/
202noncomputable def running_observed : ℝ := -0.006
203
204/-! ## Primordial Non-Gaussianity -/
205
206/-- Deviations from Gaussian statistics (f_NL):
207
208 Local f_NL = -2 ± 5 (Planck 2018)
209
210 RS prediction: f_NL may have φ-structure, but small.
211 Single-field slow-roll gives f_NL ~ slow-roll parameters ~ 0.01. -/
212noncomputable def fNL_observed : ℝ := -2
213
214/-! ## Implications -/
215
216/-- RS predictions for CMB observations:
217
218 1. **n_s - 1 ≈ -1/(8φ³)**: Testable with Planck precision
219 2. **r ≈ (φ-1)⁴ ≈ 0.02**: Testable by CMB-S4
220 3. **Running ≈ 0**: Consistent with observations
221 4. **f_NL ≈ 0**: Small non-Gaussianity -/
222def predictions : List String := [
223 "n_s ≈ 0.970 from φ-structure",
224 "r ≈ 0.02 from (φ-1)⁴",
225 "Running of n_s ~ 0",
226 "Non-Gaussianity f_NL ~ 0"
227]
228
229/-! ## Falsification Criteria -/
230
231/-- The derivation would be falsified if:
232 1. n_s has no φ-connection