semiprime_thirtythree
plain-language theorem explainer
The declaration confirms that 33 factors into exactly two prime factors and therefore satisfies the semiprime predicate. Researchers maintaining arithmetic-function interfaces inside the Recognition Science number-theory layer would cite this as a base-case verification. The proof reduces to a single native_decide call that evaluates bigOmega 33 directly.
Claim. $Ω(33)=2$, where $Ω(n)$ counts the total number of 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 n holds exactly when bigOmega n equals 2; bigOmega itself is the total prime-factor count with multiplicity, taken from the upstream definition in the same file. This theorem belongs to the collection of small explicit checks that stabilize the arithmetic-function layer before Dirichlet inversion or further prime-related constructions are added.
proof idea
The proof is a one-line term that applies native_decide to the boolean expression isSemiprime 33. The tactic computes bigOmega 33 from its definition and confirms the equality to 2.
why it matters
It supplies a verified concrete instance of the semiprime condition inside the NumberTheory.Primes.ArithmeticFunctions module. Although the used-by count is zero, such base cases are required to keep the arithmetic-function interfaces stable before inversion formulas or links to the Recognition Composition Law can be layered on top. The declaration therefore closes a small verification gap in the prime-arithmetic scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.