pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.NumberTheory.Primes.Basic

show as:
view Lean formalization →

This module supplies a transparent repo-local alias for the standard primality predicate on natural numbers together with elementary facts such as the primality of 2 and 3. Analytic number theorists working inside the Recognition Science framework import it to access basic prime properties without direct Mathlib references in downstream code. The module contains only definitions and aliases; it performs no deductive steps.

claimLet $P(n)$ denote the predicate that the natural number $n$ is prime, realized as a transparent alias to the standard definition in the naturals.

background

The module resides in the NumberTheory.Primes namespace and imports only Mathlib. It introduces the Prime predicate as a transparent alias and lists basic facts such as prime_two and prime_three. This elementary layer precedes the arithmetic functions and factorization interfaces defined in sibling modules.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the Prime predicate to the Primes aggregator and to the ports for BrunTitchmarsh, PNT, and RiemannHypothesis. It supplies the required basic interface for the number theory components of the Recognition Science framework.

scope and limits

used by (11)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (6)