chen_prime_thirtyseven
plain-language theorem explainer
37 is prime while 39 has exactly two prime factors with multiplicity, confirming it as a Chen prime under the Recognition Science definition. Number theorists checking small prime-pair instances in the arithmetic-functions module would cite this for explicit verification. The proof reduces to a single native_decide tactic that evaluates the primality predicate and the big-Omega count by direct computation.
Claim. 37 is prime and 39 is semiprime, i.e., the total number of prime factors of 39 counted with multiplicity equals 2.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the local alias for the standard primality predicate on natural numbers. isSemiprime holds precisely when bigOmega n equals 2, where bigOmega counts prime factors with multiplicity; the supplied definition states that 4 equals 2 squared is semiprime under this measure.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the conjunction of the primality statement for 37 and the equality isSemiprime 39 = true.
why it matters
This supplies an explicit small-case verification of a Chen prime inside the arithmetic-functions section. No parent theorems or downstream uses are recorded, so the declaration functions as an isolated computational check rather than a lemma feeding a larger chain. It touches the number-theory component of the Recognition Science framework without engaging the Möbius inversion machinery or the forcing chain steps T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.