## Definition ## A computable real number is an element of an [[Archimedean ordered field]] $F$ with either * A [[Cauchy sequence]] of [[rational numbers]] $s:\mathbb{N} \to \mathbb{Q}$ with a [[modulus of Cauchy convergence]] $M:\mathbb{Q}_{+} \to \mathbb{N}$ * A $Q$-indexed [[locator]] $$\epsilon(c):\prod_{a:\mathbb{Q}} \prod_{b:\mathbb{Q}} (a,b) \to ((a,c) + (c,b))$$ ## See also ## * [[real numbesr]] * [[locator]] * [[Cauchy sequence]] * [[modulus of Cauchy convergence]] * [[Cauchy approximation]]