semiprime_fortynine
plain-language theorem explainer
49 equals 7 squared and therefore satisfies Ω(49) = 2. Number theorists checking concrete instances of arithmetic predicates would cite this verification. The proof is a direct native_decide evaluation of the Boolean predicate at the fixed input 49.
Claim. $49$ is semiprime, i.e., the total number of prime factors of $49$ counted with multiplicity satisfies $Ω(49) = 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. A natural number n is declared semiprime precisely when its total prime-factor count with multiplicity, denoted Ω(n) or bigOmega n, equals 2. The local setting is basic number-theoretic footholds before deeper Dirichlet algebra or inversion formulas are introduced.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the constant Boolean expression obtained by unfolding isSemiprime at 49.
why it matters
The declaration supplies a concrete checked instance of the semiprime predicate inside the arithmetic-functions layer. It supports the NumberTheory.Primes module whose Möbius footholds may later feed Recognition Science constructions, though no downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.