Encyclopedia Cosmology Cosmology Entropy Conservation Frw Dilution From Frw

ARTICLE 4 claims 4 theorems

Cosmology Entropy Conservation Frw Dilution From Frw

In the early universe, the ratio of neutrino to photon temperature is not an assumption: the expansion equations themselves force it to a fixed value.

Verify this page

How the neutrino temperature is forced

In the standard hot Big Bang model, the universe cools as it expands, and the temperature of any gas of particles drops in a predictable way. For radiation, the temperature T falls inversely with the scale factor a, the number that measures how distances grow with time. The relation is a·T = constant. This is the free-streaming redshift law, and in most textbooks it is simply asserted as a property of how photons and neutrinos behave.

What the Recognition Science framework's machine-checked library of formal theorems shows is that this law, and the conservation of entropy that accompanies it, are not separate assumptions. They follow from the Friedmann equations, the two differential equations that govern the expansion of a homogeneous, isotropic universe. The first Friedmann equation relates the expansion rate to the energy density, the second relates the acceleration to the density plus pressure. Differentiating the first and substituting the second yields the continuity equation, which states that the energy density changes in a way dictated by the pressure. This is not a new physical input; it is the Bianchi identity, the automatic consistency condition of Einstein's equations.

From that continuity equation, the library derives two results. For any fluid in local equilibrium, meaning one where the Euler relation T·s = ρ + p and the Gibbs–Duhem relation hold, the comoving entropy, the entropy per unit volume multiplied by the cube of the scale factor, s·a³, is constant in time. For a decoupled radiation gas, the same continuity equation forces a·T to be constant. Both statements are theorems in the library, not postulates. The derivation handles the derivatives cleanly and requires no division by potentially zero quantities.

The capstone theorem, dilution_from_frw, applies these results to the early universe around the time of electron-positron annihilation. Before annihilation, the plasma contains photons, electrons, and positrons; after, only photons remain. The neutrinos have already decoupled and stream freely. The theorem takes as input the Friedmann equations, the equilibrium identities for the coupled sector, the free-radiation equation of state for the neutrinos, and the boundary data: the plasma degrees of freedom before and after annihilation, and the shared temperature at decoupling. It outputs the famous ratio (T_ν/T_γ)³ = 4/11, the standard value that enters cosmological calculations of the present-day neutrino background. A companion theorem derives the effective number of entropy degrees of freedom, g*s = 43/11, which appears in the formula for the total entropy density of the universe today.

The achievement is that the dynamics, the adiabatic expansion and the 1/a redshift law, are now derived rather than assumed. What remains as modeling choices are the Friedmann equations themselves as the input from general relativity, the local equilibrium of the coupled sector, the decoupling of the neutrinos, and the boundary identifications. The framework proves the consequences of those choices, not the choices themselves.

THEOREM comoving_entropy_conserved · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean
comoving_entropy_conserved · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean:120 
/-- **THEOREM (adiabatic expansion derived).** For a fluid in local
equilibrium — Euler relation `T·s = ρ + p` along the evolution and
Gibbs–Duhem `p′ = s·T′` at the given time — the FRW continuity equation
`a·ρ′ = −3a′(ρ+p)` forces `d/dt (s·a³) = 0`.

Differentiating the Euler relation gives `T′s + Ts′ = ρ′ + p′`; Gibbs–Duhem
removes the `T′` terms, leaving `T·s′ = ρ′`; continuity plus Euler then give
`T·(a·s′ + 3a′·s) = 0`, and `T ≠ 0` cancels. -/
theorem comoving_entropy_conserved
    {ρ p s T a : ℝ → ℝ} {ρ' p' s' a' T' t : ℝ}
    (hTt : T t ≠ 0)
    (hρ : HasDerivAt ρ ρ' t) (hp : HasDerivAt p p' t)
    (hs : HasDerivAt s s' t) (ha : HasDerivAt a a' t)
    (hT : HasDerivAt T T' t)
    (hEuler : ∀ u, T u * s u = ρ u + p u)
    (hGD : p' = s t * T')
    (hcont : a t * ρ' = -3 * a' * (ρ t + p t)) :
    HasDerivAt (fun u => s u * a u ^ 3) 0 t := by
  -- Differentiate the Euler relation.
  have hTs : HasDerivAt (fun u => T u * s u) (T' * s t + T t * s') t :=
    hT.mul hs
  have hρp : HasDerivAt (fun u => ρ u + p u) (ρ' + p') t := hρ.add hp
  have hfun : (fun u => T u * s u) = fun u => ρ u + p u := funext hEuler
  rw [hfun] at hTs
  have hdiff : T' * s t + T t * s' = ρ' + p' := hTs.unique hρp
  -- Gibbs–Duhem kills the T′ terms: T·s′ = ρ′.
  have hTs' : T t * s' = ρ' := by linear_combination hdiff + hGD
  -- Continuity + Euler force a·s′ + 3a′·s = 0.
  have hkey : a t * s' + 3 * a' * s t = 0 := by
    have h1 : T t * (a t * s' + 3 * a' * s t) = 0 := by
      linear_combination a t * hTs' + 3 * a' * hEuler t + hcont
    exact (mul_eq_zero.mp h1).resolve_left hTt
  -- Assemble the product derivative of s·a³.
  have hpow : HasDerivAt (fun u => a u ^ 3) (3 * a t ^ 2 * a') t := by
    simpa using ha.fun_pow 3
  have hprod : HasDerivAt (fun u => s u * a u ^ 3)
      (s' * a t ^ 3 + s t * (3 * a t ^ 2 * a')) t := hs.mul hpow
  have hzero : s' * a t ^ 3 + s t * (3 * a t ^ 2 * a') = 0 := by
    linear_combination a t ^ 2 * hkey
  rw [hzero] at hprod
  exact hprod
THEOREM radiation_aT_conserved · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean
radiation_aT_conserved · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean:164 
/-- **THEOREM (free streaming derived).** For a decoupled radiation gas with
`ρ = αT⁴` and `p = ρ/3`, the FRW continuity equation alone forces
`d/dt (a·T) = 0`: the redshift law `T ∝ 1/a` is not an assumption.
Continuity reads `4αT³·(a·T′ + a′·T) = 0` and `α ≠ 0`, `T ≠ 0` cancel. -/
theorem radiation_aT_conserved
    {T a : ℝ → ℝ} {T' a' ρ' t α : ℝ}
    (hα : α ≠ 0) (hTt : T t ≠ 0)
    (hT : HasDerivAt T T' t) (ha : HasDerivAt a a' t)
    (hρ : HasDerivAt (fun u => α * T u ^ 4) ρ' t)
    (hcont : a t * ρ' = -3 * a' * (α * T t ^ 4 + α * T t ^ 4 / 3)) :
    HasDerivAt (fun u => a u * T u) 0 t := by
  -- The density derivative is 4αT³T′ by uniqueness.
  have hpow : HasDerivAt (fun u => T u ^ 4) (4 * T t ^ 3 * T') t := by
    simpa using hT.fun_pow 4
  have h4 : HasDerivAt (fun u => α * T u ^ 4) (α * (4 * T t ^ 3 * T')) t :=
    hpow.const_mul α
  have hρval : ρ' = α * (4 * T t ^ 3 * T') := hρ.unique h4
  -- Continuity collapses to 4αT³·(a′T + aT′) = 0.
  have hkey : a' * T t + a t * T' = 0 := by
    have h1 : 4 * α * T t ^ 3 * (a' * T t + a t * T') = 0 := by
      rw [hρval] at hcont
      linear_combination hcont
    have hne : (4 * α * T t ^ 3 : ℝ) ≠ 0 :=
      mul_ne_zero (mul_ne_zero (by norm_num) hα) (pow_ne_zero 3 hTt)
    exact (mul_eq_zero.mp h1).resolve_left hne
  have hprod : HasDerivAt (fun u => a u * T u) (a' * T t + a t * T') t :=
    ha.mul hT
  rw [hkey] at hprod
  exact hprod
THEOREM dilution_from_frw · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean
dilution_from_frw · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean:269 
/-- **CAPSTONE (dilution from FRW dynamics).** Replace the two MODEL
hypotheses of `NeutrinoDilution.dilution_from_entropy_conservation` by
physics: the coupled sector is an equilibrium fluid (Euler + Gibbs–Duhem)
satisfying the FRW continuity equation, and the decoupled neutrino gas is
free radiation (`ρ_ν = α_ν T_ν⁴`) satisfying its own continuity equation.
Then comoving entropy conservation and the `1/a` redshift law are *derived*
(§§1–3), and with the boundary data (plasma dof `2+4 → 2` across e±
annihilation, shared temperature at decoupling) they force

  `(T_ν/T_γ)³ = 4/11`. -/
theorem dilution_from_frw
    {ρ p s T a Tν : ℝ → ℝ} {ρ' p' s' a' T' Tν' ρν' : ℝ → ℝ}
    {t₁ t₂ : ℝ} {T₁ Tγ αν : ℝ}
    (hTt : ∀ t, T t ≠ 0) (hαν : αν ≠ 0) (hTνt : ∀ t, Tν t ≠ 0)
    (ha₂ : a t₂ ≠ 0) (hTγ : Tγ ≠ 0)
    (hρ : ∀ t, HasDerivAt ρ (ρ' t) t) (hp : ∀ t, HasDerivAt p (p' t) t)
    (hs : ∀ t, HasDerivAt s (s' t) t) (ha : ∀ t, HasDerivAt a (a' t) t)
    (hT : ∀ t, HasDerivAt T (T' t) t)
    (hTν : ∀ t, HasDerivAt Tν (Tν' t) t)
    (hρν : ∀ t, HasDerivAt (fun u => αν * Tν u ^ 4) (ρν' t) t)
    (hEuler : ∀ u, T u * s u = ρ u + p u)
    (hGD : ∀ t, p' t = s t * T' t)
    (hcont : ∀ t, a t * ρ' t = -3 * a' t * (ρ t + p t))
    (hcontν : ∀ t, a t * ρν' t
        = -3 * a' t * (αν * Tν t ^ 4 + αν * Tν t ^ 4 / 3))
    (hbefore : s t₁ = NeutrinoDilution.radiationEntropy 2 4 T₁)
    (hafter : s t₂ = NeutrinoDilution.radiationEntropy 2 0 Tγ)
    (hshare : Tν t₁ = T₁) :
    (Tν t₂ / Tγ) ^ 3 = 4 / 11 := by
  -- Adiabaticity of the coupled sector (derived, §§1, 3).
  have hcons : NeutrinoDilution.radiationEntropy 2 4 T₁ * a t₁ ^ 3
      = NeutrinoDilution.radiationEntropy 2 0 Tγ * a t₂ ^ 3 := by
    have h := comoving_entropy_constant hTt hρ hp hs ha hT hEuler hGD hcont t₁ t₂
    rw [hbefore, hafter] at h
    exact h
  -- Free streaming of the neutrino sector (derived, §§2, 3).
  have hfree : a t₂ * Tν t₂ = a t₁ * T₁ := by
    have h := radiation_aT_constant hαν hTνt hTν ha hρν hcontν t₂ t₁
    rw [hshare] at h
    exact h
  exact NeutrinoDilution.dilution_from_entropy_conservation ha₂ hTγ hcons hfree
THEOREM gStarS_from_frw · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean
gStarS_from_frw · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean:311 
/-- **CAPSTONE (g*s from FRW dynamics).** With the same physics inputs, the
present-day entropy density (photons at `T_γ` + 6 fermionic neutrino dof at
the diluted `T_ν`) equals `(2π²/45)·gStarS·T_γ³` with
`EntropyPerPhoton.gStarS = 43/11`: the effective entropy dof entering the
η_B dynamical prefactor is forced by the continuity equations. -/
theorem gStarS_from_frw
    {ρ p s T a Tν : ℝ → ℝ} {ρ' p' s' a' T' Tν' ρν' : ℝ → ℝ}
    {t₁ t₂ : ℝ} {T₁ Tγ αν : ℝ}
    (hTt : ∀ t, T t ≠ 0) (hαν : αν ≠ 0) (hTνt : ∀ t, Tν t ≠ 0)
    (ha₂ : a t₂ ≠ 0) (hTγ : Tγ ≠ 0)
    (hρ : ∀ t, HasDerivAt ρ (ρ' t) t) (hp : ∀ t, HasDerivAt p (p' t) t)
    (hs : ∀ t, HasDerivAt s (s' t) t) (ha : ∀ t, HasDerivAt a (a' t) t)
    (hT : ∀ t, HasDerivAt T (T' t) t)
    (hTν : ∀ t, HasDerivAt Tν (Tν' t) t)
    (hρν : ∀ t, HasDerivAt (fun u => αν * Tν u ^ 4) (ρν' t) t)
    (hEuler : ∀ u, T u * s u = ρ u + p u)
    (hGD : ∀ t, p' t = s t * T' t)
    (hcont : ∀ t, a t * ρ' t = -3 * a' t * (ρ t + p t))
    (hcontν : ∀ t, a t * ρν' t
        = -3 * a' t * (αν * Tν t ^ 4 + αν * Tν t ^ 4 / 3))
    (hbefore : s t₁ = NeutrinoDilution.radiationEntropy 2 4 T₁)
    (hafter : s t₂ = NeutrinoDilution.radiationEntropy 2 0 Tγ)
    (hshare : Tν t₁ = T₁) :
    NeutrinoDilution.radiationEntropy 2 0 Tγ
        + NeutrinoDilution.radiationEntropy 0 6 (Tν t₂)
      = 2 * π ^ 2 / 45 * ((EntropyPerPhoton.gStarS : ℚ) : ℝ) * Tγ ^ 3 :=
  NeutrinoDilution.total_entropy_eq_gStarS hTγ
    (dilution_from_frw hTt hαν hTνt ha₂ hTγ hρ hp hs ha hT hTν hρν
      hEuler hGD hcont hcontν hbefore hafter hshare)

What this page does not claim

This does not claim that the Friedmann equations themselves are derived within the framework; they are the input from general relativity. This does not claim that the local equilibrium of the coupled sector is derived; it is a modeling assumption. This does not claim that the boundary identifications, such as the plasma degrees of freedom before and after annihilation, are derived.

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/Cosmology/EntropyConservationFRW.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND