gHi
plain-language theorem explainer
Defines the upper telescoping comparator sequence g_n = 1/(2(n+40)(n+41)) used to bound the ζ(3) tail from above. Cosmology proofs cite it to trap ∑_{n≥41} n^{-3} ≤ 1/3280 via partial-fraction differences. The body is a one-line closed-form definition; all analytic content lives in the companion lemmas on steps, monotonicity, and the telescoping sum.
Claim. For each natural number $n$, set $g^{\mathrm{hi}}_n := \dfrac{1}{2(n+40)(n+41)} \in \mathbb{R}$. This is the upper telescoping comparator for the tail of $\zeta(3)$.
background
The EntropyPerPhoton module derives the entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ in the narrow window $(7.0393, 7.0396)$, replacing a bare $7.04$ constant in the baryogenesis lane. One of the three ingredients is a rigorous window on $\zeta(3) = \sum_{k\ge 1} k^{-3}$.
The series is split after 40 terms. The partial sum $S_{40}$ is evaluated by exact rational arithmetic. The tail $\sum_{n\ge 41} n^{-3}$ is trapped between two telescoping comparators. The upper comparator is this sequence: differences of $1/(2(n+40)(n+41))$ dominate the cubic terms via $1/((n+40)(n+41)(n+42)) \ge 1/(n+41)^3$.
A matching lower comparator (sibling $g^{\mathrm{lo}}$) supplies the other side, yielding $1/3444 \le \mathrm{tail} \le 1/3280$ and hence $1.202042 < \zeta(3) < 1.202065$.
proof idea
Pure definition: the body is the closed form $1/(2((n:\mathbb{R})+40)((n:\mathbb{R})+41))$. No tactics. Downstream lemmas unfold it: gHi_step computes the forward difference by field_simp; gHi_antitone and gHi_tendsto follow by positivity and a squeeze; hasSum_gHi identifies the telescoping sum with $g^{\mathrm{hi}}_0$.
why it matters
This comparator is the upper half of the ζ(3) window that feeds the entropy-per-photon theorem. Downstream, term_hi shows each cubic tail term is ≤ the corresponding difference of $g^{\mathrm{hi}}$; hasSum_gHi sums those differences to $g^{\mathrm{hi}}0 = 1/3280$; and tail_le concludes $\sum{n\ge 41}(n)^{-3} \le 1/3280$.
Together with the matching lower bound and the $\pi^4$ and $g_{*s}=43/11$ windows, the module upgrades the baryogenesis dynamical prefactor from a fitted $7.04$ to a derived interval $(7.0393, 7.0396)$. The construction is classical analysis over Standard Model particle content, not a Recognition-forcing step (T0–T8), but it closes an arithmetic gap in the cosmology lane that consumes RS mass and CP structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.