Canonical q3=19 factor-support form for D v3

Proved

OddPerfectNumber.k_one_q2_five_q3_nineteen_D_factor_support_form_v3

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

If the q2=5,q3=19 square factorization is accepted and D divides m^2, the canonical support restriction yields an exact four-prime factorization of D with exponent bounds.

Preamble

import Mathlib

Formal statement

namespace OddPerfectNumber

theorem k_one_q2_five_q3_nineteen_D_factor_support_form_v3 (m a b c e D q4 : Nat) (hfac : m ^ 2 = 3 ^ (2*a) * 5 ^ (2*b) * 19 ^ (2*c) * q4 ^ (2*e)) (hDdvd : D ∣ m ^ 2) (hDpos : 0 < D) (hq4prime : q4.Prime) (hq4gt : 19 < q4) (hDsupport : ∀ r, r.Prime → r ∣ D → r = 3 ∨ r = 5 ∨ r = 19 ∨ r = q4) : ∃ i j k l, D = 3^i * 5^j * 19^k * q4^l ∧ i ≤ 2*a ∧ j ≤ 2*b ∧ k ≤ 2*c ∧ l ≤ 2*e := by sorry

end OddPerfectNumber

Source

Factorization-coordinate repair v3 after the first two remote compiler diagnostics.

View graph