IndisputableMonolith.NumberTheory.Primes.Wrappers
The Wrappers module supplies thin wrappers around standard prime lemmas, including the guarantee that a prime exists at least as large as any given natural number. It reuses the Basic primes module to keep all results axiom-free. Each entry is a direct one-line application of an upstream lemma.
claimFor every natural number $n$ there exists a prime $p$ with $p$ at least $n$.
background
The module lives in the NumberTheory.Primes namespace and imports Mathlib together with the Basic primes module. The Basic module supplies prime-number footholds for the reality repository by reusing the standard prime predicate from the library. Its design keeps the namespace axiom-free and sorry-free while providing small sanity theorems that confirm correct wiring.
proof idea
This is a wrapper module. Each theorem applies a lemma from the Basic module or Mathlib in a single direct step.
why it matters in Recognition Science
The module feeds the Primes namespace aggregator. Downstream code imports the aggregator rather than individual files. It supplies the prime existence result stated in the module documentation as part of the algebraic layer before any analytic extensions.
scope and limits
- Does not introduce new axioms or sorry statements.
- Does not prove results on prime distribution or density.
- Does not address composite factorization beyond the listed wrappers.