six_almost_prime_fivehundredsixty
plain-language theorem explainer
560 factors as 2^4 times 5 times 7 and therefore carries exactly six prime factors counted with multiplicity. Analytic number theorists would cite the fact when verifying small instances of almost primes for sieve estimates or arithmetic-function tables. The proof reduces the predicate directly by native decision on the concrete integer.
Claim. $560 = 2^4 5 7$ satisfies $Omega(560) = 6$, where $Omega(n)$ counts the prime factors of $n$ with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Almost-prime status is expressed through the big-Omega function Ω(n), which tallies prime factors with multiplicity; a six-almost-prime therefore obeys Ω(n) = 6. The local setting keeps statements minimal so that deeper Dirichlet inversion can be added once the basic interfaces are stable.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic, which evaluates the predicate isSixAlmostPrime on the integer 560 by direct factorization and multiplicity count.
why it matters
The declaration supplies a verified concrete example inside the arithmetic-functions module. It supports later checks that involve prime factorizations and Möbius evaluations, although no downstream theorems are recorded. Within the Recognition Science framework it remains a pure number-theoretic fact without direct attachment to the forcing chain T0-T8 or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.