Archimedean Property

The Archimedean property: the natural number embedding into TauReal is unbounded and injective. For any n < m, fromNat(m) is not equivalent to fromNat(n).

Archimedean Property

Summary

The Archimedean property: the natural number embedding into TauReal is unbounded and injective. For any n < m, fromNat(m) is not equivalent to fromNat(n).

Statement

%
\label{thm:archimedean-property}
For every $x \in \mathbb{R}_\tau$,
there exists $n \in \mathbb{N}_\tau$ such that $n > x$.

Proof / Justification

[Proof sketch]
Let $x = [q_k]$ with modulus $M$.
Choose $K := M(1)$, so $|q_k - q_K| < 1$ for $k \geq K$.
Write $q_K = a/b \in \mathbb{Q}_\tau$ with $b > 0$.
Then $q_k < |a| + 2$ for all $k \geq K$.
Setting $n := |a| + 2 \in \mathbb{N}_\tau$
(via $\mathbb{N}_\tau \hookrightarrow \mathbb{R}_\tau$)
gives $n > x$.

Source Context

• Registry source: book-01.jsonl line 188
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part17/ch76-constructive-reals.tex lines 110-115

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Boundary.ConstructiveReals
• Name: Tau.Boundary.taureal_archimedean_embedding

Dependencies

• Canonical: I.D84

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.