IndisputableMonolith.NumberTheory.Primes.Wrappers
The Wrappers module supplies thin re-exports of Mathlib prime facts through the Basic layer, centered on the statement that for every natural number n there exists a prime p at least n. Code in the Recognition monolith cites it to obtain basic prime properties without direct Mathlib references. Each entry is a one-line wrapper that forwards the corresponding result from the imported Basic module.
claim$forall n in mathbb{N}, exists p (p geq n land text{Prime}(p))$
background
The module lives in the NumberTheory.Primes namespace and imports only Mathlib plus IndisputableMonolith.NumberTheory.Primes.Basic. The upstream Basic module supplies axiom-free footholds that reuse Nat.Prime while remaining sorry-free, with the explicit goal of confirming correct wiring before any analytic extensions. Its doc-comment states the design: reuse Mathlib, keep the namespace axiom-free and sorry-free, and grow upward into analytic number theory only after the algebraic layer is stable.
proof idea
This is a wrapper module, no original proofs. Each declaration forwards a result from the Basic import via a direct application or re-export.
why it matters in Recognition Science
The module feeds the IndisputableMonolith.NumberTheory.Primes aggregator, which downstream code is instructed to import in preference to individual files. It supplies the prime-unboundedness fact that populates the prime namespace while preserving the axiom-free character required by the monolith.
scope and limits
- Does not introduce new axioms or hypotheses.
- Does not contain any sorry statements.
- Does not reinvent Mathlib's Nat.Prime definition.
- Does not extend into analytic number theory.
- Does not depend on Recognition-specific constants or the J-cost function.