not_prime_zero
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 in Recognition Science
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.
scope and limits
- Does not establish primality for any positive integer.
- Does not connect to the J-cost function or phi-ladder.
- Does not address factorization or composite numbers.
- Does not interact with the forcing chain or spatial dimension results.
Lean usage
simp [twistedPrimeCostSum, not_prime_zero]formal statement (Lean)
27theorem not_prime_zero : ¬ Nat.Prime 0 := by
proof body
Decided by rfl or decide.
28 decide
29