module module moderate

`IndisputableMonolith.Cosmology.EntropyPerPhoton`

Definition layer for early-universe entropy bookkeeping: photon/electron/neutrino internal dof, the 7/8 fermion weight as a MODEL input, before/after g_* counts, the cubed neutrino dilution 4/11, and g_*s = 43/11. Cosmology modules cite it as the shared constant vocabulary. Structure is definitions plus elementary arithmetic identities; analytic discharge of 7/8 and FRW entropy conservation live downstream.

claimPackages the relativistic internal degrees of freedom $g_\gamma=2$, $g_e$, $g_\nu$, the fermion entropy weight $7/8$, effective entropy dof $g_{*s}$ before and after $e^+e^-$ annihilation, the neutrino dilution identity $(T_\nu/T_\gamma)^3=4/11$, $g_{*s}=43/11$ in the late radiation era, and $\zeta(3)$ (with summability) for number-density integrals.

background

In standard radiation-era thermodynamics the entropy density of a bosonic species scales as $g T^3$; fermions carry an extra factor $7/8$ from the Fermi–Dirac integral relative to Bose–Einstein. Photons have two polarization states. When $e^+e^-$ annihilate, their entropy is dumped into the photon bath while decoupled neutrinos free-stream, producing the textbook dilution $(T_\nu/T_\gamma)^3=4/11$ and the late-time effective entropy dof $g_{*s}=43/11$.

This module sits in the Cosmology domain of the Recognition Science mirror. It records those constants and the elementary $g$-counting identities as Lean definitions, flagging the fermion weight (and related inputs) as MODEL data. Downstream modules replace the MODEL status by series and integral theorems and by FRW entropy conservation.

proof idea

Definition module, not a deep proof development. Internal dof and fermionWeight = 7/8 are introduced as named constants (MODEL inputs). Before/after effective $g$ counts are assembled from those constants; dilutionCubed_eq and gStarS_eq are direct arithmetic rearrangements yielding $4/11$ and $43/11$. zeta3 and zeta3_summable record the $\zeta(3)$ series data needed later for number-density integrals. No Mellin-transform analysis or FRW dynamics is proved here.

why it matters in Recognition Science

Four Cosmology parents import this vocabulary. FermionWeight upgrades the MODEL input to the series identity $\eta(4)=(7/8)\cdot\zeta(4)$. FermionWeightIntegral closes the thermodynamic gap: the Fermi–Dirac energy integral is $7/8$ of the Bose–Einstein one. NumberDensityIntegral supplies the $s=3$ number-density layer (including the $3/4$ fermion weight) required by the entropyPerPhoton_eq_ratio formula. NeutrinoDilution derives $(T_\nu/T_\gamma)^3=4/11$ and $g_{*s}=43/11$ from entropy conservation once the FRW hypotheses are discharged in EntropyConservationFRW.

Within Recognition Science this is the classical interface for photon-era entropy bookkeeping. It does not itself touch the forcing chain (T0–T8), RCL, or the phi-ladder; those enter only through the broader cosmology stack that consumes these ratios.

scope and limits

Does not derive fermion weight 7/8 from eta/zeta series or FD/BE integrals.
Does not prove comoving entropy conservation or the $1/a$ redshift law.
Does not evaluate a numerical entropy-per-photon beyond ratio identities.
Does not address RS forcing (T0–T8), RCL, or phi-ladder masses.
Does not model non-equilibrium or beyond-SM relativistic species.

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