exists_prime_ge
plain-language theorem explainer
Every natural number n is succeeded by at least one prime p satisfying n ≤ p. Recognition Science developers and number theorists cite this wrapper when they need a stable local name for prime existence in sequence constructions. The proof is a one-line term wrapper that invokes Mathlib's Nat.exists_infinite_primes and rewrites through the local Prime alias.
Claim. For every natural number $n$, there exists a prime number $p$ such that $n ≤ p$.
background
The module supplies stable wrappers around Mathlib prime theorems to insulate downstream code from API changes. Prime is defined locally as the transparent alias abbrev Prime (n : ℕ) : Prop := Nat.Prime n. The declaration sits among sibling results such as Euclid's lemma and coprimality conditions for primes.
proof idea
The proof is a one-line wrapper that applies Nat.exists_infinite_primes n and uses simpa to rewrite the local Prime definition into the Mathlib predicate.
why it matters
This result anchors the prime existence fact in the local namespace of the NumberTheory.Primes hierarchy. It supports downstream prime toolkit usage even though no direct callers are recorded yet. In the Recognition Science setting it supplies a basic number-theoretic fact consistent with the overall derivation from the unified forcing chain and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.