four_almost_prime_eightyeight
plain-language theorem explainer
88 factors as 2^3 times 11 and therefore satisfies Omega(n) = 4. Researchers checking concrete numerical cases of 4-almost primes in the Recognition Science arithmetic layer would cite this result. The proof reduces to a single native decision procedure that evaluates the prime factorization count directly.
Claim. $Omega(88) = 4$, where $Omega(n)$ counts the total number of prime factors of $n$ with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. A number n is 4-almost prime precisely when its total prime factor count with multiplicity equals 4, via the definition isFourAlmostPrime(n) := bigOmega n = 4. The local setting is a collection of small arithmetic identities that can later support Dirichlet inversion once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that invokes native_decide to confirm the equality after expanding the definition of isFourAlmostPrime via bigOmega.
why it matters
This supplies a verified instance of a 4-almost prime at 88, noted as RS-relevant because of the prime factor 11 near the Z_cf threshold. It sits alongside Möbius-related definitions in the ArithmeticFunctions module but records no downstream uses. The result supports concrete numerical checks without engaging the forcing chain or RCL directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.