semiprime_seventyfour
plain-language theorem explainer
74 factors as 2 times 37 and therefore satisfies the semiprime condition that the total number of prime factors counted with multiplicity equals exactly two. Number theorists working inside Recognition Science cite this concrete check when validating small integers against the arithmetic-function primitives. The proof is a one-line native decision procedure that evaluates the bigOmega definition directly.
Claim. $74$ is semiprime, i.e., the total number of prime factors of $74$ counted with multiplicity equals $2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related predicates. isSemiprime is defined by the equation bigOmega n = 2, where bigOmega counts prime factors with multiplicity. The local setting keeps statements minimal so that Dirichlet inversion and deeper algebra can be added once the basic interfaces stabilize. Upstream results include the isSemiprime definition itself together with collision-free and algebraic structures imported from foundation modules.
proof idea
one-line wrapper that applies native_decide to evaluate isSemiprime 74 directly from its definition bigOmega 74 = 2.
why it matters
The declaration supplies a verified semiprime instance at 74, flagged as RS-relevant because of the prime factor 37. It populates the arithmetic-functions module that prepares Möbius footholds for later use in the Recognition framework. No downstream theorems are recorded, yet the result aligns with the number-theoretic primitives required by the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.