six_almost_prime_fourhundred
plain-language theorem explainer
The theorem states that 400 equals 2 to the fourth times 5 squared and therefore carries exactly six prime factors counted with multiplicity. Number theorists checking concrete cases inside the Recognition Science arithmetic layer would reference this instance when validating the six-almost-prime predicate. The proof reduces to a single native decision step on the bigOmega definition.
Claim. $Ω(400)=6$, where $Ω(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 6-almost prime precisely when bigOmega $n$ equals 6. The present declaration checks this predicate at $n=400$, whose factorization is $2^4 × 5^2$.
proof idea
The proof is a one-line term wrapper that applies native_decide directly to the equality isSixAlmostPrime 400 = true. This evaluates the definition bigOmega 400 = 6 by computing the prime factorization in place.
why it matters
The result supplies a verified concrete instance for the arithmetic functions library that supports the Recognition Science number-theory layer. It aligns with the Möbius footholds in the module documentation and the isSixAlmostPrime definition, which encodes the bigOmega equality without new axioms. No downstream theorems are listed, so the declaration functions as a terminal check rather than an intermediate step in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.