Constructing ℤ, ℚ and ℝ

Lens

MotivationH

Do the numbers exist?

Since school you have calculated with $-3$ , with $\tfrac25$ and with $\sqrt 2$ , using rules such as $(-a)(-b) = ab$ and "every bounded increasing sequence has a limit". In the lessons on integers and real numbers we derived consequences of such rules. But a list of rules can be contradictory, and nothing so far guarantees that some system actually obeys all of them at once. The axioms of a "complete ordered field", for instance, ask a great deal: a field, with an order compatible with $+$ and $\times$ , in which every non-empty bounded set has a least upper bound. Is there such a thing?

This lesson answers yes, by building one. Starting only from the natural numbers $0, 1, 2, \dots$ and the language of sets, we construct $\Z$ , then $\Q$ , then $\R$ — and at the end we prove that the result is essentially unique: any two complete ordered fields are the same field with the elements renamed. Leopold Kronecker is reported to have said that "God made the integers; all else is the work of man". The constructions show how much of that work can be done with the natural numbers alone.

IntuitionH

One idea, used three times

Each construction repairs a defect by adding formal expressions for the missing numbers, and then declaring when two expressions should name the same number.

$\N$ has no solution of $x + 3 = 1$ . So we introduce formal differences " $a - b$ " for pairs $(a, b)$ of naturals — and since $1 - 3$ and $5 - 7$ should be equal, we identify $(a, b)$ with $(c, d)$ when $a + d = c + b$ .
$\Z$ has no solution of $3x = 1$ . So we introduce formal quotients " $a/b$ " with $b \neq 0$ , identifying $(a, b)$ with $(c, d)$ when $ad = cb$ .
$\Q$ has no number whose square is $2$ : the rationals below $\sqrt 2$ have no least upper bound in $\Q$ . So we introduce, for each "gap", the set of rationals below it (a Dedekind cut) — or a sequence of rationals crowding towards it (a Cauchy sequence), identifying sequences that crowd towards the same place.

"Identifying" means passing to equivalence classes (see equivalence relations). The price is that every operation must be checked to be well defined: the answer must not depend on which member of a class we compute with. The Remainder families Wonder Trail, linked below, shows the same phenomenon for remainders.

The two sequences below are made of fractions only. The first iterates $x \mapsto \tfrac12\big(x + \tfrac2x\big)$ from above, the second $q \mapsto \tfrac{2q + 2}{q + 2}$ from below. Both crowd towards the same point — a point that is not a fraction.

Babylonian iteration: fractions from above

Every term is a fraction; the fixed point x = √2 is not.

f(x) = (x + 2/x)/2

Iterates xₖ against k

y = f(x)
y = x
cobweb path

Starting value x₀x₀ = 2Iterationsk = 6

Last iterates: x₄ = 1.41421, x₅ = 1.41421, x₆ = 1.41421

The orbit appears to settle at a fixed point x* ≈ 1.41421.

Fixed points in view (numerical): x* = 1.4142 (attracting: |f′(x*)| < 1)

Based on 3,000 iterations in floating-point arithmetic: numerical evidence, not proof.

Climbing towards √2 from below

Each step stays in the cut {q : q² < 2} and gets closer to its upper edge.

f(x) = (2·x + 2)/(x + 2)

Iterates xₖ against k

y = f(x)
y = x
cobweb path

Starting value x₀x₀ = 1Iterationsk = 12

Last iterates: x₁₀ = 1.41421, x₁₁ = 1.41421, x₁₂ = 1.41421

The orbit appears to settle at a fixed point x* ≈ 1.41421.

Fixed points in view (numerical): x* = 1.4142 (attracting: |f′(x*)| < 1)

Based on 3,000 iterations in floating-point arithmetic: numerical evidence, not proof.

DefinitionsH

Definitions

Definition— well-defined operation on classes

Let $\sim$ be an equivalence relation on a set $X$ with classes $[x]$ . A function $f : X \times X \to X$ induces an operation on classes, $[x] \ast [y] = [f(x, y)]$ , if it is compatible with $\sim$ : whenever $x \sim x'$ and $y \sim y'$ , also $f(x, y) \sim f(x', y')$ . We then say the operation is well defined.

Definition— ordered field

An ordered field is a field $F$ with a total order $\le$ such that $x \le y$ implies $x + z \le y + z$ , and $0 \le x$ , $0 \le y$ imply $0 \le xy$ . An upper bound of $S \subseteq F$ is a $b$ with $s \le b$ for all $s \in S$ ; a least upper bound or supremum is an upper bound below every other upper bound (see order theory). $F$ is complete if every non-empty subset that is bounded above has a supremum in $F$ , and Archimedean if for every $x \in F$ there is a natural number $n$ with $x < n$ .

Definition— Dedekind cut

A Dedekind cut is a subset $A \subseteq \Q$ such that

$A \neq \varnothing$ and $A \neq \Q$ ;
$A$ is closed downwards: if $p \in A$ and $q < p$ , then $q \in A$ ;
$A$ has no greatest element: for every $p \in A$ there is $q \in A$ with $p < q$ .

Picture a cut as "all the rationals strictly to the left of a point on the line". For a rational $r$ the cut $r^\ast = \{q \in \Q : q < r\}$ describes $r$ itself; condition 3 makes this the only cut describing $r$ (we do not allow $\{q \le r\}$ ).

Definition— Cauchy sequence of rationals

A sequence $(q_n)$ of rationals is Cauchy if for every rational $\varepsilon > 0$ there is $N$ with $|q_m - q_n| < \varepsilon$ for all $m, n \geq N$ . Two Cauchy sequences are equivalent if their difference tends to $0$ : for every rational $\varepsilon > 0$ , $|q_n - r_n| < \varepsilon$ for all large $n$ .

ProofH

The integers from pairs of naturals

On $\N \times \N$ define $(a, b) \sim (c, d)$ if $a + d = c + b$ . Think of $(a, b)$ as " $a - b$ "; the condition is $a - b = c - d$ rearranged so that it makes sense in $\N$ , where subtraction is not always possible.

Theorem— Proposition 1

$\sim$ is an equivalence relation on $\N \times \N$ .

Proof

Reflexivity ( $a + b = a + b$ ) and symmetry are clear. For transitivity, suppose $a + d = c + b$ and $c + f = e + d$ . Adding,

(a + f) + (c + d) = (a + d) + (c + f) = (c + b) + (e + d) = (e + b) + (c + d),

and cancelling $c + d$ — legitimate in $\N$ , where $x + k = y + k$ implies $x = y$ — gives $a + f = e + b$ , i.e. $(a, b) \sim (e, f)$ .

∎

Define $\Z$ to be the set of equivalence classes. Guided by $(a - b) + (c - d) = (a + c) - (b + d)$ and $(a - b)(c - d) = (ac + bd) - (ad + bc)$ , set

[(a, b)] + [(c, d)] = [(a + c,\, b + d)], \qquad [(a, b)] \cdot [(c, d)] = [(ac + bd,\, ad + bc)].

Theorem— Proposition 2 (well-definedness)

These formulas define operations on equivalence classes: equivalent inputs give equivalent outputs.

Proof

Addition. If $a + b' = a' + b$ and $c + d' = c' + d$ , then adding the two equations gives $(a + c) + (b' + d') = (a' + c') + (b + d)$ , which says $(a + c, b + d) \sim (a' + c', b' + d')$ .

Multiplication. It suffices to change one factor at a time, because $\sim$ is transitive. Suppose $a + b' = a' + b$ ; we show $(ac + bd, ad + bc) \sim (a'c + b'd, a'd + b'c)$ , that is,

(ac + bd) + (a'd + b'c) = (a'c + b'd) + (ad + bc).

Group the left side as $(a + b')c + (a' + b)d$ and the right side as $(a' + b)c + (a + b')d$ . Since $a + b' = a' + b$ , these are equal. Changing the second factor is the same computation with the roles exchanged.

∎

The ring axioms for $\Z$ now follow from those of $\N$ by computing with representatives; for example associativity of addition reduces to associativity in each coordinate. The class $0 = [(0, 0)]$ is the additive identity, $1 = [(1, 0)]$ the multiplicative identity, and $-[(a, b)] = [(b, a)]$ , because $(a + b, b + a) \sim (0, 0)$ . The map $n \mapsto [(n, 0)]$ embeds $\N$ in $\Z$ preserving $+$ and $\times$ , and every class is $[(n, 0)]$ or $[(0, n)]$ for a unique $n$ (subtract the smaller coordinate from both), so $\Z$ consists of the natural numbers and their negatives — exactly the integers we know. The order is $[(a, b)] \le [(c, d)]$ if $a + d \le c + b$ .

Example— A rule that is not well defined

Why not multiply pairs componentwise, $[(a, b)] \star [(c, d)] = [(ac, bd)]$ ? Because $(0, 0) \sim (1, 1)$ (both stand for $0$ ) while $(0, 0) \star (0, 1) = (0, 0)$ and $(1, 1) \star (0, 1) = (0, 1)$ , and $(0, 0) \not\sim (0, 1)$ . The "product" of the number $0$ and the number $-1$ would depend on how $0$ was written. Well-definedness is never automatic.

ProofH

The rationals as a field of fractions

The same recipe works over any integral domain $D$ — a commutative ring with $0 \neq 1$ and no zero divisors ( $ab = 0$ implies $a = 0$ or $b = 0$ ). On pairs $(a, b) \in D \times (D \setminus \{0\})$ define $(a, b) \sim (c, d)$ if $ad = cb$ .

Theorem— Proposition 3

$\sim$ is an equivalence relation, and the operations

[(a, b)] + [(c, d)] = [(ad + cb,\, bd)], \qquad [(a, b)] \cdot [(c, d)] = [(ac,\, bd)]

are well defined. The classes form a field $\operatorname{Frac}(D)$ , the field of fractions of $D$ , and $a \mapsto [(a, 1)]$ is an injective ring homomorphism $D \to \operatorname{Frac}(D)$ .

Proof

Transitivity. Suppose $ad = cb$ and $cf = ed$ , with $b, d, f \neq 0$ . Then

(af)d = (ad)f = (cb)f = b(cf) = b(ed) = (eb)d,

and since $d \neq 0$ and $D$ has no zero divisors, $(af - eb)d = 0$ forces $af = eb$ .

The operations make sense: $bd \neq 0$ because $b, d \neq 0$ — no zero divisors again.

Addition is well defined. Let $ab' = a'b$ . Then $(ad + cb)(b'd) = (ab')d^2 + cbb'd = (a'b)d^2 + cbb'd = (a'd + cb')(bd)$ , so $(ad + cb, bd) \sim (a'd + cb', b'd)$ ; similarly in the second argument. Multiplication: $(ac)(b'd) = (ab')cd = (a'b)cd = (a'c)(bd)$ .

Field axioms. They follow from those of $D$ by computing with representatives; $[(0, 1)]$ and $[(1, 1)]$ are the zero and identity, and if $[(a, b)] \neq 0$ then $a \neq 0$ and $[(b, a)]$ is its inverse, since $(ab, ba) \sim (1, 1)$ . Finally $[(a, 1)] = [(a', 1)]$ means $a = a'$ , so $a \mapsto [(a, 1)]$ is injective.

∎

Taking $D = \Z$ gives $\Q$ . Writing $a/b$ for $[(a, b)]$ , the definitions become the familiar rules for fractions. Every fraction has a representative with $b > 0$ , and $a/b \le c/d$ (with $b, d > 0$ ) is defined by $ad \le cb$ ; this makes $\Q$ an ordered field.

Example— Where zero divisors break the construction

Over $\Z/6\Z$ , which has zero divisors ( $2 \cdot 3 = 0$ ), the same definition is not even transitive: $3/1 \sim 0/2$ (as $3 \cdot 2 = 0 = 0 \cdot 1$ ) and $0/2 \sim 0/1$ , but $3/1 \not\sim 0/1$ (as $3 \cdot 1 \neq 0$ ). One would be forced to declare $3 = 0$ . Rings with zero divisors can still be "localised", but only by inverting carefully chosen elements, and information is lost.

Universal property. $\operatorname{Frac}(D)$ is the smallest field containing $D$ , in a precise sense: every injective ring homomorphism $g : D \to K$ into a field extends to exactly one ring homomorphism $\operatorname{Frac}(D) \to K$ , namely $a/b \mapsto g(a)g(b)^{-1}$ . For $D = \Z$ there is even less freedom: there is at most one ring homomorphism from $\Q$ to any ring.

ProofH

The real numbers from Dedekind cuts

Let $\R$ be the set of Dedekind cuts, ordered by inclusion: $A \le B$ means $A \subseteq B$ . Each rational $r$ gives the cut $r^\ast = \{q : q < r\}$ , and $r \le s$ if and only if $r^\ast \subseteq s^\ast$ , so $\Q$ sits inside $\R$ with its order. But there are new cuts too:

Theorem— Proposition 4 (a cut for √2)

$S = \{q \in \Q : q < 0 \text{ or } q^2 < 2\}$ is a Dedekind cut, and it is not of the form $r^\ast$ for any rational $r$ .

Proof

$0 \in S$ and $2 \notin S$ . If $p \in S$ and $q < p$ : either $q < 0$ , or $0 \le q < p$ , in which case $p \geq 0$ , so $p^2 < 2$ and $q^2 < p^2 < 2$ . For no greatest element, let $p \in S$ . If $p < 0$ , then $0 \in S$ is larger. If $p \geq 0$ , then $p^2 < 2$ ; put $q = \frac{2p + 2}{p + 2}$ . Then

q - p = \frac{2 - p^2}{p + 2} > 0, \qquad q^2 - 2 = \frac{(2p + 2)^2 - 2(p + 2)^2}{(p + 2)^2} = \frac{2(p^2 - 2)}{(p + 2)^2} < 0,

so $q \in S$ and $q > p$ . Finally, if $S = r^\ast$ , then $r \notin S$ but every rational below $r$ is in $S$ ; as $1 \in S$ , $r > 1 > 0$ , and $r^2 \geq 2$ . If $r^2 > 2$ , the same map gives $q = \frac{2r + 2}{r + 2}$ with $0 < q < r$ and $q^2 - 2 = \frac{2(r^2 - 2)}{(r + 2)^2} > 0$ , so $q \in r^\ast \setminus S$ — impossible. Hence $r^2 = 2$ , contradicting the irrationality of $\sqrt 2$ (proved in the lesson on real numbers).

∎

Theorem— Proposition 5 (cuts are totally ordered)

For any cuts $A, B$ , either $A \subseteq B$ or $B \subseteq A$ .

Proof

Suppose $A \not\subseteq B$ , and pick $p \in A \setminus B$ . Let $q \in B$ . If $q \geq p$ , then $p \in B$ (as $p = q$ or $p < q$ and $B$ is closed downwards) — a contradiction. So $q < p$ , and $q \in A$ because $A$ is closed downwards. Thus $B \subseteq A$ .

∎

Theorem— Theorem 6 (least-upper-bound property)

Let $\mathcal{S}$ be a non-empty set of cuts that is bounded above by some cut $B$ . Then the union $U = \bigcup_{A \in \mathcal{S}} A$ is a cut, and it is the least upper bound of $\mathcal{S}$ .

Proof

$U$ is a cut. It is non-empty, because $\mathcal{S}$ contains some cut, which is non-empty. It is not all of $\Q$ : every $A \in \mathcal{S}$ is contained in $B$ , so $U \subseteq B \neq \Q$ . It is closed downwards: if $p \in U$ , then $p \in A$ for some $A \in \mathcal{S}$ , and every $q < p$ lies in $A \subseteq U$ . It has no greatest element: if $p \in A \in \mathcal{S}$ , then $A$ contains some $q > p$ , and $q \in U$ .

$U$ is an upper bound, since $A \subseteq U$ for every $A \in \mathcal{S}$ . It is the least one: if $C$ is a cut with $A \subseteq C$ for every $A \in \mathcal{S}$ , then $U \subseteq C$ .

∎

The lattice-theoretic content is striking: in the ordered set of cuts, suprema are simply unions. Everything else is work. Addition is defined by $A + B = \{a + b : a \in A, b \in B\}$ (with $0^\ast$ as identity), and multiplication first for positive cuts by $A \cdot B = \{q : q \le ab \text{ for some } a \in A, b \in B \text{ with } a, b > 0\}$ , then extended by the sign rules. Checking that this gives an ordered field takes several pages of routine verification; see Rudin's Principles of Mathematical Analysis, appendix to chapter 1. The result:

Theorem— Theorem 7 (Dedekind)

The Dedekind cuts, with these operations and the inclusion order, form a complete ordered field, and $r \mapsto r^\ast$ embeds $\Q$ in it as an ordered subfield.

Proof: completeness is Theorem 6; the field and order axioms are a long verification, which we do not reproduce (see the reading list).

ExplanationH

The real numbers from Cauchy sequences

Cantor and Méray proposed a different construction, closer to how we compute with real numbers. Let $\mathcal{C}$ be the set of Cauchy sequences of rationals, and identify equivalent ones. The sequences

1,\ 1.4,\ 1.41,\ 1.414,\ \dots \qquad\text{and}\qquad 2,\ \tfrac32,\ \tfrac{17}{12},\ \tfrac{577}{408},\ \dots

(the decimal truncations of $\sqrt 2$ and the Babylonian iteration) are equivalent, and their class is the real number $\sqrt 2$ . Similarly $0.9, 0.99, 0.999, \dots$ is equivalent to the constant sequence $1, 1, 1, \dots$ , which is the precise meaning of $0.999\ldots = 1$ .

Sums and products are computed termwise: $[(q_n)] + [(r_n)] = [(q_n + r_n)]$ and $[(q_n)][(r_n)] = [(q_n r_n)]$ . One checks that sums and products of Cauchy sequences are Cauchy (for products one uses that Cauchy sequences are bounded) and that the operations are well defined. A sequence not equivalent to $0$ is eventually bounded away from $0$ , so it can be inverted termwise from some point on; a class is positive if its terms are eventually at least some fixed rational $\varepsilon > 0$ . The result is again a complete ordered field: completeness is proved by approximating each term of a Cauchy sequence of real numbers $x_n$ by a rational $q_n$ with $|x_n - q_n| < 1/n$ , and showing that $(q_n)$ is Cauchy and its class is the limit. This is how Mathlib builds $\R$ (as Real.ofCauchy), and the same construction, with a different notion of distance, produces the $p$ -adic numbers.

Why are there two constructions? Cuts make the order and completeness easy and the algebra laborious; Cauchy sequences make the algebra easy and the order laborious. The next theorem says it does not matter which one we choose.

ProofH

There is only one complete ordered field

Theorem— Theorem 8 (complete ordered fields are Archimedean)

In a complete ordered field $F$ , the natural numbers $1, 1 + 1, 1 + 1 + 1, \dots$ are not bounded above. Consequently, between any two elements $x < y$ of $F$ there is a rational number.

Proof

Suppose $\N \subseteq F$ were bounded above, with supremum $s$ . Then $s - 1$ is not an upper bound, so $s - 1 < n$ for some natural number $n$ . But then $s < n + 1$ , and $n + 1$ is a natural number — contradicting that $s$ is an upper bound.

For density: choose a natural number $m > 1/(y - x)$ , so that $1/m < y - x$ . The multiples $k/m$ , $k \in \Z$ , are spaced $1/m$ apart, and there is a least integer $k$ with $k/m > x$ (by the Archimedean property, the set of such $k$ is non-empty and bounded below). Then $(k - 1)/m \le x$ , so $k/m \le x + 1/m < y$ .

∎

Theorem— Theorem 9 (uniqueness of the reals)

If $F$ and $G$ are complete ordered fields, there is exactly one order-preserving field isomorphism $F \to G$ .

Proof sketch. Every ordered field contains a copy of $\Q$ (the multiples of $1$ and their quotients), and any field homomorphism must be the identity on it. Define $\phi : F \to G$ by

\phi(x) = \sup{}_G \{ q \in \Q : q < x \}.

The set is non-empty and bounded above in $G$ by the Archimedean property, so the supremum exists by completeness of $G$ . Density of $\Q$ (Theorem 8) shows that $\phi$ is strictly increasing and is the identity on $\Q$ , that it has the inverse $y \mapsto \sup_F\{q \in \Q : q < y\}$ , and, with more work, that it preserves sums and products. Any order-preserving isomorphism must send $x$ to this supremum, which gives uniqueness. Mathlib contains a complete formal proof (cited in the formal section). $\square$

So the Dedekind reals and the Cauchy reals are isomorphic, and so is any other model of the axioms. "The real numbers" is a meaningful phrase: up to unique isomorphism there is only one complete ordered field.

Formal mathematicsF

The constructions in Lean

Lean's quotient types make the constructions literal: Quotient s is the type of equivalence classes of a Setoid (a type with an equivalence relation), and a function on representatives descends to classes — via Quotient.lift or Quotient.map₂ — only when given a proof that it respects the relation. In Lean, well-definedness cannot be forgotten: the definition does not compile without the proof.

The integers. Transitivity (Proposition 1), with the cancellation step made explicit; the setoid and the type of classes; the well-definedness lemmas of Proposition 2, each a calc following the human grouping; and the operations themselves, whose definitions consume those proofs.

intRel_transLean 4Proved here from basic factsFormally verified

/-- **Transitivity of `(a, b) ~ (c, d) ⟺ a + d = c + b`.** Adding the two hypotheses gives
`(a + f) + (c + d) = (e + b) + (c + d)`, and in `ℕ` we may cancel `c + d`. Cancellation is the one
property of `ℕ` that the construction really needs. -/
theorem intRel_trans {a b c d e f : ℕ} (h₁ : a + d = c + b) (h₂ : c + f = e + d) :
    a + f = e + b := by
  have h : (a + f) + (c + d) = (e + b) + (c + d) :=
    calc (a + f) + (c + d) = (a + d) + (c + f) := by ring
      _ = (c + b) + (e + d) := by rw [h₁, h₂]
      _ = (e + b) + (c + d) := by ring
  exact Nat.add_right_cancel h

Axioms used: propextformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

intSetoidLean 4Formally verified

/-- The equivalence relation on `ℕ × ℕ` whose classes are the integers: `(a, b) ~ (c, d)` means
`a + d = c + b`, i.e. "`a - b = c - d`" written without subtraction. Reflexivity and symmetry are
immediate; transitivity is `intRel_trans`. -/
def intSetoid : Setoid (ℕ × ℕ) where
  r p q := p.1 + q.2 = q.1 + p.2
  iseqv := ⟨fun _ => rfl, fun h => h.symm, fun h₁ h₂ => intRel_trans h₁ h₂⟩

Axioms used: propextformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

PairIntLean 4Formally verified

/-- The constructed integers: equivalence classes of pairs of natural numbers. -/
def PairInt : Type := Quotient intSetoid

Axioms used: propextformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

add_respectsLean 4Proved here from basic factsFormally verified

/-- **Addition of classes is well defined.** If `(a, b) ~ (a', b')` and `(c, d) ~ (c', d')`, then
`(a + c, b + d) ~ (a' + c', b' + d')`: add the two equations. -/
theorem add_respects {a b c d a' b' c' d' : ℕ} (h₁ : a + b' = a' + b) (h₂ : c + d' = c' + d) :
    (a + c) + (b' + d') = (a' + c') + (b + d) := by
  calc (a + c) + (b' + d') = (a + b') + (c + d') := by ring
    _ = (a' + b) + (c' + d) := by rw [h₁, h₂]
    _ = (a' + c') + (b + d) := by ring

Axioms used: propextformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

mul_respects_leftLean 4Proved here from basic factsFormally verified

/-- **Multiplication of classes is well defined (first argument).** With
`(a, b) · (c, d) = (ac + bd, ad + bc)` — the rule `(a - b)(c - d) = (ac + bd) - (ad + bc)` —
replacing `(a, b)` by an equivalent `(a', b')` gives an equivalent product. The key step groups
the terms as `(a + b')c + (a' + b)d` and uses `a + b' = a' + b`. -/
theorem mul_respects_left {a b a' b' c d : ℕ} (h : a + b' = a' + b) :
    (a * c + b * d) + (a' * d + b' * c) = (a' * c + b' * d) + (a * d + b * c) := by
  calc (a * c + b * d) + (a' * d + b' * c) = (a + b') * c + (a' + b) * d := by ring
    _ = (a' + b) * c + (a + b') * d := by rw [h]
    _ = (a' * c + b' * d) + (a * d + b * c) := by ring

Axioms used: propextformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

mul_respects_rightLean 4Proved here from basic factsFormally verified

/-- **Multiplication of classes is well defined (second argument):** the same computation with
the roles of the factors exchanged, grouping as `a(c + d') + b(c' + d)`. -/
theorem mul_respects_right {a b c d c' d' : ℕ} (h : c + d' = c' + d) :
    (a * c + b * d) + (a * d' + b * c') = (a * c' + b * d') + (a * d + b * c) := by
  calc (a * c + b * d) + (a * d' + b * c') = a * (c + d') + b * (c' + d) := by ring
    _ = a * (c' + d) + b * (c + d') := by rw [h]
    _ = (a * c' + b * d') + (a * d + b * c) := by ring

Axioms used: propextformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

addLean 4Formally verified

/-- Addition on the constructed integers: `[(a, b)] + [(c, d)] = [(a + c, b + d)]`. It is
well defined by `add_respects`. -/
def add : PairInt → PairInt → PairInt :=
  Quotient.map₂ (fun p q => (p.1 + q.1, p.2 + q.2))
    (fun _ _ h₁ _ _ h₂ => add_respects h₁ h₂)

Axioms used: propext, Quot.soundformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

mulLean 4Formally verified

/-- Multiplication: `[(a, b)] · [(c, d)] = [(ac + bd, ad + bc)]`. Well defined because changing
one argument at a time gives equivalent results (`mul_respects_left`, `mul_respects_right`),
and the relation is transitive. -/
def mul : PairInt → PairInt → PairInt :=
  Quotient.map₂ (fun p q => (p.1 * q.1 + p.2 * q.2, p.1 * q.2 + p.2 * q.1))
    (fun _p p' hp q _q' hq =>
      intRel_trans (mul_respects_left (c := q.1) (d := q.2) hp)
        (mul_respects_right (a := p'.1) (b := p'.2) hq))

Axioms used: propext, Quot.soundformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

To check that the construction really produces the integers, we compare it with Mathlib's ℤ (which is built differently, as an inductive type). The map $[(a, b)] \mapsto a - b$ is well defined, turns the constructed operations into the usual ones, and is a bijection — so it is a ring isomorphism.

toIntLean 4Formally verified

/-- The comparison map to Mathlib's integers: `[(a, b)] ↦ a - b`. It is well defined because
`a + d = c + b` implies `a - b = c - d` in `ℤ`. -/
def toInt : PairInt → ℤ :=
  Quotient.lift (fun p : ℕ × ℕ => (p.1 : ℤ) - p.2)
    (fun p q (h : p.1 + q.2 = q.1 + p.2) => by
      have h' : (p.1 : ℤ) + q.2 = q.1 + p.2 := by exact_mod_cast h
      linear_combination h')

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

toInt_addLean 4Proved here from basic factsFormally verified

/-- The comparison map turns the constructed addition into the addition of `ℤ`:
`(a + c) - (b + d) = (a - b) + (c - d)`. -/
theorem toInt_add (x y : PairInt) : toInt (add x y) = toInt x + toInt y := by
  induction x using Quotient.inductionOn with | h p =>
  induction y using Quotient.inductionOn with | h q =>
  show ((p.1 + q.1 : ℕ) : ℤ) - ((p.2 + q.2 : ℕ) : ℤ) = ((p.1 : ℤ) - p.2) + ((q.1 : ℤ) - q.2)
  push_cast
  ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

toInt_mulLean 4Proved here from basic factsFormally verified

/-- …and the constructed multiplication into the multiplication of `ℤ`:
`(ac + bd) - (ad + bc) = (a - b)(c - d)`. -/
theorem toInt_mul (x y : PairInt) : toInt (mul x y) = toInt x * toInt y := by
  induction x using Quotient.inductionOn with | h p =>
  induction y using Quotient.inductionOn with | h q =>
  show ((p.1 * q.1 + p.2 * q.2 : ℕ) : ℤ) - ((p.1 * q.2 + p.2 * q.1 : ℕ) : ℤ)
    = ((p.1 : ℤ) - p.2) * ((q.1 : ℤ) - q.2)
  push_cast
  ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

toInt_bijectiveLean 4Proved here from basic factsFormally verified

/-- **The construction really produces the integers.** The comparison map is a bijection:
injective because `a - b = c - d` in `ℤ` gives `a + d = c + b` in `ℕ`, and surjective because
`n = n⁺ - n⁻` with `n⁺ = max(n, 0)` and `n⁻ = max(-n, 0)`. Together with `toInt_add` and
`toInt_mul`, it is an isomorphism of rings. -/
theorem toInt_bijective : Function.Bijective toInt := by
  constructor
  · intro x y hxy
    induction x using Quotient.inductionOn with | h p =>
    induction y using Quotient.inductionOn with | h q =>
    change (p.1 : ℤ) - p.2 = (q.1 : ℤ) - q.2 at hxy
    apply Quotient.sound
    show p.1 + q.2 = q.1 + p.2
    omega
  · intro n
    refine ⟨Quotient.mk intSetoid (n.toNat, (-n).toNat), ?_⟩
    show ((n.toNat : ℕ) : ℤ) - (((-n).toNat : ℕ) : ℤ) = n
    omega

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

Fractions. Transitivity of $ad = cb$ in any commutative ring without zero divisors, with the cancellation of $d$ as the crucial last line; the $\Z/6\Z$ counterexample, checked by decide; and Mathlib's statements that $\Q$ is the field of fractions of $\Z$ and that ring homomorphisms out of $\Q$ are unique.

frac_transLean 4Proved here from basic factsFormally verified

/-- **Transitivity of equality of fractions**, `(a, b) ~ (c, d) ⟺ ad = cb`, in any commutative
ring without zero divisors (such as `ℤ`). From `ad = cb` and `cf = ed` we get
`(af)d = (eb)d`, and we cancel `d ≠ 0`. That cancellation is exactly where "no zero divisors"
is used. -/
theorem frac_trans {R : Type*} [CommRing R] [NoZeroDivisors R] {a b c d e f : R} (hd : d ≠ 0)
    (h₁ : a * d = c * b) (h₂ : c * f = e * d) : a * f = e * b := by
  have h : (a * f) * d = (e * b) * d :=
    calc (a * f) * d = (a * d) * f := by ring
      _ = (c * b) * f := by rw [h₁]
      _ = b * (c * f) := by ring
      _ = b * (e * d) := by rw [h₂]
      _ = (e * b) * d := by ring
  exact mul_right_cancel₀ hd h

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

frac_trans_fails_zmod6Lean 4Proved here from basic factsFormally verified

/-- **With zero divisors, "fractions" break.** In `ℤ/6ℤ`, using the same rule
`(a, b) ~ (c, d) ⟺ ad = cb` with non-zero denominators, `3/1 ~ 0/2` and `0/2 ~ 0/1`, but
`3/1 ≁ 0/1`: the relation is not transitive, because `2 · 3 = 0` lets us "cancel" wrongly. -/
theorem frac_trans_fails_zmod6 :
    let r : ZMod 6 × ZMod 6 → ZMod 6 × ZMod 6 → Prop := fun p q => p.1 * q.2 = q.1 * p.2
    r (3, 1) (0, 2) ∧ r (0, 2) (0, 1) ∧ ¬ r (3, 1) (0, 1) := by
  decide

Axioms used: propext, Quot.soundformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

rat_isFractionRingLean 4Applies a library theoremFormally verified

/-- **`ℚ` is the field of fractions of `ℤ`.** Mathlib's instance `Rat.isFractionRing`: every
rational is `a / b` with `a, b ∈ ℤ`, `b ≠ 0`, and `a / b = c / d` exactly when `ad = cb`. -/
theorem rat_isFractionRing : IsFractionRing ℤ ℚ := Rat.isFractionRing

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

ringHom_rat_uniqueLean 4Applies a library theoremFormally verified

/-- **A universal property in miniature:** there is at most one ring homomorphism from `ℚ` to
any ring, because it is forced on `ℤ` and then on fractions. Mathlib's `RingHom.ext_rat`. -/
theorem ringHom_rat_unique {R : Type*} [Semiring R] (f g : ℚ →+* R) : f = g :=
  RingHom.ext_rat f g

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

Dedekind cuts. A cut is a structure carrying a set of rationals together with proofs of the three conditions. The rational cuts and the cut for $\sqrt 2$ (Proposition 4, including the step $p \mapsto \frac{2p + 2}{p + 2}$ ) are constructed; cuts are totally ordered (Proposition 5); and the union of a bounded non-empty family is a cut and its least upper bound (Theorem 6).

CutLean 4Formally verified

/-- A **Dedekind cut**: a set of rationals that is non-empty, not everything, closed downwards,
and has no greatest element. Think of it as "the rationals below a real number". -/
structure Cut where
  /-- The rationals below the real number. -/
  carrier : Set ℚ
  nonempty : carrier.Nonempty
  ne_univ : carrier ≠ Set.univ
  lower : ∀ ⦃p q : ℚ⦄, p ∈ carrier → q < p → q ∈ carrier
  no_max : ∀ p ∈ carrier, ∃ q ∈ carrier, p < q

Axioms used: No axiomsformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

instLELean 4Formally verified

/-- Cuts are ordered by inclusion. -/
instance instLE : LE Cut := ⟨fun A B => A.carrier ⊆ B.carrier⟩

Axioms used: No axiomsformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

ofRatLean 4Formally verified

/-- The cut of a rational number `r`: all rationals below `r`. -/
def ofRat (r : ℚ) : Cut where
  carrier := {q | q < r}
  nonempty := ⟨r - 1, by simp⟩
  ne_univ := fun h => lt_irrefl r (h ▸ Set.mem_univ r : r ∈ {q : ℚ | q < r})
  lower := fun _ _ hp hq => lt_trans hq hp
  no_max := fun p hp => by
    have hp' : p < r := hp
    exact ⟨(p + r) / 2, show (p + r) / 2 < r by linarith, by linarith⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

sqrtTwoLean 4Formally verified

/-- **The cut of `√2`:** the rationals `q` with `q < 0` or `q² < 2`. It has no greatest element:
if `0 ≤ p` and `p² < 2`, the rational `(2p + 2)/(p + 2)` is larger than `p` and its square is
still below `2`. -/
def sqrtTwo : Cut where
  carrier := {q | q < 0 ∨ q * q < 2}
  nonempty := ⟨0, Or.inr (by norm_num)⟩
  ne_univ := by
    intro h
    have h2 : (2 : ℚ) ∈ {q : ℚ | q < 0 ∨ q * q < 2} := h ▸ Set.mem_univ 2
    rcases h2 with h2 | h2 <;> norm_num at h2
  lower := by
    intro p q hp hqp
    rcases lt_or_ge q 0 with hq | hq
    · exact Or.inl hq
    · right
      rcases hp with hp | hp
      · linarith
      · nlinarith
  no_max := by
    intro p hp
    rcases lt_or_ge p 0 with hp0 | hp0
    · exact ⟨0, Or.inr (by norm_num), hp0⟩
    · have hp2 : p * p < 2 := by
        rcases hp with hp | hp
        · linarith
        · exact hp
      have hpos : 0 < p + 2 := by linarith
      refine ⟨(2 * p + 2) / (p + 2), Or.inr ?_, ?_⟩
      · rw [div_mul_div_comm, div_lt_iff₀ (by positivity)]
        nlinarith
      · rw [lt_div_iff₀ hpos]
        nlinarith

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

le_totalLean 4Proved here from basic factsFormally verified

/-- **Cuts are totally ordered.** If `A ⊄ B`, pick `p ∈ A` with `p ∉ B`. Every `q ∈ B` is below
`p` (otherwise `p ≤ q` would put `p` in `B`, which is closed downwards), so `q ∈ A`. -/
theorem le_total (A B : Cut) : A ≤ B ∨ B ≤ A := by
  by_cases h : A ≤ B
  · exact Or.inl h
  · right
    obtain ⟨p, hpA, hpB⟩ := Set.not_subset.mp h
    intro q hqB
    rcases lt_or_ge q p with hqp | hpq
    · exact A.lower hpA hqp
    · exfalso
      rcases hpq.lt_or_eq with hlt | heq
      · exact hpB (B.lower hqB hlt)
      · exact hpB (heq ▸ hqB)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

supLean 4Formally verified

/-- The **supremum** of a non-empty family `S` of cuts that is bounded above by a cut `B`: the
union of the family. The proofs check that the union is again a cut: it is non-empty because `S`
and its members are; it is not everything because it lies inside `B`; and it is closed
downwards and has no greatest element because each member is and has none. -/
def sup (S : Set Cut) (hS : S.Nonempty) (hB : ∃ B : Cut, ∀ A ∈ S, A ≤ B) : Cut where
  carrier := ⋃ A ∈ S, A.carrier
  nonempty := by
    obtain ⟨A, hA⟩ := hS
    obtain ⟨p, hp⟩ := A.nonempty
    exact ⟨p, Set.mem_biUnion hA hp⟩
  ne_univ := by
    obtain ⟨B, hB⟩ := hB
    obtain ⟨q, hq⟩ : ∃ q, q ∉ B.carrier := by
      by_contra h
      exact B.ne_univ (Set.eq_univ_of_forall fun q => by_contra fun hq => h ⟨q, hq⟩)
    intro h
    have hq' : q ∈ ⋃ A ∈ S, A.carrier := h ▸ Set.mem_univ q
    obtain ⟨A, hA, hqA⟩ := Set.mem_iUnion₂.mp hq'
    exact hq (hB A hA hqA)
  lower := by
    intro p q hp hqp
    obtain ⟨A, hA, hpA⟩ := Set.mem_iUnion₂.mp hp
    exact Set.mem_biUnion hA (A.lower hpA hqp)
  no_max := by
    intro p hp
    obtain ⟨A, hA, hpA⟩ := Set.mem_iUnion₂.mp hp
    obtain ⟨q, hqA, hpq⟩ := A.no_max p hpA
    exact ⟨q, Set.mem_biUnion hA hqA, hpq⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

sup_isLUBLean 4Proved here from basic factsFormally verified

/-- **The least-upper-bound property of the cuts.** The union `sup S` is an upper bound of `S`
(each member is contained in the union) and it is the least one (if every member of `S` lies in
`C`, so does their union). -/
theorem sup_isLUB (S : Set Cut) (hS : S.Nonempty) (hB : ∃ B : Cut, ∀ A ∈ S, A ≤ B) :
    (∀ A ∈ S, A ≤ sup S hS hB) ∧ (∀ C : Cut, (∀ A ∈ S, A ≤ C) → sup S hS hB ≤ C) := by
  constructor
  · intro A hA p hp
    exact Set.mem_biUnion hA hp
  · intro C hC p hp
    obtain ⟨A, hA, hpA⟩ := Set.mem_iUnion₂.mp hp
    exact hC A hA hpA

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

What Mathlib provides. Completeness of Mathlib's $\R$ (built from Cauchy sequences), and the isomorphism between any two conditionally complete linearly ordered fields — Theorem 9, formalised in full in Mathlib with exactly the map $x \mapsto \sup\{q \in \Q : q < x\}$ .

real_completeLean 4Applies a library theoremFormally verified

/-- **Completeness of Mathlib's `ℝ`** (built from Cauchy sequences of rationals): every non-empty
set of reals that is bounded above has a least upper bound. This is `Real.exists_isLUB`. -/
theorem real_complete {S : Set ℝ} (hne : S.Nonempty) (hbdd : BddAbove S) : ∃ x, IsLUB S x :=
  Real.exists_isLUB hne hbdd

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

complete_ordered_field_uniqueLean 4Applies a library theoremFormally verified

/-- **Uniqueness of the complete ordered field.** Any two conditionally complete linearly
ordered fields are isomorphic as ordered rings: Mathlib's
`ConditionallyCompleteLinearOrderedField.inducedOrderRingIso`, which sends `x` to the supremum
of the rationals below `x`. (Mathlib also proves the isomorphism is unique.) -/
noncomputable def complete_ordered_field_unique (F G : Type*)
    [Field F] [ConditionallyCompleteLinearOrder F] [IsStrictOrderedRing F]
    [Field G] [ConditionallyCompleteLinearOrder G] [IsStrictOrderedRing G] : F ≃+*o G :=
  ConditionallyCompleteLinearOrderedField.inducedOrderRingIso F G

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/NumberSystemConstructions.leanTry it in the Lean web editor

Not formalised here: the ring axioms for the constructed integers (they follow by transport along the bijection toInt, but we do not build the CommRing instance), the field structure on cuts (addition and multiplication of cuts), the fact that the √2 cut is not rational, and the Cauchy construction itself (Mathlib's Real is that construction).

ComputationC

Testing well-definedness, and approaching a gap

An operation on classes is well defined if every choice of representatives gives equivalent answers. A computer can try all small choices. The correct rules pass; the tempting wrong ones — multiplying integer pairs componentwise, or adding fractions by adding numerators and denominators (the mediant) — fail, and the search returns explicit counterexamples. A counterexample is a proof of failure; a pass is only evidence.

Well-definedness tested on every small representativePythonExhaustive finite checkCounterexampleComputationally tested

"""Is an operation on equivalence classes well defined? Test every representative.

Integers are built as classes of pairs (a, b) of naturals with
(a, b) ~ (c, d) iff a + d = c + b, and fractions as classes of pairs (a, b)
with b != 0 and (a, b) ~ (c, d) iff ad = cb. An operation on pairs defines an
operation on classes only if equivalent inputs always give equivalent outputs.
The experiment checks this exhaustively for small pairs: the lesson's addition
and multiplication pass, while two tempting rules - "multiply componentwise"
for integer pairs and the "mediant" (a + c)/(b + d) for fractions - fail, and
it prints a counterexample for each. It also shows "fractions" over Z/6Z
breaking transitivity. Exhaustive for small cases; the general claims are
the lesson's proofs.
"""

import itertools

N = range(7)

def int_rel(p, q):
    """(a, b) ~ (c, d) iff a + d = c + b: both stand for a - b = c - d."""
    return p[0] + q[1] == q[0] + p[1]

def int_add(p, q):
    """(a, b) + (c, d) = (a + c, b + d)."""
    return (p[0] + q[0], p[1] + q[1])

def int_mul(p, q):
    """(a, b)(c, d) = (ac + bd, ad + bc), from (a - b)(c - d)."""
    return (p[0] * q[0] + p[1] * q[1], p[0] * q[1] + p[1] * q[0])

def int_bad(p, q):
    """A tempting but wrong rule: multiply componentwise."""
    return (p[0] * q[0], p[1] * q[1])

def frac_rel(p, q):
    """(a, b) ~ (c, d) iff ad = cb."""
    return p[0] * q[1] == q[0] * p[1]

def frac_add(p, q):
    """a/b + c/d = (ad + cb)/(bd)."""
    return (p[0] * q[1] + q[0] * p[1], p[1] * q[1])

def mediant(p, q):
    """The 'freshman sum' (a + c)/(b + d)."""
    return (p[0] + q[0], p[1] + q[1])

def counterexample(pairs, rel, op):
    """First (p, p', q, q') with p ~ p', q ~ q' but op(p, q) !~ op(p', q')."""
    equiv = [(p, p2) for p in pairs for p2 in pairs if rel(p, p2)]
    for (p, p2), (q, q2) in itertools.product(equiv, repeat=2):
        if not rel(op(p, q), op(p2, q2)):
            return p, p2, q, q2
    return None

def transitivity_failure(n):
    """Pairs in Z/nZ with non-zero second entry breaking transitivity."""
    pairs = [(a, b) for a in range(n) for b in range(1, n)]

    def rel(p, q):
        return (p[0] * q[1] - q[0] * p[1]) % n == 0

    for x, y, z in itertools.product(pairs, repeat=3):
        if rel(x, y) and rel(y, z) and not rel(x, z):
            return x, y, z
    return None

def main():
    ints = [(a, b) for a in N for b in N]
    fracs = [(a, b) for a in range(0, 5) for b in range(1, 6)]
    print(f"Integer pairs (a, b) with 0 <= a, b <= 6: {len(ints)}")
    for name, op in [("(a+c, b+d)", int_add), ("(ac+bd, ad+bc)", int_mul),
                     ("(ac, bd)", int_bad)]:
        bad = counterexample(ints, int_rel, op)
        verdict = "well defined" if bad is None else f"FAILS: {bad}"
        print(f"  {name:<16}{verdict}")
    p, p2, q, q2 = counterexample(ints, int_rel, int_bad)
    print(f"  {p} ~ {p2} and {q} ~ {q2}, but the products")
    print(f"  {int_bad(p, q)} and {int_bad(p2, q2)} are not equivalent")
    print()
    print(f"Fraction pairs a/b with 0 <= a <= 4, 1 <= b <= 5: {len(fracs)}")
    for name, op in [("(ad+cb)/(bd)", frac_add), ("(a+c)/(b+d)", mediant)]:
        bad = counterexample(fracs, frac_rel, op)
        verdict = "well defined" if bad is None else f"FAILS: {bad}"
        print(f"  {name:<16}{verdict}")
    p, p2, q, q2 = counterexample(fracs, frac_rel, mediant)
    m1, m2 = mediant(p, q), mediant(p2, q2)
    print(f"  {p[0]}/{p[1]} = {p2[0]}/{p2[1]} and {q[0]}/{q[1]} = {q2[0]}/{q2[1]},"
          f" but {m1[0]}/{m1[1]} != {m2[0]}/{m2[1]}")
    print()
    for n in (5, 6):
        print(f"'Fractions' over Z/{n}Z, transitivity counterexample:",
              transitivity_failure(n))
    print()
    print("Epistemic status: exhaustive checks over small representatives, plus")
    print("explicit counterexamples. A failure found here is a proof that the")
    print("rule is not well defined; a pass is only evidence. The lesson proves")
    print("well-definedness of the correct operations for all representatives.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The second experiment works entirely inside $\Q$ , with exact fractions. The climbing sequence stays inside the $\sqrt 2$ cut and the Babylonian sequence outside it, and the gap between them shrinks rapidly — two equivalent Cauchy sequences of rationals, crowding towards a point that $\Q$ does not contain.

Closing in on the square root of 2 with fractionsPythonExact computationExhaustive finite checkComputationally tested

"""Closing in on the square root of 2 with rationals only: cuts and Cauchy sequences.

Two sequences of exact fractions approach the "missing" number sqrt(2): the
Babylonian (Newton) iteration x -> (x + 2/x)/2 from above, and the map
q -> (2q + 2)/(q + 2) from below, which the lesson uses to show that the
Dedekind cut {q : q < 0 or q^2 < 2} has no largest element. The experiment
checks with exact rational arithmetic that the lower terms stay inside the
cut, the upper terms stay outside, the gap between them shrinks, and the two
sequences are equivalent Cauchy sequences (their difference tends to 0). It
also checks that no fraction with denominator up to 1000 squares to 2. All
arithmetic is exact; the statements about limits are not proved by it.
"""

from fractions import Fraction

TWO = Fraction(2)

def in_cut(q):
    """Membership in the Dedekind cut of sqrt(2): q < 0 or q^2 < 2."""
    return q < 0 or q * q < TWO

def babylonian(x):
    """One Newton step for x^2 = 2: the average of x and 2/x."""
    return (x + TWO / x) / 2

def climb(q):
    """The lesson's step inside the cut: (2q + 2)/(q + 2) > q when q^2 < 2."""
    return (2 * q + 2) / (q + 2)

def iterate(step, start, n):
    """The list [start, step(start), ..., step^n(start)]."""
    terms = [Fraction(start)]
    for _ in range(n):
        terms.append(step(terms[-1]))
    return terms

def no_rational_root(max_den):
    """True if no p/q with 1 <= q <= max_den has (p/q)^2 = 2."""
    for q in range(1, max_den + 1):
        p = int((2 * q * q) ** 0.5)
        if any(r * r == 2 * q * q for r in (p - 1, p, p + 1)):
            return False
    return True

def main():
    upper = iterate(babylonian, 2, 5)
    lower = iterate(climb, 1, 5)
    print(" n  lower (in cut)   upper (not in cut)  gap upper - lower")
    for n, (lo, up) in enumerate(zip(lower, upper)):
        lo_s, up_s = f"{lo}", f"{up}"
        if len(up_s) > 18:
            up_s = f"({len(str(up.numerator))} digits)/..."
        gap = float(up - lo)
        print(f"{n:>2}  {lo_s:<15}  {up_s:<18}  {gap:.3e}")
    print("all lower terms in the cut:", all(in_cut(q) for q in lower))
    print("no upper term in the cut:  ", not any(in_cut(x) for x in upper))
    print("lower terms increase:      ",
          all(a < b for a, b in zip(lower, lower[1:])))
    err = [float(x * x - TWO) for x in upper]
    print("upper x^2 - 2:", ", ".join(f"{e:.1e}" for e in err[1:]))
    print("(Newton roughly squares the error at each step.)")
    print("no fraction p/q with q <= 1000 squares to 2:", no_rational_root(1000))
    print()
    print("Epistemic status: exact rational arithmetic for finitely many terms.")
    print("It shows the gap shrinking but cannot show that it tends to 0, nor")
    print("that sqrt(2) is irrational (only that no small fraction works). Those")
    print("are proved in the lesson and in the lesson on real numbers.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Exercises

1. Constructing ℤ, ℚ and ℝ

Warm-upHuman

With $(a, b) \sim (c, d)$ iff $a + d = c + b$ , which pairs of natural numbers lie in the class that represents the integer $-2$ ? (Choose all that apply.)

Choose all that apply

2. Constructing ℤ, ℚ and ℝ

Warm-upHuman

Using $[(a, b)] \cdot [(c, d)] = [(ac + bd,\, ad + bc)]$ , compute $[(3, 5)] \cdot [(4, 1)]$ . Which integer does the resulting class represent?

3. Constructing ℤ, ℚ and ℝ

CoreHuman

In the proof that equality of fractions ( $ad = cb$ ) is transitive, from $ad = cb$ and $cf = ed$ we derive $(af)d = (eb)d$ . Which step needs the hypothesis that the ring has no zero divisors?

Choose one

Concluding

af = eb

from

(af)d = (eb)d

and

d \neq 0

Rewriting

(af)d = (ad)f

Substituting

ad = cb

Reflexivity,

ab = ab

4. Constructing ℤ, ℚ and ℝ

CoreHuman

Each rule below is defined on a representative $a/b$ (or two, $a/b$ and $c/d$ ) of a rational number, with $b, d \neq 0$ . Which rules are not well defined as functions of the rational numbers? (Choose all that apply.)

Choose all that apply

(a/b, c/d) \mapsto (a + c)/(b + d)

(a/b, c/d) \mapsto (ad + cb)/(bd)

a/b \mapsto b/a

, for

a \neq 0

a/b \mapsto a + b

a/b \mapsto a^2/b^2

5. Constructing ℤ, ℚ and ℝ

CoreHuman

Which of these subsets of $\Q$ are Dedekind cuts (non-empty, not all of $\Q$ , closed downwards, no greatest element)? (Choose all that apply.)

Choose all that apply

6. Constructing ℤ, ℚ and ℝ

CoreHuman

Which example shows that $\Q$ is not complete (that not every non-empty, bounded-above subset has a least upper bound in $\Q$ )?

Choose one

\{q \in \Q : q^2 < 2\}

\N \subseteq \Q

\{q \in \Q : q < 1\}

the sequence

(-1)^n

7. Constructing ℤ, ℚ and ℝ

CoreFormal

In the lesson's Lean file, PairInt.add is defined with Quotient.map₂ (fun p q => (p.1 + q.1, p.2 + q.2)) (proof). What is the second argument, and what happens if you leave it out?

Choose one

A proof that equivalent inputs give equivalent outputs (here built from add_respects); without it the definition does not type-checkA proof of commutativity of addition; without it Lean assumes addition is not commutativeAn optional hint for the simplifier; leaving it out only makes proofs slowerThe decidability of the relation; without it Lean cannot compute

8. Constructing ℤ, ℚ and ℝ

StretchComputational

Implement the integers as pairs of natural numbers. Write canonical(p), returning the representative of the class of p that has a $0$ in at least one coordinate, and mul(p, q) using $(a, b)(c, d) = (ac + bd, ad + bc)$ . Then check, for all pairs with entries up to $5$ , that mul is well defined: equivalent inputs give outputs with the same canonical form.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"Operations on equivalence classes are automatically well defined." They are not. Componentwise multiplication of integer pairs, and the mediant $\frac{a + c}{b + d}$ of fractions, are perfectly good operations on pairs that do not respect the equivalence: $\tfrac12 = \tfrac24$ but the mediants of these with $\tfrac13$ are $\tfrac25 \neq \tfrac37$ . Every operation on classes needs a proof that it does not depend on the representatives.

Misconception

"The constructions tell us what numbers really are." They show that structures with the required properties exist (given $\N$ and set theory), not that $-3$ "is" a set of pairs or $\sqrt 2$ "is" a set of rationals. The Dedekind and Cauchy constructions produce different sets, yet Theorem 9 says they are isomorphic; what matters is the structure, which is unique up to unique isomorphism.

Misconception

" $\Q$ is complete because between any two rationals there is another." Density is not completeness. The rationals are dense, yet $\{q : q^2 < 2\}$ is bounded above with no least upper bound in $\Q$ , and the Babylonian sequence is Cauchy with no rational limit.

Misconception

" $0.999\ldots$ is slightly less than $1$ ." In the Cauchy construction $0.999\ldots$ is the class of $0.9, 0.99, 0.999, \dots$ , which differs from the constant sequence $1$ by $10^{-n} \to 0$ : the two sequences are equivalent, so they are the same real number. With cuts: the rationals below $0.999\ldots$ are exactly the rationals below $1$ .

Misconception

"A cut is the same as its supremum, so $\{q \le r\}$ is also a cut." Condition 3 (no greatest element) rules out $\{q \le r\}$ ; without it, every rational would be described by two different cuts. Conventions differ between books (some use upper sets, or allow a greatest element and exclude the other one), but each makes the correspondence one-to-one.

ViewpointsH

Many ways of seeing

Analysis— Completion of a metric space, and other completions of Q

The Cauchy construction works in any metric space $X$ : the completion $\hat X$ is the set of Cauchy sequences up to equivalence, and $X$ sits densely inside the complete space $\hat X$ ; every uniformly continuous map from $X$ to a complete space extends uniquely to $\hat X$ . Completing $\Q$ for the usual distance gives $\R$ . But $\Q$ has other distances: for a prime $p$ , $|x|_p = p^{-k}$ when $x = p^k a/b$ with $p \nmid ab$ . Completing $\Q$ for $|\cdot|_p$ gives the field $\Q_p$ of $p$ -adic numbers, in which $1 + p + p^2 + \cdots$ converges (to $1/(1 - p)$ ). Ostrowski's theorem (1916) says that up to equivalence these are all the non-trivial absolute values on $\Q$ : so $\R$ and the $\Q_p$ are all the completions of $\Q$ (see real analysis and congruences).

Topology— Completeness is connectedness

Give an ordered set its order topology. A densely ordered set without endpoints is connected if and only if it is Dedekind complete (every non-empty bounded-above subset has a supremum). So the completeness of $\R$ is the same thing as its connectedness — the intermediate value theorem in disguise — while $\Q$ is totally disconnected: for any irrational $\alpha$ , the sets $\{q < \alpha\}$ and $\{q > \alpha\}$ split $\Q$ into two disjoint open pieces. The Dedekind construction is an instance of a general order-theoretic completion, the Dedekind–MacNeille completion, which embeds any partially ordered set into a complete lattice (see point-set topology).

Algebra— Group completion and localisation

The construction of $\Z$ works for any commutative monoid $M$ : pairs $(a, b)$ modulo $(a, b) \sim (c, d)$ iff $a + d + k = c + b + k$ for some $k$ give an abelian group $K(M)$ , the Grothendieck group, with a universal property — every monoid homomorphism from $M$ to an abelian group factors uniquely through $K(M)$ . (The extra $k$ is needed when $M$ lacks cancellation; for $\N$ it can be dropped.) Applied to isomorphism classes of vector bundles, this is the starting point of topological K-theory. The construction of $\Q$ is localisation: for a multiplicative subset $S$ of a commutative ring $R$ , the ring $S^{-1}R$ of fractions $r/s$ — used constantly in commutative algebra and algebraic geometry.

Logic— Categorical in second-order logic, not in first-order logic

The axioms of a complete ordered field are categorical: by Theorem 9 they have exactly one model up to isomorphism. But the completeness axiom quantifies over all subsets — it is a second-order statement. If we keep only first-order consequences (statements about elements), uniqueness fails: by the compactness theorem there are non-Archimedean ordered fields — such as the hyperreals of non-standard analysis — that satisfy exactly the same first-order sentences as $\R$ , and by the Löwenheim–Skolem theorem there are countable ones, such as the field of real algebraic numbers. Tarski proved (1948) that this first-order theory, the theory of real closed fields, is decidable (see model theory).

Geometry— Eudoxus, Euclid and the continuous line

Book V of Euclid's Elements (about 300 BCE), usually credited to Eudoxus, defines when two ratios of magnitudes are equal: $a : b = c : d$ if, for all whole numbers $m, n$ , $ma > nb$ exactly when $mc > nd$ , and likewise with $=$ and $<$ . In modern terms, a ratio is determined by the set of fractions $n/m$ below it — a Dedekind cut, more than two thousand years early. Dedekind discussed the relationship with Euclid's definition in letters to Rudolf Lipschitz (1876). Geometry also motivated completeness: Euclid's very first construction assumes that two circles cross where they ought to, a continuity assumption that rational coordinates do not satisfy. Hilbert's axioms for geometry (1899) acquired, in later editions, an axiom of completeness for exactly this reason, so that the points of a line correspond to the real numbers (see Euclidean geometry).

Wonder Trails

Wonder Trail · Optional · never gradedRemainder familiesSort every integer — positive, negative and zero — into families by its remainder after dividing by 3. If you add a member of one family to a member of another, does the family of the answer depend on which members you chose?Follow the trail

History & global context

History and global context

Ancient ratios. Greek mathematicians discovered incommensurable magnitudes (the side and diagonal of a square), and Eudoxus's theory of proportion, preserved in Book V of Euclid's Elements, handled them rigorously without numbers. Negative quantities and zero were treated as numbers in Chinese and Indian mathematics many centuries before Europe (see the integers lesson).
Decimals. Decimal fractions were used by al-Uqlīdisī (952–953 CE, Damascus) and al-Kāshī (1427, Samarkand), and popularised in Europe by Simon Stevin's De Thiende (1585). An infinite decimal is, implicitly, a Cauchy sequence.
Arithmetisation. In the nineteenth century, analysts wanted the foundations of calculus to rest on arithmetic rather than geometric intuition. William Rowan Hamilton (1837) defined complex numbers as pairs of reals. Karl Weierstrass lectured on a construction of the reals in Berlin in the 1860s. In 1872 three constructions appeared: Charles Méray's and Georg Cantor's by sequences (Méray's dated from 1869), and Richard Dedekind's by cuts, in Stetigkeit und irrationale Zahlen, an idea he said he had conceived in 1858 while teaching calculus in Zürich.
Foundations of the naturals. Dedekind's Was sind und was sollen die Zahlen? (1888) and Giuseppe Peano's axioms (1889) characterised the natural numbers themselves. David Hilbert (1900) described the reals axiomatically as a complete ordered field, and Edmund Landau's Grundlagen der Analysis (1930) carried out the whole chain of constructions in full detail.

Do the numbers exist?

One idea, used three times

Definitions

The integers from pairs of naturals

The rationals as a field of fractions

The real numbers from Dedekind cuts

The real numbers from Cauchy sequences

There is only one complete ordered field

The constructions in Lean

Testing well-definedness, and approaching a gap

Exercises

Common misconceptions

Many ways of seeing

Wonder Trails

History and global context

Further reading