`matter_exceeds_baryons`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.BAO
domain: Physics
line: 76 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.BAO on GitHub at line 76.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  73def rs_omega_m_h2 : ℝ := 0.143
  74
  75/-- Matter density exceeds baryon density (dark matter component). -/
  76theorem matter_exceeds_baryons : rs_omega_b_h2 < rs_omega_m_h2 := by
  77  norm_num [rs_omega_b_h2, rs_omega_m_h2]
  78
  79/-- **RS SPECTRAL INDEX**: n_s ≈ 0.967 from slow-roll inflation.
  80    n_s = 1 - 2/N_e where N_e ≈ 60 e-foldings. -/
  81noncomputable def rs_spectral_index (N_e : ℝ) : ℝ := 1 - 2 / N_e
  82
  83/-- For N_e = 60 e-foldings: n_s ≈ 0.967. -/
  84theorem spectral_index_60efolds :
  85    rs_spectral_index 60 = 1 - 1/30 := by
  86  unfold rs_spectral_index
  87  norm_num
  88
  89/-- Spectral index is less than 1 (red-tilted spectrum). -/
  90theorem spectral_index_red_tilt (N_e : ℝ) (hN : 0 < N_e) :
  91    rs_spectral_index N_e < 1 := by
  92  unfold rs_spectral_index
  93  linarith [div_pos two_pos hN]
  94
  95/-! ## Sound Horizon -/
  96
  97/-- **RS DRAG EPOCH REDSHIFT**: z_drag ≈ 1060.
  98    This is where baryons decouple from photons (Saha equation). -/
  99def rs_drag_redshift : ℝ := 1060
 100
 101/-- **SOUND HORIZON** (simplified formula valid for matter+radiation):
 102    r_s ≈ (2/3) × (c / k_eq) × √(6/R_eq) × ln[...]
 103    where k_eq is the wavenumber at matter-radiation equality.
 104
 105    Numerically: r_s ≈ 147 Mpc. -/
 106abbrev sound_horizon_approx : ℝ := 147  -- in Mpc

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.