Registry · Definition I.D36 tau-effective formalized

I.D36 — Constructive Reals

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

Book I Part 10 Ch. 42

Dependency Graph

Depends on (1)

I.D35

Lean Formalization

Module: TauLib.BookI.Boundary.NumberTower

Symbol: Tau.Boundary.TauReal