five_almost_prime_twohundredfortythree
plain-language theorem explainer
The declaration verifies that 243 factors as 3 to the fifth power and therefore carries exactly five prime factors counted with multiplicity. Number theorists populating tables of almost-primes for Recognition Science ladder calculations would cite this concrete case. The proof is a one-line native_decide term that evaluates the big-Omega predicate directly.
Claim. $243 = 3^5$ satisfies $Omega(243) = 5$, where $Omega(n)$ counts all prime factors of $n$ with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The predicate isFiveAlmostPrime is defined by the equality bigOmega n = 5, where bigOmega returns the total number of prime factors counted with multiplicity. Upstream results include the definition of isFiveAlmostPrime together with several is predicates from foundation modules that function as collision-free or algebraic-tautology checks.
proof idea
The proof is a term-mode native_decide invocation that directly evaluates the boolean equality by computing bigOmega 243 and confirming it equals 5.
why it matters
This instance supplies a verified five-almost-prime example inside the arithmetic-functions layer. It supports concrete checks on the phi-ladder for mass formulas, although no downstream theorems currently reference it. The declaration closes a small verification point in the NumberTheory.Primes.ArithmeticFunctions module without touching the forcing chain or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.