pi4_lt
plain-language theorem explainer
Strict upper bound π⁴ < 97.40914, the arithmetic half of the π⁴ window used in the entropy-per-photon ratio. Cosmology and baryogenesis lanes cite it when closing s/n_γ < 7.0396. The proof lifts Mathlib's six-decimal π bound through a monotone fourth-power step and a norm_num comparison.
Claim. $\pi^4 < 97.40914$.
background
The EntropyPerPhoton module derives the present-day ratio $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ in the open interval $(7.0393, 7.0396)$, replacing the bare constant 7.04 in the baryogenesis dynamical prefactor. Three ingredients enter: a $\zeta(3)$ window from a 40-term split, a $\pi^4$ window, and $g_{*s}=43/11$ from Standard Model particle content (photon 2 polarizations, $e^\pm$ 4 fermionic dof, three neutrino generations 6 fermionic dof) with the $7/8$ fermion weight proved from series and thermodynamic integrals.
The $\pi^4$ window is stated in the module doc as $97.40900 < \pi^4 < 97.40914$ (true value $\approx 97.409091$), taken from Mathlib's six-decimal bounds on $\pi$. This declaration is the strict upper half of that window. Sibling material in the file includes the $\zeta(3)$ sum, $g_{*s}$, and dilution factors; the entropy symbols appearing in the dependency list are ambient thermodynamics/ledger definitions, not inputs to this arithmetic step.
proof idea
One short calc. Invoke Mathlib's Real.pi_lt_d6 to get $\pi < 3.141593$. Raise both sides to the fourth power with pow_lt_pow_left₀, using positivity of $\pi$ and the exponent $4 > 0$. Finish by norm_num on $(3.141593)^4 < 97.40914$. No Recognition-specific lemmas are required; the argument is pure real analysis plus decimal arithmetic.
why it matters
Closes the upper $\pi^4$ edge needed for the entropy-per-photon upper bound. Downstream, entropyPerPhoton_lt applies this fact together with the lower $\zeta(3)$ bound to prove $s/n_\gamma < 7.0396$ after unfolding the ratio and clearing the positive denominator $45\zeta(3)$. That bound is the analytic replacement for the bare 7.04 constant in the baryogenesis dynamical lane (EpsilonCPFromGap.dynPrefactor).
Within the module status note, this is the "π⁴ window (THEOREM)" half of an analysis-plus-arithmetic derivation over MODEL particle content. It does not touch the forcing chain (T0–T8), RCL, or $\phi$-ladder mass formula; its role is cosmological bookkeeping that feeds CP-asymmetry numerics once $g_{*s}$ and $\zeta(3)$ are in hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.