semiprime_thirtynine
plain-language theorem explainer
The declaration confirms that 39 factors as 3 times 13 and therefore satisfies the semiprime condition given by total prime factor count equaling two. Number theorists using the Recognition Science arithmetic functions module would cite this as a verified concrete case. The proof reduces to a single native_decide tactic that evaluates the predicate by direct computation.
Claim. The natural number 39 is semiprime, that is, its total number of prime factors counted with multiplicity equals two: $Ω(39)=2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The predicate isSemiprime is defined by the equation bigOmega n = 2, where bigOmega counts prime factors with multiplicity. This supplies a concrete instance for n=39=3×13. Upstream results include the isSemiprime definition together with several 'is' structures from foundation modules that encode collision-free or algebraic tautology properties.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate isSemiprime 39 by direct computation.
why it matters
This supplies a basic verified instance inside the arithmetic functions section. It supports explicit checks on prime factorizations that feed into larger number-theoretic constructions, consistent with the framework's use of Ω counts in the phi-ladder and eight-tick octave steps. No direct downstream uses are recorded, leaving it as a leaf verification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.