semiprime_eightyfive
plain-language theorem explainer
The declaration establishes that 85 factors as 5 times 17 and therefore satisfies the semiprime condition with exactly two prime factors counted with multiplicity. Number theorists building arithmetic tools for Recognition Science would cite this concrete case because the prime 17 carries RS relevance. The proof reduces to a single native_decide call that evaluates the bigOmega predicate directly on the integer.
Claim. $85$ is semiprime, i.e., the total number of prime factors counted with multiplicity satisfies $85 = 5^1 17^1$ so that the count equals 2.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function and related predicates. The central definition is isSemiprime, which returns true precisely when bigOmega n equals 2; bigOmega itself counts every prime factor of n with multiplicity. The local setting keeps statements minimal so that Dirichlet inversion and deeper algebra can be added later once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the Boolean equality isSemiprime 85 = true by direct computation of bigOmega 85.
why it matters
This instance supplies a verified semiprime datum (85 = 5 × 17) that can feed later prime-counting arguments in the Recognition Science number-theory layer. The module doc-comment flags 17 as RS-relevant, placing the result among the arithmetic footholds needed for Möbius inversion and square-free checks. No downstream uses are recorded, so the declaration functions as a concrete building block rather than a parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.