gAfter
plain-language theorem explainer
After electron–positron annihilation, the coupled plasma’s entropy degrees of freedom reduce to photons alone, fixed at the rational value 2. Cosmologists cite this as the post-annihilation g-factor entering the neutrino temperature ratio. It is a one-line alias of the photon polarization count.
Claim. Define the post-$e^{\pm}$ annihilation entropy degrees of freedom of the photon sector by $g_{\mathrm{after}} := 2$, equal to the two photon polarization states (electrons and positrons having dropped out of equilibrium).
background
The module derives the present-day entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ in a narrow window around 7.04, for use in the baryogenesis dynamical prefactor. One arithmetic ingredient is the effective entropy dof $g_{*s}$ after $e^{\pm}$ annihilation, built from photon and diluted-neutrino contributions.
Standard Model particle content supplies the bare counts: photons carry 2 polarizations; $e^{\pm}$ carry 4 fermionic dof; three neutrino generations carry 6. The fermion weight $7/8$ is proved elsewhere from Fermi–Dirac integrals, not assumed. Before annihilation the coupled photon–electron plasma has $g_{\mathrm{before}} = 2 + (7/8)\cdot 4 = 11/2$; afterward only photons remain thermalized with the plasma.
Upstream, gPhoton is the MODEL constant 2. The physical dilution theorem in NeutrinoDilution states that entropy conservation in the photon–$e^{\pm}$ sector plus free-streaming neutrinos force $(T_\nu/T_\gamma)^3 = 4/11$.
proof idea
Pure definitional abbreviation: gAfter is set equal to gPhoton, itself the rational constant 2. No tactics or lemmas are invoked; the body is a single assignment.
why it matters
This constant is the numerator of the dilution ratio dilutionCubed := gAfter / gBefore. The companion theorem dilutionCubed_eq then evaluates that ratio by unfolding to $2 / (11/2) = 4/11$ via norm_num.
That $4/11$ is exactly the classical neutrino-to-photon temperature cube used in $g_{*s} = 2 + (7/8)\cdot 6 \cdot (4/11) = 43/11$, which closes the third ingredient of the entropy-per-photon derivation. Downstream, NeutrinoDilution’s entropy-conservation theorem recovers the same $4/11$ from radiation-entropy integrals rather than from these rationals alone, so the definition here stays a plain bookkeeping marker while the physics is proved elsewhere.
In the broader RS cosmology lane this feeds the replacement of the bare constant 7.04 by a derived interval, tightening the baryogenesis dynamical prefactor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.