matter_exceeds_baryons
plain-language theorem explainer
RS cosmology sets baryon density Ω_b h² = 0.022 from its baryogenesis process while total matter density reaches Ω_m h² = 0.143. This strict inequality establishes the required non-baryonic dark matter component for structure formation. BAO analysts cite it when matching the predicted sound horizon scale to observations. The proof reduces to a direct numerical comparison of the two constant definitions.
Claim. In the Recognition Science framework the baryon density parameter satisfies $Ω_b h^2 < Ω_m h^2$, where $Ω_b h^2 = 0.022$ from RS baryogenesis and $Ω_m h^2 = 0.143$ from RS dark matter plus baryons.
background
The BAO module derives the sound horizon r_s ≈ 147 Mpc from RS-predicted cosmological parameters. The definition rs_omega_b_h2 fixes the baryon density parameter at 0.022, while rs_omega_m_h2 fixes the total matter density at 0.143 to include both baryons and dark matter. These constants appear in the baryon loading ratio R(z) = 3ρ_b/(4ρ_γ) and the sound speed formula c_s = c/√(3(1+R)).
proof idea
The proof is a one-line wrapper that applies the norm_num tactic to the definitions of rs_omega_b_h2 and rs_omega_m_h2. This evaluates the numerical constants 0.022 and 0.143 and confirms the inequality.
why it matters
The result confirms a dark matter component inside the RS BAO calculation and supports the module's derivation of the sound horizon integral. It is consistent with the framework's eight-tick octave and phi-ladder mass scales that generate the required matter excess. No downstream uses are recorded in the supplied graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.