semiprime_fiftyeight
plain-language theorem explainer
The declaration verifies that 58 factors as the product of two distinct primes and therefore satisfies the semiprime predicate given by total prime-factor count equal to two. Number theorists building small-case tables inside Recognition Science arithmetic wrappers would cite it when populating explicit semiprime instances. The proof reduces to a single native_decide tactic that evaluates the underlying arithmetic definition directly.
Claim. The integer 58 satisfies $58 = 2 × 29$ and therefore obeys the semiprime condition $Ω(58) = 2$, where $Ω(n)$ counts all prime factors of $n$ with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The predicate isSemiprime is introduced via the definition isSemiprime n := bigOmega n = 2, where bigOmega implements the total prime-factor function Ω. Upstream results include the isSemiprime definition itself together with several foundational “is” structures that guarantee algebraic or collision-free properties, although none are invoked in the present statement.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the boolean equality isSemiprime 58 = true. This tactic evaluates the definition bigOmega 58 = 2 inside the kernel without further lemmas.
why it matters
The declaration supplies a concrete, machine-checked instance of the semiprime predicate inside the arithmetic-functions module. It supports the module’s goal of providing Möbius footholds for later Dirichlet inversion, though it currently feeds no downstream theorems. The fact aligns with Recognition Science’s practice of explicit small-integer verifications that can later interface with the phi-ladder and prime distributions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.