semiprime_four
plain-language theorem explainer
The declaration verifies that 4 satisfies the semiprime condition under the arithmetic definition where the total prime factor count with multiplicity equals exactly two. Number theorists building base cases for prime-related predicates in the Recognition Science number theory layer would reference this instance. The proof reduces to a direct native decision procedure on the boolean equality.
Claim. $4$ is semiprime, i.e., its total number of prime factors counted with multiplicity equals two.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function as a foothold for Dirichlet inversion. The isSemiprime predicate is defined by the equality bigOmega n = 2, where bigOmega tallies all prime factors with multiplicity. This theorem provides a concrete evaluation of that predicate at n=4 within the local setting of small arithmetic checks.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the boolean equality directly for the constant input 4.
why it matters
This supplies a verified base case for the semiprime definition in the ArithmeticFunctions module, which prepares Möbius-based tools for later use in prime factorization arguments. It closes a specific instance without new hypotheses and aligns with the module's role in supporting Recognition Science number theory scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.