Physics Bao Baryon Loading Decreasing

The declining baryon load

In the hot early universe, ordinary matter and light were mixed into a single fluid. The proportion of matter in that fluid is called the baryon loading, written R. At early times, when the universe was dense and hot, R was large. As the universe expanded, the matter thinned out more slowly than the radiation, so the ratio R decreased. The theorem baryon_loading_decreasing states this precisely: for any positive starting value R₀ and any two redshifts z₁ and z₂ with z₁ < z₂, the loading at z₂ is less than the loading at z₁. Redshift here is a measure of cosmic time, larger meaning earlier; the theorem says the loading falls monotonically as time moves forward.

The definition behind the theorem is simple: baryon_loading (R₀ z) = R₀ / (1 + z). The denominator grows with time, so the quotient shrinks. The proof is a direct application of the fact that dividing a positive number by a larger positive number gives a smaller result. The machine-checked library of formal theorems verifies that this holds for all positive R₀ and all redshifts greater than minus one, which is the physically meaningful range where the formula is defined.

This monotonic decrease is not an isolated curiosity. It feeds directly into the speed of sound in the baryon-photon fluid, c_s = 1 / √(3(1+R)). As R falls, the sound speed rises toward its radiation-only limit of 1/√3. That changing speed, integrated over cosmic history, sets the distance sound waves could travel before decoupling, the sound horizon of about 147 Mpc. The horizon, in turn, sets the scale of the acoustic peaks in the cosmic microwave background, the ripples that map the early universe's density structure.

In Recognition Science, the framework models cosmology from its own derived parameters. The baryon density parameter 0.022 and matter density 0.143 are definitional choices in its library, not measured inputs. The spectral index n_s = 1 - 2/N_e with 60 e-folds gives 0.967, a red tilt. These feed the same standard cosmological equations used in conventional physics, producing the sound horizon and the peak spacing. The framework's contribution is the origin of these parameters, not a new equation for the sound speed.

The theorem establishes a monotonic decrease, nothing more. It does not claim that baryon loading reaches zero, that the decrease is linear, or that the specific value R₀ is derived from first principles. It does not prove that the sound horizon is exactly 147 Mpc; that number is an approximation, and the library's consistency theorem only shows it lies within 0.5 Mpc of 147.18. The theorem is a clean statement about a defined function, and its power comes from being placed in the larger chain that produces observable cosmological scales.

/-- Baryon loading decreases with redshift (photons more dominant at high z). -/
theorem baryon_loading_decreasing (R₀ : ℝ) (hR : 0 < R₀) (z₁ z₂ : ℝ)
    (hz₁ : -1 < z₁) (hz₂ : -1 < z₂) (h : z₁ < z₂) :
    baryon_loading R₀ z₂ < baryon_loading R₀ z₁ := by
  unfold baryon_loading
  apply div_lt_div_of_pos_left (by linarith) (by linarith) (by linarith)

/-- **SOUND SPEED**: c_s = c/√(3(1+R))
    In units c=1: c_s = 1/√(3(1+R)). -/
noncomputable def sound_speed (R : ℝ) : ℝ := 1 / Real.sqrt (3 * (1 + R))

/-- **RS PREDICTION**: Sound horizon agrees with BOSS measurement.
    BOSS: r_s = 147.18 ± 0.29 Mpc.
    Agreement: |r_s^RS - r_s^BOSS| < 0.5 Mpc. -/
theorem rs_sound_horizon_consistent :
    |sound_horizon_approx - 147.18| < 0.5 := by
  norm_num [sound_horizon_approx]

What this page does not claim

The theorem does not claim that baryon loading reaches zero at any finite redshift. The theorem does not claim that the decrease is linear in time or redshift. The theorem does not derive the specific value of R₀ from first principles.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/BAO.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: