three_almost_prime_fortyfive
plain-language theorem explainer
The declaration verifies that 45 factors as 3 squared times 5 and therefore satisfies Ω(45) = 3. Recognition Science researchers would cite the result when anchoring the specific numerical constant 45 inside the arithmetic-functions layer. The proof is a one-line wrapper that applies native_decide to evaluate the bigOmega predicate directly.
Claim. $45 = 3^2 × 5$ satisfies $Ω(45) = 3$, where $Ω(n)$ counts the prime factors of $n$ with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The relevant definition states that a natural number is 3-almost prime precisely when bigOmega n equals 3. This instance sits inside the NumberTheory.Primes section and supplies a concrete numerical anchor labeled an RS constant in the declaration comment.
proof idea
The proof is a one-line wrapper that invokes native_decide on the boolean equality produced by the definition isThreeAlmostPrime 45.
why it matters
The result supplies a verified 3-almost-prime instance at 45, recorded as an RS constant. It populates the arithmetic-functions layer that can feed later constructions such as the phi-ladder or mass formulas, even though no downstream uses are recorded yet. The placement aligns with the framework's practice of fixing small numerical values before invoking the Recognition Composition Law or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.