prime_iff
plain-language theorem explainer
The theorem asserts that the repository's local primality predicate on natural numbers coincides exactly with the standard library definition. Number theorists extending arithmetic functions within the Recognition Science monolith cite it to convert between custom and library predicates on primes. The proof reduces to a single reflexivity step on logical equivalence because the local abbreviation is transparent and identical to the library predicate.
Claim. For every natural number $n$, the local primality predicate holds if and only if the standard primality predicate from the mathematical library holds.
background
The module supplies basic prime-number results for the Recognition Science repository. It reuses the mathematical library's primality predicate on natural numbers without axioms or sorrys, keeping the namespace stable for later analytic extensions. The local abbreviation defines primality directly as the library predicate, rendering the two interchangeable by definition. Upstream, the set of primes is introduced as the collection of natural numbers satisfying the standard primality condition, providing the set-theoretic foundation for subsequent arithmetic functions.
proof idea
The proof is a term-mode application of reflexivity on the if-and-only-if relation. Because the local abbreviation is transparent, the two predicates are definitionally equal, so the equivalence follows immediately without tactics or lemmas.
why it matters
This equivalence anchors the algebraic layer of the primes module and is invoked in thirty-six downstream results, including evaluations of the total prime factors function to one on primes, the Liouville function to negative one, and coprimality statements for prime powers. It supports the module's design goal of axiom-free compatibility with standard number theory before analytic extensions, ensuring all later arithmetic functions remain consistent with library results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.