four_almost_prime_thirtysix
plain-language theorem explainer
36 equals 2 squared times 3 squared and therefore has exactly four prime factors counting multiplicity, satisfying the definition of a 4-almost prime. Number theorists working with arithmetic functions in the Recognition Science context would cite this as a verified concrete instance. The proof reduces directly to a computational check via native decision.
Claim. $36 = 2^2 3^2$ satisfies $Omega(36) = 4$, where $Omega$ counts prime factors with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to bigOmega for total prime factor counts. A number n is declared 4-almost prime precisely when bigOmega n equals 4, as defined in the sibling isFourAlmostPrime. The local setting keeps statements minimal to support later Dirichlet inversion once interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the equality bigOmega 36 = 4 directly.
why it matters
This supplies a checked example inside the arithmetic functions layer of NumberTheory.Primes, supporting downstream prime-related arguments even though no immediate used_by edges appear. It contributes concrete verification to the Möbius footholds without touching the forcing chain T0-T8 or RS constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.