semiprime_sixtytwo
plain-language theorem explainer
The theorem records that 62 factors as 2 times 31 and therefore satisfies the semiprime condition Omega(n) equals 2. Number theorists maintaining tables of small composites or checking arithmetic-function implementations would cite the result. The proof reduces to a direct Boolean evaluation via the native_decide tactic.
Claim. $62$ is semiprime, i.e., $Omega(62)=2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. A central definition states that a number is semiprime precisely when bigOmega n equals 2. This places the declaration inside the NumberTheory.Primes.ArithmeticFunctions section, where explicit small-case checks support later Dirichlet inversion work.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate isSemiprime 62 directly from its definition as bigOmega n = 2.
why it matters
This explicit check belongs to the arithmetic-functions scaffolding that precedes deeper Möbius inversion. It does not feed any downstream theorem in the supplied graph and does not touch the Recognition Science forcing chain, phi-ladder, or constants such as alpha inverse. Its role is limited to verifying concrete instances of the semiprime predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.