three_almost_prime_fortyfour
plain-language theorem explainer
The declaration verifies that 44 factors as 2 squared times 11 and therefore satisfies the arithmetic condition for a 3-almost prime. Number theorists building the Recognition Science phi-ladder or mass formulas would cite this concrete check when confirming specific constants. The proof is a direct native decision that evaluates the bigOmega count on 44.
Claim. The integer 44 satisfies $44 = 2^2 · 11$ and therefore has total prime factor count with multiplicity equal to three.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function, and keeps statements minimal until Dirichlet inversion layers are added. The central definition states that a number is 3-almost prime precisely when its bigOmega value equals 3. This places the result inside the NumberTheory.Primes.ArithmeticFunctions setting that supports later prime-related constructions in the Recognition framework.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the boolean isThreeAlmostPrime 44 directly.
why it matters
This instance check for 44 populates the arithmetic functions library with verified 3-almost primes that feed the Recognition Science number-theoretic toolkit. It supports the broader use of prime factor counts in deriving constants on the phi-ladder, consistent with the module's role as a Möbius foothold. No downstream theorems are listed yet, leaving the result as a concrete data point rather than a general lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.