three_almost_prime_sixtythree
plain-language theorem explainer
63 factors as 3 squared times 7 and therefore has exactly three prime factors counted with multiplicity. Number theorists verifying small cases inside the Recognition Science arithmetic layer would cite this concrete evaluation. The proof is a one-line wrapper that invokes native_decide to compute the bigOmega count directly.
Claim. $63$ is 3-almost prime, i.e., the total number of prime factors of $63$ counted with multiplicity equals three.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. A number $n$ is 3-almost prime when its bigOmega value equals three. The upstream definition states: def isThreeAlmostPrime (n : ℕ) : Bool := bigOmega n = 3.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the boolean expression isThreeAlmostPrime 63.
why it matters
This theorem supplies a verified instance of the 3-almost prime condition for 63. It contributes to the arithmetic functions module, which prepares for deeper Dirichlet algebra once basic interfaces stabilize. No parent theorems appear in the used_by edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.