Canonical q3=29 finite small-D terminal after the lower cut

Proved

OddPerfectNumber.k_one_q2_five_q3_twentynine_D15_lt_D_lt_75_absurd_v1

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

four-supportodd-perfectq2-fiveq3-twentyninereduced-compositionsmall-d

After the accepted lower-abundance cut 15<D, the canonical q3=29 small-D candidates are exactly D=31,37,45 and the accepted terminal dispatcher contradicts each.

Preamble

import Mathlib
import Theorems.Thm_OddPerfectNumber_k_one_q2_five_q3_twentynine_small_D_cases_v2
import Theorems.Thm_OddPerfectNumber_k_one_q2_five_q3_twentynine_D31_D37_D45_reduced_absurd_v2

Formal statement

namespace OddPerfectNumber

theorem k_one_q2_five_q3_twentynine_D15_lt_D_lt_75_absurd_v1 (m d D p q4 sigma a b c e : Nat) (hfac : m ^ 2 = 3 ^ (2*a) * 5 ^ (2*b) * 29 ^ (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), 29 ^ i) * (∑ i ∈ Finset.range (2*e + 1), q4 ^ i)) (hrel : D * sigma = p * m ^ 2) (hDgt : 15 < D) (hDlt : D < 75) (hDodd : Odd D) (hp : p.Prime) (hp_eq : p = 2 * D - 1) (hp4 : p % 4 = 1) (hq4prime : q4.Prime) (hq4gt : 29 < q4) (hDq : D < q4) (hDsupport : ∀ r, r.Prime → r ∣ D → r = 3 ∨ r = 5 ∨ r = 29 ∨ r = q4) (hm0 : m ≠ 0) (hsig : (∑ x ∈ (m ^ 2).divisors, x) = p * d) (hglobal : sigma = ∑ x ∈ (m ^ 2).divisors, x) (hddvd : d ∣ m ^ 2) (hsupport : ∀ x ∈ m.primeFactors, x = 3 ∨ x = 5 ∨ x = 29 ∨ x = q4) (ha : 8 ≤ a) (hb : 6 ≤ b) (hc : 4 ≤ c) (he : 2 ≤ e) (hD45q4 : D = 45 → q4 = 31 ∨ q4 = 41) : False := by
  sorry

end OddPerfectNumber

Source

Apply the accepted finite D=31,37,45 candidate theorem and the accepted exact dispatcher; evenness of the doubled exponents is immediate.

View graph