module module moderate

`IndisputableMonolith.Cosmology.EntropyPerPhoton`

Defines the standard-model bookkeeping constants for cosmological entropy density: photon, electron, and neutrino internal degrees of freedom, the 7/8 fermion weight, pre/post e⁺e⁻ annihilation g-factors, the (4/11) neutrino dilution cube, g_*s = 43/11, and ζ(3). Cosmologists deriving η_γ, N_eff, or T_ν/T_γ cite these as the MODEL layer. The module is definitional; identities such as dilutionCubed_eq and gStarS_eq are algebraic equalities, not deep proofs.

claimFix the internal dof $g_\gamma=2$, $g_e=4$, $g_\nu=6$, the fermion entropy weight $7/8$, and the effective counts $g_{\mathrm{before}}=2+\frac78(4+6)$, $g_{\mathrm{after}}=2+\frac78\cdot 6$. Set the dilution cube $(T_\nu/T_\gamma)^3=4/11$ and $g_{*s}=43/11$, and record $\zeta(3)=\sum_{n\ge1}n^{-3}$ as a summable series used in number-density integrals.

background

In early-universe thermodynamics the entropy density of a relativistic species is $s=(2\pi^2/45)g_{*s}T^3$, with $g_{*s}$ an effective count of bosonic and fermionic degrees of freedom. Photons contribute $g_\gamma=2$ (two helicities). Electrons and positrons together contribute $g_e=4$; three neutrino species (left-handed, plus antineutrinos) contribute $g_\nu=6$. Fermions enter with a weight $7/8$ relative to bosons because the Fermi–Dirac energy integral is $7/8$ of the Bose–Einstein one.

Before $e^+e^-$ annihilation the full relativistic content is $g_{\mathrm{before}}=g_\gamma+(7/8)(g_e+g_\nu)$; afterward only photons and neutrinos remain, so $g_{\mathrm{after}}=g_\gamma+(7/8)g_\nu$. Entropy conservation then forces the neutrino temperature to dilute relative to the photon bath by $(T_\nu/T_\gamma)^3=g_{\mathrm{after}}/g_{\mathrm{before}}=4/11$, and the present-day $g_{*s}$ becomes $43/11$. The Riemann value $\zeta(3)$ appears in the number-density integrals that convert energy densities into particle counts per photon.

This module records those constants as MODEL inputs. Downstream modules discharge the $7/8$ weight and the dilution law from series and FRW identities.

proof idea

Definition module: no substantive proofs. Constants gPhoton, gElectron, gNeutrino, and fermionWeight are numeric MODEL inputs. gBefore and gAfter are arithmetic combinations of those inputs. dilutionCubed_eq and gStarS_eq are one-line algebraic rewrites equating the named symbols to the rationals $4/11$ and $43/11$. zeta3 is the series $\sum n^{-3}$ with a summability certificate zeta3_summable imported from Mathlib.

why it matters in Recognition Science

This is the MODEL layer that every entropy-per-photon identity in the Cosmology stack imports. FermionWeight upgrades the bare fermionWeight = 7/8 input to the series identity $\eta(4)=(7/8)\zeta(4)$; FermionWeightIntegral lifts that to the thermodynamic Fermi–Dirac versus Bose–Einstein energy integrals. NumberDensityIntegral closes the $s=3$ number-density layer (including the $3/4$ fermion weight) that feeds entropyPerPhoton_eq_ratio. NeutrinoDilution turns dilutionCubed and gStarS into theorems $(T_\nu/T_\gamma)^3=4/11$ and $g_{*s}=43/11$ once comoving entropy conservation and the $1/a$ redshift law are discharged from the FRW continuity equation.

Without these named constants the later modules would have nowhere to attach their discharges. In the broader Recognition framework they sit in the cosmology bookkeeping that connects the eight-tick and $\phi$-ladder structure to observable $N_{\mathrm{eff}}$ and baryon-to-photon ratios, but the present file itself is pure Standard-Model thermodynamics.

scope and limits

Does not derive the 7/8 fermion weight; that is discharged in FermionWeight and FermionWeightIntegral.
Does not prove neutrino dilution or g_*s from FRW; NeutrinoDilution and EntropyConservationFRW do.
Does not evaluate number-density or energy-density integrals; those live in NumberDensityIntegral.
Does not claim RS-native forcing of g_γ, g_e, or g_ν; they remain MODEL inputs.
Does not address non-equilibrium or beyond-Standard-Model entropy sources.

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Cosmology.FermionWeight module_import
IndisputableMonolith.Cosmology.FermionWeightIntegral module_import
IndisputableMonolith.Cosmology.NeutrinoDilution module_import
IndisputableMonolith.Cosmology.NumberDensityIntegral module_import

declarations in this module (43)

def gPhoton L81
def gElectron L84
def gNeutrino L87
def fermionWeight L99
def gBefore L103
def gAfter L106
def dilutionCubed L119
theorem dilutionCubed_eq L121
def gStarS L127
theorem gStarS_eq L130
def zeta3 L141
lemma zeta3_summable L143
lemma tail_summable L150
lemma zeta3_split L158
def gLo L172
lemma gLo_nonneg L174
lemma gLo_tendsto L176
lemma gLo_step L183
lemma gLo_antitone L191
lemma hasSum_gLo L196
lemma term_lo L203
lemma tail_ge L210
def gHi L217
lemma gHi_tendsto L219
lemma gHi_step L227
lemma gHi_antitone L235
lemma hasSum_gHi L240
lemma term_hi L247
lemma tail_le L254
lemma S40_gt L260
lemma S40_lt L264
theorem zeta3_gt L271
theorem zeta3_lt L278
theorem zeta3_pos L284
theorem pi4_gt L289
theorem pi4_lt L297
def entropyPerPhoton L308
theorem entropyPerPhoton_eq_formula L312
theorem entropyPerPhoton_eq_ratio L320
theorem entropyPerPhoton_gt L329
theorem entropyPerPhoton_lt L338
theorem entropyPerPhoton_pos L346
theorem entropyPerPhoton_near_704 L352