Constructive Reals

R_tau: Cauchy completion of Q_tau with explicit modulus of convergence. Constructive reals aligned with computable/effectively presented analysis.

Constructive Reals

Summary

R_tau: Cauchy completion of Q_tau with explicit modulus of convergence. Constructive reals aligned with computable/effectively presented analysis.

Statement

%
\label{def:constructive-reals}
The \textbf{$\tau$-real numbers} are defined as:
\[
    \mathbb{R}_\tau := \{\text{Cauchy sequences in } \mathbb{Q}_\tau
    \text{ with explicit modulus of convergence}\} \,/\, \sim,
\]
where two Cauchy sequences $(q_n)$ and $(r_n)$ are equivalent
if $|q_n - r_n| \to 0$ as $n \to \infty$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 86
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part10/ch42-number-tower.tex lines 269-279

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Boundary.NumberTower
• Name: Tau.Boundary.TauReal

Dependencies

• Canonical: I.D35

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.