not_prime_zero
plain-language theorem explainer
Zero is not prime under the standard definition on the natural numbers. Workers in the Recognition monolith invoke the result when boundary cases arise in prime-indexed sums. The proof is a one-line wrapper that applies the decide tactic to the decidable negated primality predicate.
Claim. $0$ is not a prime number, i.e., $¬Prime(0)$, where $Prime(n)$ is the standard predicate asserting that the natural number $n$ is prime.
background
The module supplies elementary prime results to anchor the Recognition Science development. It reuses Mathlib's definition of primality without axioms or sorries, keeping the namespace stable for later analytic extensions. The local alias Prime is the transparent wrapper for the standard primality predicate on natural numbers. This theorem functions as a basic sanity check confirming correct wiring with the surrounding library.
proof idea
The proof is a direct one-line wrapper that invokes the decide tactic. The tactic resolves the negated primality statement for zero by decidable computation.
why it matters
The result is invoked inside the proof of twistedPrimeCostSum_zero, which establishes that the twisted prime cost sum vanishes at the zero argument. It supports the algebraic layer before growth into analytic number theory, matching the module's design goal of axiom-free footholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.