Internal Primes

p is prime iff p >= 2 and only divisors are 1 and p. P_tau is the set of internal primes; infinite (Euclid’s argument earned internally).

Internal Primes

Summary

p is prime iff p >= 2 and only divisors are 1 and p. P_tau is the set of internal primes; infinite (Euclid’s argument earned internally).

Statement

%
\label{def:internal-primes}
An element $\underline{p} \in \tau\text{-Idx}$ is
\textbf{prime} (or \textbf{irreducible}) if:
\begin{enumerate}
    \item $\underline{p} \geq \underline{2}$, and
    \item the only divisors of $\underline{p}$ are
          $\underline{1}$ and $\underline{p}$ itself.
\end{enumerate}
We write $\mathbb{P}_\tau$ for the set of internal primes.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 52
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part04/ch16-primes-divisibility.tex lines 100-111

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Coordinates.Primes
• Name: Tau.Coordinates.idx_prime

Dependencies

• Canonical: I.D19a

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.