chen_prime_seven
plain-language theorem explainer
7 is prime and 9 is semiprime, confirming 7 as a Chen prime since 7+2=9 has exactly two prime factors. Number theorists examining small cases of Chen's theorem or prime-pair properties would cite this verified instance. The proof is a one-line term that invokes native_decide to evaluate the conjunction of the primality and semiprimality predicates.
Claim. $7$ is prime and $9$ is semiprime, where semiprime means the total number of prime factors counting multiplicity equals two.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and the total prime-factor counting function bigOmega. Prime is the transparent alias for the standard primality predicate on natural numbers. isSemiprime n returns true precisely when bigOmega n equals 2, so that 9 satisfies the predicate because its factorization is 3 squared.
proof idea
The proof is a one-line term wrapper that applies native_decide to the conjunction Prime 7 ∧ isSemiprime 9 = true, letting the kernel compute the concrete truth value of both predicates.
why it matters
The declaration supplies a concrete Chen-prime example inside the arithmetic-functions layer that supports number-theoretic statements in the Recognition Science framework. It illustrates the use of semiprime checks that appear in prime-pair constructions, though no downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.