Cosmology Neutrino Dilution Plasma Before Eq G Before

The pre-annihilation plasma

In the early universe, the plasma of photons, electrons, and positrons had a specific entropy content. The declaration plasma_before_eq_gBefore is a theorem in the framework's machine-checked library of formal theorems. It proves that the entropy density of this photon-electron-positron plasma equals a simple closed form: (2π²/45) times the effective degrees of freedom, gBefore, times the temperature cubed. The value of gBefore is 11/2, a number that emerges from the calculation, not one that is put in by hand.

The theorem is a precise statement about the framework's definition of plasma entropy. It shows that the entropy density of a relativistic plasma with 2 bosonic and 4 fermionic degrees of freedom is exactly (2π²/45) * (gB + (7/8) * gF) * T³. Here, gB and gF are the counts of bosonic and fermionic internal degrees of freedom. The 7/8 factor is the standard entropy weight for fermions, and the 2π²/45 coefficient comes from the derived integrals of the entropy functional. The theorem then identifies this expression with the pre-annihilation effective degrees of freedom, gBefore = 11/2, which is the sum of 2 bosonic and 4 fermionic degrees of freedom weighted by the 7/8 factor.

The proof is a formal derivation, verified by the Lean kernel. It relies on the structural theorem radiationEntropy_eq, which collapses the definition of plasma entropy into a compact form. The theorem does not assume the value of gBefore; it derives it from the underlying entropy functional. This is a key step in the larger framework, as it provides the starting point for the subsequent derivation of the neutrino dilution factor and the effective entropy degrees of freedom after electron-positron annihilation.

The declaration does not claim that the physical universe actually had this exact plasma composition. The particle content (2 photon polarizations, 4 electron-positron degrees of freedom) is a model hypothesis, not a derived result. The theorem also does not claim that the plasma was in thermal equilibrium or that it expanded adiabatically. These are separate physical assumptions. The theorem only establishes a mathematical identity within the framework's definitions, given the specified particle content. It is a clean, formal statement about the entropy of a well-defined plasma model.

/-- The photon–electron plasma before e± annihilation (2 bosonic + 4
fermionic dof) carries exactly `gBefore = 11/2` effective entropy dof: the
`11/2` of `EntropyPerPhoton.gBefore` is the functional-layer value. -/
theorem plasma_before_eq_gBefore (T : ℝ) :
    radiationEntropy ((EntropyPerPhoton.gPhoton : ℚ) : ℝ)
        ((EntropyPerPhoton.gElectron : ℚ) : ℝ) T
      = 2 * π ^ 2 / 45 * ((EntropyPerPhoton.gBefore : ℚ) : ℝ) * T ^ 3 := by
  rw [radiationEntropy_eq]
  unfold EntropyPerPhoton.gBefore EntropyPerPhoton.gPhoton
    EntropyPerPhoton.gElectron EntropyPerPhoton.fermionWeight
  push_cast
  ring

/-- The photon–electron plasma before e± annihilation (2 bosonic + 4
fermionic dof) carries exactly `gBefore = 11/2` effective entropy dof: the
`11/2` of `EntropyPerPhoton.gBefore` is the functional-layer value. -/
theorem plasma_before_eq_gBefore (T : ℝ) :
    radiationEntropy ((EntropyPerPhoton.gPhoton : ℚ) : ℝ)
        ((EntropyPerPhoton.gElectron : ℚ) : ℝ) T
      = 2 * π ^ 2 / 45 * ((EntropyPerPhoton.gBefore : ℚ) : ℝ) * T ^ 3 := by
  rw [radiationEntropy_eq]
  unfold EntropyPerPhoton.gBefore EntropyPerPhoton.gPhoton
    EntropyPerPhoton.gElectron EntropyPerPhoton.fermionWeight
  push_cast
  ring

/-- **THEOREM (structural form).** The plasma entropy density collapses to
`(2π²/45)·(gB + (7/8)·gF)·T³`, with the `2π²/45` coefficient and the `7/8`
entropy weight both coming from the derived integrals `∫σ_B = 4π⁴/45`,
`∫σ_F = 7π⁴/90` — neither is assumed. -/
theorem radiationEntropy_eq (gB gF T : ℝ) :
    radiationEntropy gB gF T = 2 * π ^ 2 / 45 * (gB + 7 / 8 * gF) * T ^ 3 := by
  unfold radiationEntropy
  rw [RadiationEntropyRelation.bose_entropy_integral_value,
    RadiationEntropyRelation.fermi_entropy_integral_value]
  have hpi : (π : ℝ) ≠ 0 := Real.pi_ne_zero
  field_simp
  ring

What this page does not claim

This theorem does not claim the physical universe had exactly this plasma composition. It does not claim the plasma was in thermal equilibrium or expanded adiabatically. It does not derive the particle content of the early universe.

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/NeutrinoDilution.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: