semiprime_fifteen
plain-language theorem explainer
The theorem confirms that 15 is semiprime by verifying that its total number of prime factors with multiplicity equals exactly two. Number theorists using arithmetic functions in the Recognition Science setting would cite this as a concrete base case for small semiprimes. The proof reduces immediately to native_decide, which evaluates the bigOmega definition directly.
Claim. $15$ is semiprime, i.e., the total number of prime factors counted with multiplicity satisfies $Ω(15)=2$.
background
The module provides lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function μ. A number n is semiprime when bigOmega n equals 2, where bigOmega counts all prime factors with multiplicity. The local setting keeps statements minimal to support later Dirichlet algebra and inversion once interfaces stabilize. The isSemiprime definition supplies the direct predicate used here.
proof idea
This is a one-line wrapper that applies native_decide to the equality isSemiprime 15 = true, which computes bigOmega 15 and confirms it equals 2.
why it matters
The declaration supplies a verified instance for semiprime numbers inside the arithmetic functions module, supporting Möbius footholds and prime-related calculations in the Recognition framework. It aligns with the lightweight style of the module and provides a concrete check that can feed into broader number-theoretic constructions. No downstream uses are recorded yet, so it functions as foundational scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.