gLo_antitone
plain-language theorem explainer
Consecutive differences of the lower telescoping comparator for the ζ(3) tail are nonnegative: g_lo(n) ≥ g_lo(n+1) for every natural n. Anyone assembling the HasSum of that telescoping series (to trap the Apéry-constant tail) cites this. The proof rewrites the difference by the closed-form step identity and finishes by positivity.
Claim. For every natural number $n$, if $g_{\mathrm{lo}}(n) = \frac{1}{2(n+41)(n+42)}$, then $0 \leq g_{\mathrm{lo}}(n) - g_{\mathrm{lo}}(n+1)$. Equivalently, the sequence $g_{\mathrm{lo}}$ is nonincreasing on $\mathbb{N}$.
background
The module derives the entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ in the window $(7.0393, 7.0396)$, replacing a bare $7.04$ constant in the baryogenesis lane. One ingredient is a rigorous window on $\zeta(3)=\sum 1/(n+1)^3$: a partial sum through 40 terms plus a trapped tail.
The lower comparator $g_{\mathrm{lo}}(n)=1/(2(n+41)(n+42))$ is the telescoping series whose differences under-estimate the cubic tail terms. The sibling step lemma records the exact difference $g_{\mathrm{lo}}(n)-g_{\mathrm{lo}}(n+1)=1/((n+41)(n+42)(n+43))$, which is the comparison term used against $1/(n+41)^3$.
proof idea
Term-mode proof in three steps. Rewrite the goal by the step identity, so the claimed difference becomes the explicit positive rational $1/((n+41)(n+42)(n+43))$. Record nonnegativity of the real cast of $n$. Discharge the resulting inequality by the positivity tactic, which sees a reciprocal of a product of three strictly positive linear terms.
why it matters
Feeds hasSum_gLo, which applies the Mathlib criterion hasSum_iff_tendsto_nat_of_nonneg and therefore needs nonnegativity of consecutive differences. That HasSum identifies the infinite sum of lower differences with $g_{\mathrm{lo}}(0)$, closing the lower half of the telescoping trap $1/3444 \leq \mathrm{tail}$ on $\zeta(3)$.
Inside the Recognition cosmology stack this is pure analysis scaffolding for the entropy-per-photon theorem that upgrades the dynamical prefactor in baryogenesis from a numeric constant to a derived interval. It does not touch the forcing chain (T0–T8) or the J-cost directly; it sits in the Standard-Model-content arithmetic that produces $g_{*s}=43/11$ and the $\zeta(3)$, $\pi^4$ windows.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.