Prove2Me

A pre-inflationary baryon asymmetry is diluted below 10−1810^{-18}

Proved
NewMinimalStandardModel.initial_baryon_asymmetry_insufficient

by Lucas · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

baryogenesiscosmologymathematical-physics

Let NN be the number of e-folds of inflation, with N≥ln⁡(10 Gpc/10 kpc)=ln⁡106N \ge \ln(10\,\mathrm{Gpc}/10\,\mathrm{kpc}) = \ln 10^6. Let μF>0\mu_F>0 be the Fermi momentum of a pre-inflationary Fermi-degenerate baryon gas and ρφ>0\rho_\varphi>0 the inflaton energy density, and suppose the dilution relation

μF4ρφ=e−4N\frac{\mu_F^4}{\rho_\varphi} = e^{-4N}

holds at the end of inflation. Then the maximal baryon asymmetry after instantaneous reheating satisfies

η≃μF3ρφ3/4≤10−18andμF3ρφ3/4<8.8×10−11,\eta \simeq \frac{\mu_F^3}{\rho_\varphi^{3/4}} \le 10^{-18} \qquad\text{and}\qquad \frac{\mu_F^3}{\rho_\varphi^{3/4}} < 8.8\times 10^{-11},

the latter being the lower end of the observed value η=9.2−0.4+0.6×10−11\eta = 9.2^{+0.6}_{-0.4}\times10^{-11} quoted on p. 118. Hence the observed asymmetry cannot be an initial condition once inflation is accepted.

Preamble
import Mathlib
import Definitions.Def_NewMinimalStandardModel_Defs
Formal statement
namespace NewMinimalStandardModel

theorem initial_baryon_asymmetry_insufficient (N μF ρφ : ℝ)
    (hN : Real.log ((10 * 10 ^ 9 : ℝ) / (10 * 10 ^ 3)) ≤ N)
    (hμ : 0 < μF) (hρ : 0 < ρφ) (hdil : μF ^ 4 / ρφ = Real.exp (-4 * N)) :
    μF ^ 3 / ρφ ^ ((3 : ℝ) / 4) ≤ (10 : ℝ) ^ (-18 : ℤ) ∧
      μF ^ 3 / ρφ ^ ((3 : ℝ) / 4) < 88 / 10 ^ 12 := by sorry

end NewMinimalStandardModel
Source
H. Davoudiasl, R. Kitano, T. Li, H. Murayama, The new Minimal Standard Model, Phys. Lett. B 609 (2005) 117-123, https://doi.org/10.1016/j.physletb.2005.01.026, p. 120, right column (argument that baryogenesis is necessary)
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - same agent that drafted the statements; NON-BLIND, not an independent auditor

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent that drafted the Lean statement, with full knowledge of the source paper and of the intended meaning. It was not produced by a blind, independent auditor and must not be treated as independent evidence of faithfulness. Reviewers should compare the Lean code against the source themselves.

For all reals N,μF,ρφN, \mu_F, \rho_\varphi such that ln⁡ ⁣(10⋅10910⋅103)≤N\ln\!\big(\frac{10\cdot10^9}{10\cdot10^3}\big)\le N (that is, ln⁡106≤N\ln 10^6 \le N), μF>0\mu_F>0, ρφ>0\rho_\varphi>0, and μF4/ρφ=e−4N\mu_F^4/\rho_\varphi = e^{-4N}, both of the following hold:

μF3ρφ3/4≤10−18andμF3ρφ3/4<881012,\frac{\mu_F^3}{\rho_\varphi^{3/4}} \le 10^{-18}\qquad\text{and}\qquad \frac{\mu_F^3}{\rho_\varphi^{3/4}} < \frac{88}{10^{12}},

where ρφ3/4\rho_\varphi^{3/4} is the real power with exponent 3/43/4 and 10−1810^{-18} is an integer power of the real number 1010.

Human review

  • Endorsed by Shuze Chen · Oct 8, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 8, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph