semiprime_twentyfive
plain-language theorem explainer
25 satisfies the semiprime condition that the total number of prime factors counted with multiplicity equals 2. Number theorists working with arithmetic functions inside the Recognition Science setup would cite this as a verified concrete instance. The proof reduces directly to a native decision procedure on the bigOmega evaluation.
Claim. $25$ is semiprime, i.e., the total number of prime factors of $25$ counted with multiplicity equals $2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related maps such as bigOmega. A number $n$ is semiprime precisely when bigOmega $n$ equals $2$, per the definition that sets isSemiprime $n$ to true exactly on that equality. The local setting keeps statements minimal so that Dirichlet inversion and related algebra can be added once the basic interfaces stabilize.
proof idea
One-line wrapper that applies native_decide to evaluate the semiprime predicate on $25$ directly from the bigOmega definition.
why it matters
The declaration supplies a concrete base case for semiprime verification inside the arithmetic-functions module. It supports number-theoretic tooling that may later feed prime-related arguments in the Recognition framework, though no downstream results are recorded and the statement does not engage the forcing chain, the Recognition Composition Law, or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.