semiprime_fiftyone
plain-language theorem explainer
51 factors as the product of the distinct primes 3 and 17, satisfying the semiprime predicate that the total prime-factor count with multiplicity equals two. Number theorists extending the Recognition Science arithmetic layer for Möbius inversion would cite the verification when populating small composite cases. The proof is a one-line native decision procedure that unfolds the bigOmega definition and evaluates the factorization directly.
Claim. $51$ is semiprime, i.e., the arithmetic function counting prime factors with multiplicity satisfies $Ω(51)=2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. A semiprime is defined by the predicate isSemiprime n which holds precisely when bigOmega n equals 2. bigOmega counts the prime factors with multiplicity, so the theorem confirms that 51 = 3 × 17 meets this count. The local setting keeps statements minimal to support later Dirichlet algebra layers once interfaces stabilize.
proof idea
The proof is a term-mode application of the native_decide tactic. It unfolds the definition isSemiprime n := bigOmega n = 2 and lets the kernel compute the prime factorization of the constant 51 to decide the equality.
why it matters
This small verification populates the arithmetic functions layer that underpins Möbius function applications in the Recognition Science number theory component. It supports the broader prime factorization machinery without introducing new hypotheses. No downstream theorems currently depend on it, leaving it as a foundational check for semiprime cases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.