ch:real-numbers: cuts and Cauchy completion

For $q : Q$ , the predicates $L_{q} (r) \equiv r < q$ and $U_{q} (r) \equiv q < r$ are inhabited at $q - 1$ and $q + 1$ . Density of the rational order proves both roundedness implications; transitivity proves their converses. They are disjoint by irreflexivity. If $a < b$ , decidability of rational order gives either $a < q$ , hence $L_{q} (a)$ , or $q \leq a < b$ , hence $U_{q} (b)$ . Thus they form a cut.

Moreover, $(L_{q}, U_{q}) < (L_{r}, U_{r}) ⟺ \exists s : Q . q < s < r ⟺ q < r .$ The middle equivalence is the definition of cut order, and the last is rational density. Hence the rational-cut map preserves and reflects strict order. If its values at $q$ and $r$ are equal, neither $q < r$ nor $r < q$ can hold by order reflection; rational trichotomy gives $q = r$ . Thus the map is injective.

Put $L_{- x} (q) : = U_{x} (- q)$ and $U_{- x} (q) : = L_{x} (- q)$ . Inhabitedness and disjointness are inherited after negating the rational witnesses. For lower roundedness, from $U_{x} (- q)$ choose $t < - q$ with $U_{x} (t)$ and take $- t > q$ ; the other roundedness law is dual. If $q < r$ , then $- r < - q$ , so locatedness of $x$ gives $L_{x} (- r)$ or $U_{x} (- q)$ , namely $U_{- x} (r)$ or $L_{- x} (q)$ . This is the one place where locatedness is used to show that negation is a cut.

For the inverse law, a witness to $L_{x + (- x)} (q)$ consists of $r < x < - s$ with $q = r + s$ , and hence $q < 0$ . Conversely, if $q < 0$ , choose a rational bracket $r < x < t$ with $t - r < - q$ . Then $x < r - q$ and the witnesses $r$ and $q - r$ sum to $q$ , so $L_{x + (- x)} (q)$ . Dually, a witness to the upper cut forces $0 < q$ ; if $0 < q$ , choose $t < x < r$ with $r - t < q$ and use $r$ and $q - r$ . Thus the lower and upper predicates of $x + (- x)$ are exactly $q < 0$ and $0 < q$ , and cut extensionality gives $x + (- x) = 0$ .

Let the antitone modulus satisfy $m, n \geq M (η) ⟹ | s_{m} - s_{n} | < η .$ For $δ, ϵ > 0$ , suppose without loss of generality that $δ \leq ϵ$ . Antitonicity gives $M (δ / 2) \geq M (ϵ / 2)$ , so both selected indices are at least $M (ϵ / 2)$ . Hence $| s_{M (δ / 2)} - s_{M (ϵ / 2)} | < ϵ / 2 < δ + ϵ .$ The rational-point closeness rule turns this inequality into $rat (s_{M (δ / 2)}) \sim_{δ + ϵ} rat (s_{M (ϵ / 2)}),$ so the displayed map is a Cauchy approximation. Applying $\lim$ produces the required Cauchy real.

Suppose $p : rat (q) = rat (r)$ . Transporting reflexive closeness along $p$ gives $rat (q) \sim_{ϵ} rat (r)$ for every $ϵ : Q^{+}$ . By the assumed rational characterization, $| q - r | < ϵ$ for every positive $ϵ$ . If $q \neq r$ , then $d : = | q - r |$ is positive; taking $ϵ = d / 2$ gives $d < d / 2$ , a contradiction. Therefore $q = r$ , so $rat : Q \to R_{c}$ is injective.

Fix $ϵ, θ : Q^{+}$ . If $L_{x_{ϵ}} (a)$ , put $q = a - ϵ - θ$ ; then $L_{x_{ϵ}} (q + ϵ + θ)$ witnesses $L_{y} (q)$ . If $U_{x_{ϵ}} (b)$ , put $r = b + ϵ + θ$ ; then $U_{x_{ϵ}} (r - ϵ - θ)$ witnesses $U_{y} (r)$ . Hence both halves are inhabited.

Suppose $L_{y} (q)$ is witnessed by $ϵ, θ$ and $L_{x_{ϵ}} (q + ϵ + θ)$ . Set $q^{'} = q + θ / 2$ and $θ^{'} = θ / 2$ . Then $q < q^{'}$ and $q^{'} + ϵ + θ^{'} = q + ϵ + θ,$ so the same cut witness proves $L_{y} (q^{'})$ . Downward closure gives the converse roundedness implication. For $U_{y} (q)$ use $q^{'} = q - θ / 2$ and $θ^{'} = θ / 2$ ; then $q^{'} < q$ and the defining upper endpoint is unchanged. Upward closure gives the converse implication.

Finally, let $L_{y} (q)$ be witnessed by $ϵ, θ$ and let $U_{y} (q)$ be witnessed by $δ, η$ . Their defining inequalities are $q + ϵ + θ < x_{ϵ}, x_{δ} < q - δ - η .$ Consequently $x_{ϵ} - x_{δ} > δ + η + ϵ + θ > δ + ϵ,$ which contradicts $| x_{δ} - x_{ϵ} | < δ + ϵ$ . Thus the two halves are disjoint.