theorem
proved
term proof
matter_exceeds_baryons
show as:
view Lean formalization →
formal statement (Lean)
76theorem matter_exceeds_baryons : rs_omega_b_h2 < rs_omega_m_h2 := by
proof body
Term-mode proof.
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. -/