photon
plain-language theorem explainer
Registers the photon as a thermal species: massless, two polarization states, bosonic. Cosmology and g_*(T) bookkeeping cite it as the baseline massless gauge boson that never drops out of the relativistic count. The body is a four-field structure literal on the Species record.
Claim. The photon is the thermal species with name $\mathrm{photon}$, mass threshold $m=0\,\mathrm{GeV}$, internal degrees of freedom $g=2$, and bosonic statistics ($\mathrm{fermion}=\mathrm{false}$).
background
The module builds the standard instantaneous-threshold step function $g_*(T)$ over adopted SM content. Each species contributes its full relativistic degree count while $T$ exceeds its mass threshold and drops out below it; the QCD crossover switches the strong sector from QGP to pions. Arithmetic is exact over $\mathbb{Q}$.
A Species record packages four fields: a display name, a rational mass threshold in GeV (only order relative to $T$ matters), an internal degree-of-freedom count, and a fermion/boson flag. Particle content and the $7/8$ fermionic integral follow the same SM bookkeeping as StandardModel.RelativisticDOF; gauge group and generation count are RS-derived elsewhere, while matter representations and the neutrino convention are imported.
The photon is the massless end-member of that table: it remains relativistic at every temperature in the module's stated domain $T\gtrsim 1,\mathrm{MeV}$.
proof idea
Pure definition: the four-tuple constructor of Species is applied to the string "photon", mass $0$, dof $2$, and fermion := false. No lemmas, no tactics.
why it matters
Supplies the never-decoupling bosonic baseline for every $g_*(T)$ evaluation in this module and for the high-$T$ bridge that matches RelativisticDOF.g_star_derived (symmetric and broken electroweak phases both total 28 bosonic DOF). Downstream consumers include stellar mass-to-light and assembly structures (J_bit, StellarConfig, ml_is_phi_power), nucleosynthesis tier bookkeeping, and $\alpha$-genesis normalizations that count the gauge-invariant photon channel (alphaInvK_pos, gauge_redundancy_eq_7, seed_channel_count). In the RS forcing chain the photon is the massless $U(1)$ carrier whose two helicities enter the eight-tick and $\alpha$ closures; this entry does not re-derive that physics, it only freezes the SM dof count used by the threshold model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.