---
id: F-013
title: Elementary logarithmic bound on distinct prime factors
tier: lean
polarity: positive
depends_on: []
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-013_distinct-prime-factor-card-bound/lean/Research/PrimeFactorCard.lean workspace/experiments/experiment_2_elementary_upper_bound/lean/Research/PrimeFactorCard.lean && (cd workspace/experiments/experiment_2_elementary_upper_bound/lean && lake build)
date: 2026-07-11
---

## Statement

For every nonzero natural `n`,

\[
2^{\omega(n)}\le n,
\qquad
\omega(n)\log 2\le\log n,
\]

where `ω(n)=n.primeFactors.card` counts distinct prime factors.

Formal theorems: `two_pow_card_primeFactors_le` and
`card_primeFactors_mul_log_two_le_log`.

## Proof / verification

Every prime factor is at least two, so their distinct product is at least
`2^ω(n)`; Mathlib proves that this product divides `n`, hence is at most `n`.
Casting and monotonicity of the real logarithm yield the second inequality.
Lean accepts the proof with no `sorry`, `admit`, or axioms.
