Canonical q3=23 large-D D upper cut v4
ProvedOddPerfectNumber.k_one_q2_five_q3_twentythree_large_D_D_le_685_v4canonical-reductionfour-supportodd-perfectq2-fiveq3-twentythree
After the accepted fourth-prime window and divisibility reduction, the q3=23 large-D abundance inequality forces D <= 685.
Preamble
import Mathlib import Theorems.Thm_OddPerfectNumber_geom_sum_cross_lt_of_le import Theorems.Thm_OddPerfectNumber_k_one_q2_five_q3_twentythree_large_D_q4_cases
Formal statement
namespace OddPerfectNumber theorem k_one_q2_five_q3_twentythree_large_D_D_le_685_v4 (m a b c e D p q4 sigma : Nat) (hfac : m ^ 2 = 3 ^ (2*a) * 5 ^ (2*b) * 23 ^ (2*c) * q4 ^ (2*e)) (hsigma : sigma = (∑ i ∈ Finset.range (2*a + 1), 3 ^ i) * (∑ i ∈ Finset.range (2*b + 1), 5 ^ i) * (∑ i ∈ Finset.range (2*c + 1), 23 ^ i) * (∑ i ∈ Finset.range (2*e + 1), q4 ^ i)) (hrel : D * sigma = p * m ^ 2) (hDlow : 111 ≤ D) (hDodd : Odd D) (hp : p.Prime) (hp4 : p % 4 = 1) (hp_eq : p = 2 * D - 1) (hq4prime : q4.Prime) (hq4gt47 : 47 < q4) (hq4le : q4 ≤ 61) (hq4dvd : q4 ∣ D) (hDsupport : ∀ r, r.Prime → r ∣ D → r = 3 ∨ r = 5 ∨ r = 23 ∨ r = q4) (ha : 5 ≤ a) (hb : 3 ≤ b) (hc : 4 ≤ c) (he : 1 ≤ e) : D ≤ 685 := by sorry end OddPerfectNumber
Source
The geometric-sum upper inequality gives a strict linear coefficient bound. The accepted prime window splits q4 into 53, 59, and 61; divisibility writes D=q4*k. The 59 and 61 arms are immediately below 685, while the only q4=53 values above 685 are eliminated by rewriting p=2*D-1 before the finite checks. The q4=53 finite split is terminal after those checks, so no dead fallback tactic follows it.