semiprime_ten
plain-language theorem explainer
The declaration verifies that the integer 10 has exactly two prime factors counting multiplicity and therefore meets the semiprime predicate. Number theorists building base cases inside the Recognition Science arithmetic-functions library would reference this fact when initializing Möbius inversion or square-free checks. The proof reduces to a single native_decide call that evaluates the bigOmega definition directly on the constant.
Claim. The integer $10$ satisfies the semiprime condition, i.e., its total number of prime factors counted with multiplicity equals $2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related predicates. The predicate isSemiprime is defined by the equality bigOmega n = 2, where bigOmega counts prime factors with multiplicity. This places the result among the small verified constants that serve as footholds before deeper Dirichlet algebra is layered on.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the definition of isSemiprime on the numeral 10.
why it matters
This verified constant contributes to the collection of base cases in the arithmetic-functions module. It supports downstream constructions that rely on explicit semiprime checks within the Recognition Science framework, consistent with the module's stated goal of providing Möbius footholds. No parent theorems are listed among the used-by edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.