isSemiprime
plain-language theorem explainer
isSemiprime is a definition that returns true for a natural number n precisely when the total number of its prime factors with multiplicity equals two. Number theorists examining Chen primes would cite this predicate when verifying examples such as 9 = 3² or 21 = 3×7. The definition consists of a single equality check against the bigOmega function.
Claim. Let $n$ be a natural number. Then $n$ is semiprime when $Ω(n) = 2$, where $Ω$ counts the prime factors of $n$ with multiplicity.
background
The ArithmeticFunctions module provides small wrappers around Mathlib's arithmetic function library, with an emphasis on the Möbius function as a starting point for Dirichlet algebra. The upstream bigOmega abbreviation, defined as ArithmeticFunction.cardFactors, supplies the Ω(n) count used here. This setup maintains lightweight interfaces so that deeper inversion formulas can be added once the basic predicates stabilize.
proof idea
The definition is a one-line wrapper that applies bigOmega to the input and tests for equality with 2.
why it matters
This predicate is invoked by multiple Chen prime theorems in the same file, including chen_prime_seven which states that 7 is prime and 9 is semiprime, and similarly for 19, 31, and others. It supplies the semiprime check required for twin-prime-like statements where p + 2 is semiprime. Within the Recognition Science framework the definition supports number-theoretic scaffolding but does not directly engage the J-uniqueness or eight-tick octave steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.