chen_prime_fortyseven
plain-language theorem explainer
47 is prime and 49 is semiprime, confirming the Chen prime condition that p+2 factors into exactly two primes. Number theorists studying bounded prime gaps or explicit constellations reference this case. The proof reduces to a single native_decide call that evaluates both predicates by direct computation.
Claim. The integer 47 is prime and the integer 49 is semiprime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. isSemiprime holds precisely when the total number of prime factors counted with multiplicity equals two. The Prime predicate follows the standard definition from the Basic submodule.
proof idea
The proof is a one-line wrapper that invokes native_decide to compute the conjunction of primality for 47 and the semiprime predicate for 49.
why it matters
This supplies a concrete Chen prime instance inside the arithmetic functions library. It supports explicit data points for constructions that later invoke the phi-ladder lattice or related number-theoretic structures. No downstream parent theorems are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.