gPhoton
plain-language theorem explainer
The photon contributes two internal degrees of freedom (two polarization states). Cosmology proofs that build present-day entropy degrees of freedom g*s and the neutrino dilution factor 4/11 cite this as the bosonic MODEL input. It is a one-line rational constant, not a derived theorem.
Claim. The photon internal degree-of-freedom count is the rational number $g_\gamma = 2$, corresponding to two polarization states (a Standard Model particle-content input).
background
The module derives the entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ in the narrow window $(7.0393, 7.0396)$, replacing a bare $7.04$ constant in the baryogenesis lane. Three ingredients enter: a $\zeta(3)$ window, a $\pi^4$ window, and the arithmetic identity $g_{*s} = 43/11$ from Standard Model particle content.
Effective entropy degrees of freedom count bosonic and fermionic species with a fermion weight $7/8$. Photons are the pure bosonic baseline: two helicity (polarization) states. Electrons and positrons add four fermionic dof; three neutrino generations add six. Before $e^\pm$ annihilation the photon–electron plasma has $g_\mathrm{before} = 2 + (7/8)\cdot 4 = 11/2$; after annihilation only photons remain, so $g_\mathrm{after} = 2$.
Entropy conservation across annihilation then forces the neutrino temperature dilution $(T_\nu/T_\gamma)^3 = g_\mathrm{after}/g_\mathrm{before} = 4/11$, which feeds the present-day $g_{*s}$.
proof idea
No proof. The declaration is a definitional assignment of the rational constant $2$, documented as a MODEL input (two photon polarizations). Downstream lemmas unfold this name and discharge the arithmetic with norm_num.
why it matters
Every entropy-dof assembly in the module starts from this constant. It is the bosonic term in $g_\mathrm{before} = g_\gamma + (7/8)g_e$ and the entire content of $g_\mathrm{after} = g_\gamma$. The dilution identity dilutionCubed_eq unfolds it to obtain $4/11$; gStarS_eq then obtains $g_{*s} = 43/11$. NeutrinoDilution equates the functional radiation-entropy of the pre-annihilation plasma to $g_\mathrm{before}$, casting this $2$ into the thermodynamic layer. NumberDensityIntegral uses it when reconstructing entropy per photon from integrals. Within Recognition Science this is the SM particle-content seed for the entropy-per-photon factor that replaces the bare $7.04$ in the baryogenesis dynamical prefactor; it is not itself a forcing-chain (T0–T8) result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.