Exact three-term geometric lower ratio v3

Proved

OddPerfectNumber.geom_ratio_lower_three_terms_exact_v3

by WillR · Sep 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

For every positive exponent index, the final three terms of the geometric sum give the exact lower ratio (q²+q+1)/q².

Preamble

import Mathlib
import Theorems.Thm_OddPerfectNumber_geom_sum_last_three_terms_le

Formal statement

namespace OddPerfectNumber

theorem geom_ratio_lower_three_terms_exact_v3 (q e : Nat) (he : 1 ≤ e) : (q^2 + q + 1) * q^(2*e) ≤ q^2 * (∑ i ∈ Finset.range (2*e + 1), q^i) := by
  sorry

end OddPerfectNumber

Source

Scale the accepted last-three-term bound by q² and use explicit equality normalization; the reflexive final calc step is discharged by the calc chain itself.

View graph