Chapter 212OptionalScaffold

Choice-Free HII Cauchy Completion

Prerequisites. Direct starred prerequisites: Chapter 199. No later core chapter depends on this route.

Remark 212.1 ¶

Draft status. This chapter is a scaffold.

Opening obstruction

Completing a quotient of Cauchy sequences appears to require choosing representatives from countably many equivalence classes.

Development contract

Define completion and closeness simultaneously by the selected HII/QIIT, prove its eliminator, metric laws, completeness and rational embedding, and replay the pinned formalization without importing the whole QIIT schema into the core real-number chapter.

Choice-free HII Cauchy completion

The Cauchy construction must complete and quotient at once: completing the quotient of Cauchy sequences requires lifting sequences of equivalence classes, i.e. countable choice. A higher inductive-inductive definition avoids this appeal to countable choice by introducing the limit and equality constructors simultaneously with a closeness relation.

Definition 74.68 — Cauchy reals ¶

Generate $R_{c}$ together with relations $u \sim_{ϵ} v$ , indexed by $ϵ : Q^{+}$ . A family $x : Q^{+} \to R_{c}$ is a Cauchy approximation when $x_{δ} \sim_{δ + ϵ} x_{ϵ}$ for all positive $δ, ϵ$ . The constructor $\lim$ takes such a family:

Γ ⊢ q : Q

Γ ⊢ rat (q) : R_{c}

Rc-Rat

Γ ⊢ x : Q^{+} \to R_{c}

Γ ⊢ p : \prod_{δ : Q^{+}} \prod_{ϵ : Q^{+}} x_{δ} \sim_{δ + ϵ} x_{ϵ}

Γ ⊢ \lim (x, p) : R_{c}

Rc-Lim

Γ ⊢ p : \prod_{ϵ : Q^{+}} u \sim_{ϵ} v

Γ ⊢ eq (u, v, p) : u =_{R_{c}} v

Rc-Eq

In the closeness rules, every difference occurring in a subscript is required to be positive (following convention 26.14).

Γ ⊢ w : - ϵ < q - r < ϵ

Γ ⊢ {cl}_{rr} (w) : rat (q) \sim_{ϵ} rat (r)

Cl-RR

Γ ⊢ w : rat (q) \sim_{ϵ - δ} y_{δ}

Γ ⊢ {cl}_{rl} (w) : rat (q) \sim_{ϵ} \lim (y)

Cl-RL

Γ ⊢ w : x_{δ} \sim_{ϵ - δ} rat (r)

Γ ⊢ {cl}_{lr} (w) : \lim (x) \sim_{ϵ} rat (r)

Cl-LR

Γ ⊢ w : x_{δ} \sim_{ϵ - δ - η} y_{η}

Γ ⊢ {cl}_{ll} (w) : \lim (x) \sim_{ϵ} \lim (y)

Cl-LL

Γ ⊢ ξ : u \sim_{ϵ} v

Γ ⊢ ζ : u \sim_{ϵ} v

Γ ⊢ {cl}_{tr} (ξ, ζ) : ξ = ζ

Cl-Prop

We abbreviate $\lim (x, p)$ as $\lim (x)$ . Simultaneous induction uses a motive $P (u)$ for $u : R_{c}$ and a relational motive $S_{ϵ} (u, v, p)$ over $p : u \sim_{ϵ} v$ . It asks for a $P$ -case for $rat$ and $\lim$ , an $S$ -case for each of ${cl}_{rr}, {cl}_{rl}, {cl}_{lr}, {cl}_{ll}$ , and compatibility with $eq$ and ${cl}_{tr}$ . Taking $S$ constantly $1$ yields the following induction principle.

Referenced from 2 locations

Choice-Free HII Cauchy Completion

Lemma 74.69 — Induction for mere properties ¶

Let $P : R_{c} \to Prop$ . If $P (rat (q))$ holds for all $q : Q$ , and $P (\lim (x))$ holds whenever $P (x_{ϵ})$ holds for all $ϵ$ , then $\prod_{u : R_{c}} P (u)$ .

Referenced from 2 locations

Choice-Free HII Cauchy Completion

Proof of Lemma 74.69 — Induction for mere properties

Proof. Instantiate the simultaneous induction principle with the constant relational motive $1$ . For each of ${cl}_{rr}, {cl}_{rl}, {cl}_{lr}, {cl}_{ll}$ choose $⋆ : 1$ as the relational clause; the ${cl}_{tr}$ clause is ${refl}_{⋆}$ . The constructor $eq$ asks that its two endpoint $P$ -proofs agree, which holds because every $P (u)$ is a proposition. The assumed rational and limit clauses supply the two remaining point cases. ◻

Theorem 74.70 ¶

Let $A$ be a separated premetric space and let $C A$ be Gilbert’s higher inductive–inductive completion. Then:

$C A$ is a separated premetric space, the unit $η_{A} : A \to C A$ is an embedding, and every Cauchy approximation $x$ has limit $\lim (x)$ ;
if $B$ is Cauchy complete, $L : Q^{+}$ , and $f : A \to B$ is $L$ -Lipschitz, there is an $L$ -Lipschitz extension $\bar{f} : C A \to B$ with $\bar{f} (η_{A} (a)) = f (a)$ ; it is the unique continuous map with that unit equation;
the defining limit clause uses the rescaled approximation $\bar{f} (\lim (x)) = lim (ϵ \mapsto \bar{f} (x_{ϵ / L})) .$

For $A = Q$ , Gilbert’s formalization proves that $R_{c} : = C Q$ is a Cauchy-complete archimedean ordered field.

Referenced from 4 locations

Choice-Free HII Cauchy Completion

Proof of Theorem 74.70

Proof. Items (1)–(3) are Theorems 3.16, 3.18–3.20 of [Gil17]; the last displayed equation is the limit clause in the proof of Theorem 3.20, where division by the positive constant $L$ makes $ϵ \mapsto \bar{f} (x_{ϵ / L})$ a Cauchy approximation. The rational specialization and its field operations are the formalized development of [Gil17]. Addition and negation are Lipschitz extensions; multiplication is extended on rationally bounded intervals and the compatible extensions are glued. Thus the field conclusion is imported at the exact signature proved in that source rather than inferred from an unrescaled limit equation. ◻

Remark 212.5 — What extension does not prove ¶

If the rational map into a Cauchy-complete premetric space $F$ is Lipschitz, theorem 74.70 gives its unique continuous extension $R_{c} \to F$ . Field-homomorphism, order-reflection, and injectivity require separate compatibility arguments. We therefore make no initiality claim for arbitrary Cauchy-complete archimedean ordered fields.

Referenced from 2 locations

Choice-Free HII Cauchy Completion

An untruncated locator for $x : R_{d}$ chooses, for each $q < r$ , either $q < x$ or $x < r$ . Repeated trisection with a locator produces nested rational brackets $q_{n} < x < r_{n}$ of width at most $(2 / 3)^{n} (r_{0} - q_{0})$ .

Theorem 74.72 — Agreement ¶

The canonical order-reflecting additive embedding $i : R_{c} \to R_{d}$ fixing $Q$ is an equivalence provided that every $x : R_{d}$ merely has a locator $c : \prod_{q : Q} \prod_{r : Q} (q < r) \to (q < x) + (x < r)$ . In particular, LEM or countable choice ( $\prod_{n : N} ‖ P (n) ‖ \to ‖ \prod_{n : N} P (n) ‖$ for families of sets) implies $R_{c} ≃ R_{d}$ .

Referenced from 3 locations

Proof of Theorem 74.72 — Agreement

Proof. Fix $x$ and, under the outer truncation, choose a locator $c$ and an inhabited-cut bracket $q_{0} < x < r_{0}$ . Given $q_{n} < x < r_{n}$ , put $s_{n} : = (2 q_{n} + r_{n}) / 3, t_{n} : = (q_{n} + 2 r_{n}) / 3.$ If $c (s_{n}, t_{n})$ returns $s_{n} < x$ , take $(q_{n + 1}, r_{n + 1}) = (s_{n}, r_{n})$ ; if it returns $x < t_{n}$ , take $(q_{n + 1}, r_{n + 1}) = (q_{n}, t_{n})$ . Thus the brackets are nested and $q_{n} < x < r_{n}, r_{n} - q_{n} = (2 / 3)^{n} (r_{0} - q_{0}) .$ For their midpoints $a_{n} : = (q_{n} + r_{n}) / 2$ and $m \geq n$ , nesting gives $| a_{m} - a_{n} | < (2 / 3)^{n} (r_{0} - q_{0}) .$ Choose an antitone $N (ϵ)$ with the right side below $ϵ / 2$ . Then $ϵ \mapsto rat (a_{N (ϵ)})$ is a Cauchy approximation and determines $z : R_{c}$ . The embedding $i$ is the nonexpanding extension of the rational-cut map; the formalized characterizations $L_{i (u)} (q) \leftrightarrow rat (q) < u, U_{i (u)} (q) \leftrightarrow u < rat (q)$ show that it preserves these limits and reflects strict order [Gil17].

The Cauchy-limit inequality also places $i (z)$ in every closed bracket $[q_{n}, r_{n}]$ : all later midpoints lie in that bracket, and the error bound tends to zero. It remains to identify the resulting cut. If $q < x$ , roundedness chooses $q^{'}$ with $q < q^{'} < x$ . Choose $n$ with $r_{n} - q_{n} < q^{'} - q$ . Were $q_{n} \leq q$ , we would have $r_{n} < q^{'}$ , contradicting $q^{'} < x < r_{n}$ ; hence $q < q_{n}$ . The bracket bound gives $q_{n} \leq i (z)$ , and roundedness yields $q < i (z)$ . Thus the $q_{n}$ are cofinal in the lower cut. Dually, if $x < r$ , choose $x < r^{'} < r$ and then $n$ with $r_{n} - q_{n} < r - r^{'}$ ; the assumption $r \leq r_{n}$ would imply $r^{'} < q_{n}$ , contradicting $q_{n} < x < r^{'}$ , so $i (z) \leq r_{n} < r$ , and roundedness yields $i (z) < r$ . The $r_{n}$ are coinitial in the upper cut. Cut extensionality therefore gives $i (z) = x$ . Every fiber of the embedding $i$ is a mere proposition, so the merely constructed preimage proves that $i$ is an equivalence.

Under LEM, decide $q < x$ ; its negation gives $x \leq q < r$ , hence $x < r$ . Without LEM, locatedness gives the same sum for each rational pair $q < r$ , and countable choice assembles those choices into a locator. This proves the two stated sufficient conditions. ◻

Without LEM or choice the two real types can differ, and $R_{d}$ is generally the more robust object; theorem 74.67 proves its Cauchy completeness, while no Dedekind-finality or Cauchy-initiality theorem is claimed here. The direct extension is the higher inductive–inductive completion $C A$ of a separated premetric space $A$ : its unit inserts points of $A$ , its limit constructor completes Cauchy approximations, and its closeness family imposes separatedness, exactly as in theorem 74.70.

Exercise 74.19 ¶

★★☆ Show that a Cauchy sequence $s : N \to Q$ equipped with an antitone modulus of convergence $M : Q^{+} \to N$ determines a Cauchy approximation $ϵ \mapsto rat (s_{M (ϵ / 2)})$ , and hence a Cauchy real.

Referenced from 3 locations

Exercise 74.20 ¶

★★☆ Assuming the characterization of $\sim_{ϵ}$ on rational points ( $rat (q) \sim_{ϵ} rat (r)$ iff $- ϵ < q - r < ϵ$ ), prove that $rat : Q \to R_{c}$ is injective.

Referenced from 3 locations