def
definition
fNL_observed
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.PrimordialSpectrum on GitHub at line 212.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
233 2. r contradicts (φ-1)⁴ prediction
234 3. Large non-Gaussianity found -/
235structure SpectrumFalsifier where
236 ns_no_phi : Prop
237 r_contradicts : Prop
238 large_nongaussianity : Prop
239 falsified : ns_no_phi ∧ r_contradicts → False
240
241end PrimordialSpectrum
242end Cosmology