four_almost_prime_fiftysix
plain-language theorem explainer
The declaration verifies that 56 factors as 2^3 times 7 and therefore satisfies Omega(56) equals 4. Number theorists tabulating almost-prime counts would reference this concrete check. The proof reduces directly to native evaluation of the big-Omega definition.
Claim. $56 = 2^3 7$ and therefore satisfies $Omega(56) = 4$, 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 and extending to big-Omega. A number is 4-almost prime precisely when bigOmega n equals 4. The upstream definition states: a number is 4-almost prime if Omega(n) equals 4. This instance checks the concrete factorization 56 = 2 cubed times 7 against that predicate.
proof idea
The proof is a one-line wrapper that applies native_decide to the equality isFourAlmostPrime 56 = true, which reduces immediately to evaluating bigOmega 56.
why it matters
This supplies a verified base case inside the arithmetic-functions module for 4-almost primes. It anchors concrete integer checks that can feed later number-theoretic constructions, though no downstream uses are recorded. The result sits within the broader Recognition Science scaffolding that treats arithmetic functions as footholds before deeper Dirichlet or inversion layers are added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.