semiprime_nine
plain-language theorem explainer
The declaration verifies that 9 satisfies the semiprime predicate under the total prime factor count. Number theorists building the arithmetic functions layer in Recognition Science would reference it for base-case checks. The proof reduces the equality to a direct computational evaluation.
Claim. The integer 9 satisfies $Ω(9) = 2$, where $Ω(n)$ counts the prime factors of $n$ with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. A number $n$ is semiprime precisely when its total prime factor count equals 2, implemented via the predicate that sets isSemiprime $n$ to the boolean equality bigOmega $n = 2$. This theorem checks the concrete case $n = 9 = 3^2$. Upstream results supply the semiprime definition together with auxiliary structures for collision-free properties and simplicial edge lengths, though the direct dependency is the arithmetic predicate itself.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the decidable proposition directly from the definition of bigOmega.
why it matters
The result populates the arithmetic functions library with an explicit small-case verification that supports the Möbius footholds described in the module. It supplies a concrete instance of the semiprime predicate without introducing hypotheses, consistent with the framework's pattern of discharging basic number-theoretic checks before layering Dirichlet algebra or inversion formulas. No downstream theorems are recorded as users of this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.