Exact three-term geometric lower ratio v4

Proved

OddPerfectNumber.geom_ratio_lower_three_terms_exact_v4

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_v4 (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 close the normalized equality with a simp-only reflexivity step.

View graph