Divisor Count and Radical Rigidity
Abstract
A positive integer whose divisor count divides its squarefree kernel has those two quantities equal.
Theorem 1.1 (Distinct prime factors bound the prime factors of the divisor count).
Proof. Machine-checked in Lean as D5/S3/Arith/DivisorCountRadicalCoincidence.primeFactors_card_le_cardFactors_card_divisors (✓ std3). ∎
Source. Repository-derived.
Commentary.
For a nonzero natural number k, the number of its distinct prime factors is at most the number of prime factors of its divisor count, counted with multiplicity. Each positive exponent contributes a factor greater than one to the prime-exponent product for the divisor count.
Theorem 1.2 (Divisibility forces equality).
Proof. Machine-checked in Lean as D5/S3/Arith/DivisorCountRadicalCoincidence.radical_eq_card_divisors_of_dvd (✓ std3). ∎
Source. Repository-derived.
Commentary.
The radical is squarefree, so every divisor of it is squarefree. The prime-exponent product for the divisor count contributes at least one prime factor for every distinct prime factor of k. Divisibility gives the reverse bound on distinct prime factors. The two prime-factor sets therefore coincide, and their products give the stated equality.