six_almost_prime_threehundredtwentyfour
plain-language theorem explainer
Verification that 324 factors as 2 squared times 3 to the fourth and therefore satisfies Ω(n) = 6 appears as a direct computation. Number theorists populating tables of 6-almost primes for phi-ladder mass estimates or rung calculations would cite this instance. The proof applies native_decide to evaluate the boolean predicate defined via bigOmega.
Claim. $Ω(324) = 6$, where $Ω$ counts the total number of prime factors with multiplicity and $324 = 2^2 · 3^4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The predicate isSixAlmostPrime n holds exactly when bigOmega n equals 6, with bigOmega n defined as the sum of the exponents in the prime factorization of n. Sibling declarations establish related maps such as mobius and bigOmega_apply for squarefree and multiplicity counts.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate isSixAlmostPrime 324 directly from its definition bigOmega 324 = 6.
why it matters
This instance supplies a concrete 6-almost prime at 324 that may enter mass formulas on the phi-ladder or eight-tick octave steps. It anchors arithmetic infrastructure in the NumberTheory.Primes.ArithmeticFunctions module but feeds no downstream theorems. The local setting keeps statements lightweight until deeper Dirichlet algebra stabilizes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.