fermi_series
plain-language theorem explainer
For every positive real t, the Fermi–Dirac factor 1/(e^t+1) equals the alternating geometric series ∑_{n≥0} (−1)^n e^{−(n+1)t} as an unconditional real sum. Cosmology and statistical-mechanics proofs that convert Fermi kernels into Dirichlet η-series cite this identity. The argument is a norm-controlled geometric series with ratio −e^{−t}, followed by algebraic simplification of the closed form.
Claim. For every real $t>0$, the series $\sum_{n=0}^{\infty}(-1)^n\,e^{-(n+1)t}$ converges unconditionally to $1/(e^{t}+1)$.
background
This module sits at the thermodynamic (integral) layer of the Recognition Science entropy bookkeeping. The sibling module FermionWeight already proved the pure series identity η(4)=(7/8)ζ(4). What remains is to identify the Fermi–Dirac energy integral ∫ t³/(e^t+1) dt with Γ(4)·η(4), and the Bose–Einstein integral with Γ(4)·ζ(4), so the 7/8 ratio passes from Dirichlet series to physical integrals.
Both kernels expand as geometric series in e^{−t}. The Bose kernel is ∑ e^{−(n+1)t} = 1/(e^t−1); the Fermi kernel is the alternating version ∑ (−1)^n e^{−(n+1)t} = 1/(e^t+1). Mathlib’s Mellin-of-power-series lemma then turns each expansion into a shifted Dirichlet sum at s=4 (or s=3 for number density).
The present lemma is exactly the Fermi geometric identity, stated as a HasSum so it plugs directly into the Mellin machinery. The hypothesis t>0 guarantees |−e^{−t}|<1, which is the geometric-series radius condition.
proof idea
Set r := e^{−t}. Positivity of the exponential gives 0<r, and t>0 forces r<1, hence ‖−r‖<1. Apply Mathlib’s hasSum_geometric_of_norm_lt_one to the series ∑ (−r)^n, then multiply on the left by r to obtain ∑ (−1)^n r^{n+1} = r/(1−(−r)).
A short field calculation rewrites the closed form: r/(1+r) = e^{−t}/(1+e^{−t}) = 1/(e^t+1). Congruence of the summand finishes the proof (neg_pow and pow_succ rearrange the powers). No Recognition-specific lemmas are used; the argument is pure real analysis.
why it matters
This is the Fermi half of the geometric-series bridge that turns the series identity η(4)=(7/8)ζ(4) into the thermodynamic statement ∫ t³/(e^t+1) dt = (7/8) ∫ t³/(e^t−1) dt. Downstream, hasSum_mellin_fermi feeds the alternating coefficients into Mathlib’s Mellin transform at s=4, recovering Γ(4)·η(4) as the energy integral; hasSum_mellin_fermi3 does the same at s=3 for number density.
Once both Mellin identities are in place, the entire mathematical content of EntropyPerPhoton.fermionWeight = 7/8 is theorem-level: only the g* species census remains model content. The module doc records that all theorems here are axiom-clean (Lean’s base three only). The lemma does not itself touch the forcing chain T0–T8 or the Recognition Composition Law; it is classical analysis supporting the cosmology entropy ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.