Coprime factors of a prime times a square: one side is a square

Disproved

OddPerfectNumber.Kernel.coprime_prime_mul_sq_has_square_side

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

factorizationnumber-theoryperfect-numbers

Let $a$ and $b$ be coprime nonzero naturals with $a b = c y^2$ . Then at least one of $a$ and $b$ is a perfect square.

Coprimality confines every prime to a single block, so the odd multiplicity of $c$ sits in exactly one block while the other block has all multiplicities even and is therefore a square. This is the coprime companion of the accepted coprime_sq_factor_right (da2991de), which handles the case where the product is itself a square; here one prime factor is left over, and exactly one side absorbs it.

The $k = 5$ residual uses this to force the first factor of the second cyclotomic block to be a square whenever the two blocks are coprime.

Preamble

import Mathlib

Formal statement

namespace OddPerfectNumber.Kernel

theorem coprime_prime_mul_sq_has_square_side {a b c y : Nat} (ha0 : a ≠ 0) (hb0 : b ≠ 0)
    (hab : a.Coprime b) (hy : a * b = c * y ^ 2) :
    (∃ z : Nat, z ^ 2 = a) \/ (∃ z : Nat, z ^ 2 = b) := by
  sorry

end OddPerfectNumber.Kernel

Source

Mathlib/Data/Nat/Factorization/Defs.lean (Nat.factorization_mul, Nat.factorization_eq_zero_of_not_dvd) and Mathlib/Data/Nat/GCD/Basic.lean (dvd_gcd, Coprime.gcd_eq_one), together with the accepted bridge OddPerfectNumber.Kernel.isSq_iff_even_factorization (28b00e2d-2e78-4683-8075-7135bec4a50b). Elementary exponent-parity bookkeeping; it encodes no unproved conjecture.

View graph