six_almost_prime_fourhundredeightysix
plain-language theorem explainer
486 factors as 2 times 3 to the fifth power, so its total prime multiplicity is exactly six and it meets the six-almost-prime criterion. Number theorists working inside the Recognition Science arithmetic-function layer would cite the check when validating concrete integers against the big-Omega threshold. The proof is a one-line native decision that evaluates the predicate directly on the input.
Claim. $486 = 2^1 3^5$ satisfies $Omega(486) = 6$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. A number is six-almost-prime precisely when the total number of prime factors counted with multiplicity equals six, as defined by the big-Omega function. This declaration checks the concrete case 486 against that definition, relying on the upstream predicate that returns true exactly when bigOmega n equals 6.
proof idea
The proof is a one-line wrapper that applies the native decision procedure to evaluate the six-almost-prime predicate directly on 486.
why it matters
The result supplies an explicit verified example inside the arithmetic-function infrastructure that Recognition Science uses for prime-related constructions. It sits alongside other concrete checks (such as the 528 case flagged as RS-relevant because of the factor 11) and supports the lightweight Möbius and big-Omega layer described in the module. No downstream theorems are listed, so the declaration functions as a concrete anchor rather than a lemma feeding a larger proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.