Encyclopedia Cosmology Cosmology Grand Potential Dilution From Potential

ARTICLE 5 claims 5 theorems

Cosmology Grand Potential Dilution From Potential

A theorem in the Recognition Science library shows how the cosmic neutrino temperature ratio 4/11 follows from a single thermodynamic assumption.

Verify this page

The dilution result

In standard cosmology, the ratio of neutrino to photon temperatures after electron-positron annihilation is a famous number: (Tν/Tγ)3 = 4/11. The Recognition Science framework's theorem dilution_from_potential derives this ratio from a single structural assumption about the hot plasma: that its pressure is a differentiable potential with entropy density s = dP/dT. This is the definition of local equilibrium, not an extra dynamical postulate. The theorem shows that the Euler relation T·s = ρ + P and the Gibbs–Duhem relation p′ = s·T′ are algebraic consequences of this potential structure, not independent inputs.

The derivation proceeds in the grand-canonical ensemble at zero chemical potential, where a fluid is characterized by its pressure P(T) as a function of temperature. Entropy density is defined as s = dP/dT, and energy density as the Legendre transform ρ = T·s − P. From these definitions, the Euler relation is an identity, Gibbs–Duhem is the chain rule, and the fundamental relation dρ = T·ds follows by differentiation. The framework's library, a machine-checked collection of formal theorems, proves all three statements (potential_euler, potential_gibbs_duhem, energy_deriv).

The concrete plasma realizes this structure. For a massless Bose/Fermi gas, the pressure from the grand partition function is P = (π²/90)·(g_B + (7/8)·g_F)·T⁴, with the fermionic weight 7/8 emerging from Mellin-transform integrals. The temperature derivative of this pressure exactly matches the independently derived entropy density, and the Legendre transform reproduces the energy integrals, forcing the radiation equation of state p = ρ/3. These are theorems of the ensemble, not inputs.

With this structure in place, the capstone theorem dilution_from_potential states: given FRW continuity equations for both the coupled sector and the neutrino sector, plus boundary data (plasma degrees of freedom 2+4 → 2 across e± annihilation, shared temperature at decoupling), the ratio (Tν/Tγ)3 = 4/11 follows. The theorem also propagates to the effective entropy degrees of freedom g*s = 43/11. What remains model upstream is the grand-canonical form of the plasma pressure at the boundaries, the Friedmann equations behind continuity, sector decoupling, and the boundary identifications.

THEOREM dilution_from_potential · IndisputableMonolith/Cosmology/GrandPotential.lean
dilution_from_potential · IndisputableMonolith/Cosmology/GrandPotential.lean:272 
/-- **CAPSTONE (dilution from the potential).** `(T_ν/T_γ)³ = 4/11` from:
the coupled sector has a pressure potential with `s = dP/dT` (local
equilibrium, the *only* thermodynamic input), both sectors satisfy their FRW
continuity equations, and the boundary data (plasma dof `2+4 → 2` across e±
annihilation, shared temperature at decoupling).  Compared with
`EntropyConservationFRW.dilution_from_frw`, the Euler and Gibbs–Duhem
hypotheses are gone — they are theorems of the potential structure. -/
theorem dilution_from_potential
    {P s : ℝ → ℝ} {T a Tν : ℝ → ℝ} {sT T' a' 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)
    (hP : ∀ t, HasDerivAt P (s (T t)) (T t))
    (hs : ∀ t, HasDerivAt s (sT t) (T t))
    (hT : ∀ t, HasDerivAt T (T' t) t) (ha : ∀ t, HasDerivAt a (a' t) t)
    (hTν : ∀ t, HasDerivAt Tν (Tν' t) t)
    (hρν : ∀ t, HasDerivAt (fun u => αν * Tν u ^ 4) (ρν' t) t)
    (hcont : ∀ t, a t * (T t * sT t * T' t)
        = -3 * a' t * (energyOf P s (T t) + P (T t)))
    (hcontν : ∀ t, a t * ρν' t
        = -3 * a' t * (αν * Tν t ^ 4 + αν * Tν t ^ 4 / 3))
    (hbefore : s (T t₁) = NeutrinoDilution.radiationEntropy 2 4 T₁)
    (hafter : s (T t₂) = NeutrinoDilution.radiationEntropy 2 0 Tγ)
    (hshare : Tν t₁ = T₁) :
    (Tν t₂ / Tγ) ^ 3 = 4 / 11 := by
  -- Adiabaticity of the coupled sector: derived from the potential structure.
  have hcons : NeutrinoDilution.radiationEntropy 2 4 T₁ * a t₁ ^ 3
      = NeutrinoDilution.radiationEntropy 2 0 Tγ * a t₂ ^ 3 := by
    have h := potential_entropy_constant hTt hP hs hT ha hcont t₁ t₂
    rw [hbefore, hafter] at h
    exact h
  -- Free streaming of the neutrino sector (derived in EntropyConservationFRW).
  have hfree : a t₂ * Tν t₂ = a t₁ * T₁ := by
    have h := EntropyConservationFRW.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 potential_euler · IndisputableMonolith/Cosmology/GrandPotential.lean
potential_euler · IndisputableMonolith/Cosmology/GrandPotential.lean:90 
/-- **Euler relation (derived).** `T·s = ρ + P` is an algebraic identity of
the Legendre-transform structure — not an independent equilibrium postulate. -/
theorem potential_euler (P s : ℝ → ℝ) (x : ℝ) :
    x * s x = energyOf P s x + P x := by
  simp only [energyOf]
  ring
THEOREM potential_gibbs_duhem · IndisputableMonolith/Cosmology/GrandPotential.lean
potential_gibbs_duhem · IndisputableMonolith/Cosmology/GrandPotential.lean:97 
/-- **Gibbs–Duhem relation (derived).** Along any temperature trajectory
`T(t)`, the pressure obeys `p′ = s(T)·T′`: this is the chain rule applied to
`s = dP/dT`, not an independent postulate. -/
theorem potential_gibbs_duhem
    {P s T : ℝ → ℝ} {T' t : ℝ}
    (hP : HasDerivAt P (s (T t)) (T t))
    (hT : HasDerivAt T T' t) :
    HasDerivAt (fun u => P (T u)) (s (T t) * T') t := by
  simpa [Function.comp] using hP.comp t hT
THEOREM plasmaPressure_eq · IndisputableMonolith/Cosmology/GrandPotential.lean
plasmaPressure_eq · IndisputableMonolith/Cosmology/GrandPotential.lean:203 
/-- **THEOREM (plasma pressure closed form).** The log-kernel integrals
(`π⁴/45`, `7π⁴/360`, both derived via Mellin transforms) collapse the
pressure to `P = (π²/90)·(g_B + (7/8)·g_F)·T⁴`.  The `7/8` is the same
fermionic weight that appears in entropy and energy — here it comes out of
the pressure channel independently. -/
theorem plasmaPressure_eq (gB gF T : ℝ) :
    plasmaPressure gB gF T = π ^ 2 / 90 * (gB + 7 / 8 * gF) * T ^ 4 := by
  unfold plasmaPressure
  rw [RadiationEntropyRelation.boseLog_integral_value,
    RadiationEntropyRelation.fermiLog_integral_value]
  have hπ : (π : ℝ) ≠ 0 := Real.pi_ne_zero
  field_simp
  ring
THEOREM plasma_eos · IndisputableMonolith/Cosmology/GrandPotential.lean
plasma_eos · IndisputableMonolith/Cosmology/GrandPotential.lean:263 
/-- **THEOREM (radiation equation of state derived).** `p = ρ/3` is forced by
the grand-canonical integrals — it is not an input anywhere in the chain. -/
theorem plasma_eos (gB gF T : ℝ) :
    plasmaPressure gB gF T = plasmaEnergy gB gF T / 3 := by
  rw [plasmaEnergy_eq, plasmaPressure_eq]
  ring

What this page does not claim

The theorem does not derive the grand-canonical form of the plasma pressure at the boundaries; that remains a statistical mechanics input. The theorem does not prove the Friedmann equations or the continuity equation; those are discharged separately. The theorem does not establish sector decoupling or the shared temperature at decoupling; those are boundary identifications, not derived results.

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/GrandPotential.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