Physics Bao Sound Speed Radiation Limit

The radiation limit

Sound needs a medium. In the first few hundred thousand years after the Big Bang, the universe was filled with a hot, dense plasma of protons, electrons, and photons. A pressure wave moving through that mixture is called a baryon acoustic oscillation. Its speed is not set by the plasma's material properties alone. It depends on how the plasma is loaded with matter compared to radiation.

The standard formula for this speed is c_s = c / √(3(1+R)), where c is the speed of light and R is the baryon-to-photon ratio. When matter and radiation are balanced, R is large and the sound slows down. When radiation dominates completely, R approaches zero. The formula then simplifies to c_s = c / √3, which is about 0.577 times the speed of light. This is the radiation limit: the fastest sound can move in a plasma whose pressure comes entirely from radiation, with no matter to weigh it down.

In Recognition Science, a machine-checked library of formal theorems records this result as sound_speed_radiation_limit. The theorem proves that the general formula, with R set to zero, reduces exactly to 1/√3 in units where the speed of light is 1. It is a pure algebraic identity, derived from the definition of the sound speed. The theorem does not introduce new physics. It states a mathematical fact about the standard formula.

The same library also proves that the sound speed is positive for any physically allowed loading, and that it decreases as the matter loading grows. These facts together describe how the early universe's sound waves behaved as the plasma cooled and matter came to dominate. The radiation limit is the upper bound of that behavior, the speed at the very beginning of the story.

What the declaration does not do is connect this speed to any measured cosmological quantity. It says nothing about the actual value of R at any real time, nor about the size of the sound horizon, which is the distance sound could travel before the plasma cooled. Those are separate claims in the library, each with its own definitions and checks. The radiation limit is a clean, self-contained piece of the larger framework, a fact about a formula rather than a statement about the universe.

/-- In the limit R → 0 (radiation dominated): c_s → c/√3. -/
theorem sound_speed_radiation_limit :
    sound_speed 0 = 1 / Real.sqrt 3 := by
  unfold sound_speed
  norm_num

/-- Sound speed is positive for R ≥ 0. -/
theorem sound_speed_positive (R : ℝ) (hR : -1 < R) :
    0 < sound_speed R := by
  unfold sound_speed
  apply div_pos one_pos
  apply Real.sqrt_pos_of_pos
  linarith

/-- Sound speed decreases with R (more baryons → slower sound). -/
theorem sound_speed_decreasing (R₁ R₂ : ℝ) (hR₁ : -1 < R₁) (hR₂ : -1 < R₂) (h : R₁ < R₂) :
    sound_speed R₂ < sound_speed R₁ := by
  unfold sound_speed
  apply div_lt_div_of_pos_left one_pos
  · apply Real.sqrt_pos_of_pos; linarith
  · apply Real.sqrt_lt_sqrt
    · linarith
    · linarith

What this page does not claim

The declaration does not state any measured value for the sound speed in the early universe. The declaration does not derive the baryon-to-photon ratio from first principles. The declaration does not connect the radiation limit to the observed cosmic microwave background anisotropies.

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: