four_almost_prime_onehundredthirtytwo
plain-language theorem explainer
The integer 132 equals 2 squared times 3 times 11 and therefore carries exactly four prime factors counted with multiplicity. Number theorists checking specific almost-prime values inside the Recognition Science arithmetic layer would cite this verification for its tie to the factor 11. The proof reduces to a single native computation of the big-Omega function.
Claim. The positive integer 132 satisfies $Ω(132)=4$, where $Ω(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. A number is 4-almost prime precisely when its big-Omega value equals 4. The instance at 132 is flagged as RS-relevant through the prime factor 11. Upstream results include the definition of the 4-almost-prime predicate as bigOmega n = 4 together with structural 'is' declarations from foundation modules that frame empirical programs and simplicial ledgers.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the equality directly by computing the big-Omega function on 132.
why it matters
This supplies a concrete verified 4-almost-prime instance at 132 that supports the arithmetic-functions module and its Möbius footholds. The factor 11 links to Recognition Science number theory checks on the phi-ladder. No downstream theorems are recorded, so the result functions as a base case rather than feeding a named parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.