semiprime_thirtyfour
plain-language theorem explainer
34 factors as 2 times 17 and therefore satisfies the semiprime condition that the total number of prime factors counted with multiplicity equals 2. Researchers building tables of arithmetic functions for the Recognition Science number-theory layer would cite this when populating small verified cases ahead of Möbius inversion. The proof reduces to a single native_decide call that evaluates the bigOmega definition directly.
Claim. $34$ is semiprime: its total number of prime factors counted with multiplicity equals two, i.e., $Ω(34)=2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. A number n is semiprime precisely when Ω(n)=2, implemented by the definition isSemiprime n := bigOmega n = 2. This supplies the Boolean predicate used throughout the file for small-case verification before deeper Dirichlet algebra is added.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the Boolean expression isSemiprime 34 directly from the bigOmega definition.
why it matters
The declaration populates the set of verified semiprimes inside the ArithmeticFunctions module, supporting the Möbius footholds described in the module documentation. It contributes concrete data points for later inversion steps without introducing new hypotheses. No downstream uses are recorded, so its role remains that of a building block for prime-related arithmetic constructions in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.