Prove2Me

Electron fraction of a fully ionized IGM: fe=7/8f_e = 7/8

Proved
HuWang2023.electronFraction_fully_ionized

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

cosmologyfast-radio-bursts

With hydrogen fraction YH=0.75Y_H = 0.75, helium fraction YHe=0.25Y_{He} = 0.25 and complete ionization Xe,H=Xe,He=1X_{e,H} = X_{e,He} = 1 (valid at z<3z<3), the electron fraction fe=YHXe,H+12YHeXe,Hef_e = Y_HX_{e,H} + \tfrac12 Y_{He}X_{e,He} appearing in Eq. (5) equals

fe=78.f_e = \frac78.

This is the value of fef_e that enters the FRB dispersion measure in the redshift range used in Section 3.4.

Preamble
import Mathlib
import Definitions.Def_HuWang2023_HubbleTension_Defs
Formal statement
namespace HuWang2023

theorem electronFraction_fully_ionized :
    electronFraction 0.75 1 0.25 1 = 7 / 8 := by sorry

end HuWang2023
Source
Jian-Ping Hu and Fa-Yin Wang, *Hubble Tension: The Evidence of New Physics*, Universe 2023, 9(2), 94, https://doi.org/10.3390/universe9020094, Section 3.4, p. 6, text following Eq. (5)
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

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

View graph