five_almost_prime_thirtytwo
plain-language theorem explainer
The declaration confirms that 32 equals 2 to the fifth power and therefore carries exactly five prime factors counted with multiplicity. Number theorists building tables of almost-prime factorizations or verifying small cases in arithmetic functions would cite the result. The proof is a direct native decision that evaluates the bigOmega predicate on this concrete input.
Claim. $Ω(32) = 5$, where $Ω(n)$ denotes the total number of prime factors of $n$ counted with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to bigOmega for counting prime factors with multiplicity. The predicate isFiveAlmostPrime n holds exactly when bigOmega n equals 5. This instance records the concrete case n = 32 = 2^5. Upstream, the definition of isFiveAlmostPrime directly encodes the predicate as bigOmega n = 5, while the surrounding file keeps statements minimal pending deeper Dirichlet algebra.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to evaluate the equality bigOmega 32 = 5 directly.
why it matters
The result supplies a verified base case inside the arithmetic-functions module that supports exact prime-factor bookkeeping. It fills a small concrete slot in the NumberTheory.Primes layer without touching the forcing chain, RCL, or phi-ladder. No downstream theorems depend on it, so it functions as an isolated check rather than a load-bearing lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.