six_almost_prime_fivehundredtwentyeight
plain-language theorem explainer
528 factors as 2^4 × 3 × 11 and therefore carries exactly six prime factors counted with multiplicity. Number theorists building almost-prime tables or Recognition Science applications to arithmetic functions cite this concrete case because the factor 11 is flagged as RS-relevant. The verification is a direct native_decide evaluation of the bigOmega predicate.
Claim. The natural number 528 satisfies $Ω(528)=6$, 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 but extending to bigOmega for prime-factor counting. A 6-almost prime is defined by isSixAlmostPrime n := bigOmega n = 6, where bigOmega n equals the sum of exponents in the prime factorization of n. This sits inside NumberTheory.Primes.ArithmeticFunctions, whose module doc describes the file as providing Möbius footholds that can later support Dirichlet algebra and inversion.
proof idea
The proof is a term-mode one-liner that applies native_decide directly to the equality isSixAlmostPrime 528 = true. The tactic evaluates the definition bigOmega 528 = 6 by computing the factorization 2^4 × 3 × 11 and confirming the exponent sum equals six.
why it matters
This supplies a concrete 6-almost prime instance at 528 with the factor 11 marked RS-relevant, supporting the development of arithmetic functions inside the Recognition Science framework. No parent theorems appear in the used_by edges, so the declaration functions as a base case for future results that may link prime-factor counts to the phi-ladder or forcing-chain constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.