Constructive Reals

TauReal: constructive reals via Cauchy completion of TauRat. Represented as sequences of TauRat approximations with pointwise equivalence. Every TauReal is explicitly specified by a constructive sequence.

Constructive Reals

Summary

TauReal: constructive reals via Cauchy completion of TauRat. Represented as sequences of TauRat approximations with pointwise equivalence. Every TauReal is explicitly specified by a constructive sequence.

Statement

%
\label{def:tau-real-field}
The \textbf{TauReal field structure} on $\mathbb{R}_\tau$ consists of:
\begin{itemize}
    \item Addition and multiplication (term-by-term on representatives).
    \item Additive identity $0_{\mathbb{R}} := [\underline{0}, \underline{0}, \ldots]$,
          multiplicative identity $1_{\mathbb{R}} := [\underline{1}, \underline{1}, \ldots]$.
    \item Additive inverse: $-[q_n] := [-q_n]$.
    \item Multiplicative inverse: for $[q_n] \neq 0$,
          choose $N$ with $|q_n| > \varepsilon > 0$ for $n \geq N$,
          then $[q_n]^{-1} := [q_n^{-1}]_{n \geq N}$.
    \item Order: $[q_n] < [r_n]$ if there exist
          $\varepsilon > 0$ and $N$ with $r_n - q_n > \varepsilon$ for all $n \geq N$.
\end{itemize}

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

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

Lean / Formalization Notes

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

Dependencies

• Canonical: I.D15, I.D14

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.