entropyPerPhoton_pos

The module derives the CMB-era entropy-to-photon ratio used in the baryogenesis lane,

$$s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3)),$$

with model particle content fixing $g_{*s}=43/11$ (2 photon polarizations, $e^\pm$ and three neutrino species with the fermionic $7/8$ weight). The bare staging constant 7.04 is replaced by a certified window $(7.0393,7.0396)$.

Here entropyPerPhoton is exactly that real: $\pi^4\cdot(43/11)/(45\zeta(3))$, where $\zeta(3)=\sum_{n\ge1}n^{-3}$ is trapped by a 40-term partial sum plus telescoping tail bounds, and $\pi^4$ comes from Mathlib's six-decimal $\pi$ inequalities. The sibling theorem entropyPerPhoton_gt already gives the strict lower bound $7.0393 < s/n_\gamma$.

Term-mode application of real strict-order transitivity. The first leg is by norm_num, which discharges $0 < 7.0393$. The second leg is the upstream theorem entropyPerPhoton_gt ($7.0393 < \texttt{entropyPerPhoton}$). Composing them yields $0 < \texttt{entropyPerPhoton}$. No unfolding of $\pi$, $\zeta(3)$, or $g_{*s}$ is required at this step.

Positivity is the minimal analytic hygiene for any formula that treats $s/n_\gamma$ as a scale in baryogenesis or entropy-density conversions (the module's stated consumer is the dynamical prefactor that previously hard-coded 7.04). It sits under the same derivation chain that proves the three-significant-figure match $|s/n_\gamma-7.04|<0.0007$ and the tight window from $\zeta(3)$, $\pi^4$, and $g_{*s}=43/11$. No downstream Lean users are recorded yet; the result is infrastructure for those numerical and dynamical lemmas rather than a forcing-chain (T0–T8) step.