semiprime_sixtyfive
plain-language theorem explainer
65 equals 5 times 13 and therefore has exactly two prime factors counted with multiplicity. Number theorists building arithmetic-function tools inside Recognition Science would cite the fact as a verified base case. The proof reduces to a direct computational check on the definition of semiprimality.
Claim. The integer 65 satisfies $65=5×13$, hence $Ω(65)=2$ where $Ω$ counts prime factors with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. isSemiprime is defined by the equation bigOmega n = 2. bigOmega itself returns the total number of prime factors of n counted with multiplicity. The local setting keeps statements minimal so that Dirichlet inversion can be added once the basic interfaces stabilize.
proof idea
One-line wrapper that applies native_decide to evaluate isSemiprime 65 directly from its definition via bigOmega.
why it matters
The declaration supplies a concrete, machine-checked semiprime instance inside the arithmetic-functions module. It supports later Möbius-based arguments and squarefree checks that appear in Recognition Science constructions. No parent theorem or downstream use is recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.