pi4_gt
plain-language theorem explainer
Strict lower bound π⁴ > 97.40900 on the reals. Cosmology and baryogenesis calculations cite it when trapping the entropy-per-photon window s/n_γ = π⁴ g*s/(45 ζ(3)). The proof lifts Mathlib's six-decimal lower bound on π through a fourth-power comparison with a short calc and norm_num.
Claim. One has $\pi^4 > 97.40900$ as a strict inequality of real numbers.
background
The EntropyPerPhoton module derives the present-day entropy-to-photon ratio
$s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$
in the open interval $(7.0393, 7.0396)$, replacing a bare $7.04$ constant in the baryogenesis dynamical prefactor. The three inputs are a $\zeta(3)$ window, a $\pi^4$ window, and $g_{*s}=43/11$ from Standard Model particle content with the fermionic $7/8$ weight proved rather than assumed.
The $\pi^4$ window is obtained from Mathlib's decimal bounds on $\pi$. The companion upper bound is $\pi^4 < 97.40914$; the true value is about $97.409091$. This declaration is only the lower half of that window.
proof idea
Start from Mathlib's Real.pi_gt_d6, which gives $\pi > 3.141592$. A one-step norm_num check shows $97.40900 < (3.141592)^4$. Then pow_lt_pow_left₀ lifts the strict inequality on the base through the fourth power (exponent positive, base positive), yielding $97.40900 < \pi^4$.
why it matters
Parent use is entropyPerPhoton_gt, which proves $s/n_\gamma > 7.0393$ by unfolding the entropy-per-photon formula and combining this lower bound on $\pi^4$ with the upper bound on $\zeta(3)$ and positivity. That ratio is the analytic replacement for the bare $7.04$ in the baryogenesis dynamical lane (EpsilonCPFromGap.dynPrefactor).
Within Recognition Science cosmology this is pure analysis-plus-arithmetic scaffolding: it does not invoke the forcing chain (T0–T8), RCL, or the $\phi$-ladder, but it closes a numeric gate so the entropy-per-photon claim is a theorem over model particle content rather than a fitted constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.