chen_prime_three
plain-language theorem explainer
The declaration delivers the assertion that both 3 and 5 are prime numbers, confirming the Chen prime pair with 3+2=5. Number theorists working on arithmetic functions and Möbius applications in the Recognition Science number theory layer would cite this for small-case verification. The proof goes through by direct computational decision via native_decide on the decidable conjunction.
Claim. $3$ and $5$ are both prime numbers.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the repo-local alias for the standard natural-number primality predicate. Upstream results supply the Prime definition as an alias for Nat.Prime together with structural is statements from foundation modules that frame empirical and combinatorial checks.
proof idea
The proof is a term-mode one-line wrapper that applies native_decide to evaluate the decidable proposition Prime 3 ∧ Prime 5.
why it matters
This supplies a basic prime fact inside the arithmetic functions module that supports later Möbius and prime-counting steps in the Recognition framework. It aligns with the number-theory footholds required for constants such as the alpha band and phi-ladder mass formulas, though no downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.