semiprime_six
plain-language theorem explainer
The theorem confirms that 6 satisfies the semiprime predicate because its factorization into 2 and 3 produces exactly two prime factors counted with multiplicity. Number theorists building arithmetic-function tools inside the Recognition Science stack would reference this as an explicit base case next to the checks for 4 and 9. The proof is a one-line native_decide invocation that evaluates the bigOmega predicate by direct computation on the constant 6.
Claim. $Ω(6) = 2$, where $Ω(n)$ denotes the total number of prime factors of $n$ counted with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The predicate isSemiprime is defined by the equation bigOmega n = 2, where bigOmega counts prime factors with multiplicity; sibling declarations such as bigOmega_def and bigOmega_apply establish the supporting notation. The local setting is a collection of small, stable interfaces that later layers of Dirichlet algebra and inversion can build upon.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the Boolean expression isSemiprime 6 by direct computation of bigOmega 6.
why it matters
This supplies a concrete base case for the semiprime predicate inside the arithmetic-functions module, supporting later development of Möbius inversion and related number-theoretic tools. It sits among the prime-related constructions that feed Recognition Science number theory, although the declaration currently has no downstream users. The result closes a simple verification step without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.