Prime
plain-language theorem explainer
Prime aliases the standard primality predicate on natural numbers from Mathlib. Researchers building Gap-45 barrier certificates and Euler-Mascheroni bounds cite it to keep the number-theory layer axiom-free. The implementation is a transparent one-line redefinition that re-exports Nat.Prime without new content.
Claim. For a natural number $n$, the predicate Prime$(n)$ holds precisely when $n$ is prime in the usual arithmetic sense.
background
The module supplies basic prime-number footholds for the reality repo. Its design reuses Mathlib’s Nat.Prime to remain axiom-free and sorry-free, supplying only small sanity theorems that confirm the algebraic layer is wired correctly before any growth into analytic number theory. This local setting keeps the namespace lightweight so that downstream modules can import primality without importing new hypotheses.
proof idea
The declaration is a transparent abbrev that directly equates Prime n to Nat.Prime n; no tactics or lemmas are applied.
why it matters
It is referenced by BarrierCert (requiring beat_prime : Nat.Prime 37), gapDiff_prime, shimmer_cert, and gamma_numerical_bounds (which records the open C-011 status that the RS derivation of γ remains unresolved). The alias therefore anchors the prime requirements that appear in Gap-45 arithmetic and the eight-tick constructions of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.