Canonical q3=29 small-D support cases v6
ProvedOddPerfectNumber.k_one_q2_five_q3_twentynine_small_D_cases_canonical_v6canonical-reductionfour-supportodd-perfectq2-fiveq3-twentyninesmall-d
The canonical q3=29 small-D support enumeration with separate hypothesis normalization in four bounded intervals.
Preamble
import Mathlib
Formal statement
namespace OddPerfectNumber theorem k_one_q2_five_q3_twentynine_small_D_cases_canonical_v6 (D p q4 : Nat) (hDgt : 15 < D) (hDlt : D < 75) (hDodd : Odd D) (hp : p.Prime) (hp_eq : p = 2 * D - 1) (hq4gt : 29 < q4) (hDsupport : ∀ r, r.Prime → r ∣ D → r = 3 ∨ r = 5 ∨ r = 29 ∨ r = q4) : D = 27 ∨ D = 31 ∨ D = 37 ∨ D = 45 := by sorry end OddPerfectNumber
Source
Finite canonical support reduction with separate hDodd and hp normalization stages to avoid closed-goal sequencing failures.