Every limit in the earlier chapters is a real number that was not on the list when the sequence began. A sequence of rationals can close in on a number that is not rational, so the claim that the limit exists has to come from somewhere. It comes from one property of the real numbers: a nonempty set with an upper bound has a least upper bound.
Take the rationals whose square is less than 2. Any rational u > 0 with u2 > 2 is an upper bound for that set, and it is never the least one: the rational u′ = (u2 + 2)/(2u) is smaller and still an upper bound, because u′2 − 2 = (u2 − 2)2/(4u2) > 0 and u − u′ = (u2 − 2)/(2u) > 0. Starting at 3/2 this gives 3/2, 17/12, 577/408, each smaller than the last and each with square above 2; 17/12 squared is 289/144, which is 2 + 1/144. The same holds from below: for a rational x ≥ 0 with x2 < 2, the rational x′ = (2x + 2)/(x + 2) is larger and still has square below 2, since x′2 − 2 = (2x2 − 4)/(x + 2)2. So the set has no least rational upper bound.
The step that remains is that no rational has square 2: if p2 = 2q2 with p/q in lowest terms, then p is even, say p = 2r, so q2 = 2r2 and q is even too, against lowest terms. This is Lebl’s Example 1.1.4 (p.24), where the property that fails is Definition 1.1.3, the least-upper-bound property. The script checks both update formulas on 1,187 fractions above √2 and 673 below it (denominators up to 30, not reduced, so some values repeat), and finds no solution of p2 = 2q2 with q up to 3,000. The finite checks test the formulas; the parity argument is what proves the claim. Lean: newton_improves and control_no_rational_sqrt_two are proved from field arithmetic and Mathlib’s irrationality of √2; completeness is Mathlib’s Real.exists_isLUB. All of it compiles; the axiom report lists only propext, Classical.choice and Quot.sound.
A bounded sequence has a convergent part (Bolzano–Weierstrass, Lebl Thm 2.3.8, p.78). The sequence xn = (−1)n(1 + 1/n) is bounded by 2 and does not converge, but its even terms satisfy x2k − 1 = 1/(2k) exactly, and its odd terms x2k−1 + 1 = −1/(2k−1) exactly, so one subsequence tends to 1 and the other to −1. Control: xn = n is unbounded and has no convergent subsequence, since any strictly increasing choice of indices has nk ≥ k.
A continuous function crosses every value between two of its values (Bolzano’s intermediate value theorem, Thm 3.3.8, p.133). Take f(x) = x3 − x − 1 on [1, 2], where f(1) = −1 and f(2) = 5. Bisection (Example 3.3.9, p.134), in exact arithmetic, keeps f(a) < 0 < f(b) at each of 40 steps and traps a root in an interval of width exactly 2−40, at about 1.3247179572. The only rational candidates for a root, ±1, are not roots, so the root the bisection finds is not a rational: the theorem is delivering a number that is not on the rational list. Two controls. Over the rationals, the same bisection for x2 − 2 on [0, 2] never lands on a zero in 60 steps: the function changes sign, the interval shrinks to width 2−59, and there is no rational to land on. And a step function that is −1 below 1/2 and +1 from 1/2 changes sign on [0, 1] without ever being zero: continuity is a hypothesis.
A continuous function on a closed interval attains its maximum and minimum (Thm 3.3.2, p.130). For x(1 − x) on [0, 1] the identity 1/4 − x(1 − x) = (x − 1/2)2 shows the maximum is 1/4, attained only at 1/2 (checked exactly on a grid of 201 points). Controls: x on the open interval (0, 1) has no maximum, because (x + 1)/2 is larger; and 1/x on (0, 1] is unbounded, with value n at x = 1/n. Closed and bounded matter.
Lean: bolzano_weierstrass, ivt and extreme_value call Mathlib’s own theorems (tendsto_subseq_of_bounded, intermediate_value_Icc, IsCompact.exists_isMaxOn and exists_isMinOn); they compile, and they check the statements, not Lebl’s proofs.
A sequence of functions converges pointwise if it converges at each point separately, and uniformly if one index N works for every point at once (Definition 6.1.6, p.229). Take fn(x) = xn on [0, 1). At each point tried (1/2, 9/10, 99/100) the powers fall below 1/1000 eventually, so the pointwise limit is 0. But at xn = 1 − 1/(2n) the value is at least 1/2 for every n, by Bernoulli’s inequality (1 − t)n ≥ 1 − nt; the script checks it exactly for n up to 300. So for ε = 1/2 no N works, and the convergence is not uniform (compare Lebl’s Example 6.1.8, p.230, for x2n on [−1, 1]). Each xn is continuous on [0, 1], yet at x = 1 every one equals 1 while the limit elsewhere is 0: the limit jumps, which Theorem 6.2.2 (p.235) forbids under uniform convergence.
A uniform case: fn(x) = x/(1 + nx2). Since (1 + nx2)2 − 4nx2 = (1 − nx2)2 ≥ 0, we get |fn(x)| ≤ 1/(2√n) for every x, with equality at x = 1/k when n = k2. So for ε = 1/100, any N > 2500 works for all x at once. Lean: uniform_limit_continuous, Mathlib’s TendstoUniformly.continuous, compiled (the first attempt passed continuity for all n where the library asks for frequently many n; it is now fixed).
Chapter 7 uses the monotone convergence theorem (Lebl Thm 2.1.10, p.55): a bounded increasing sequence converges. The standard proof takes the supremum of the terms, and that supremum exists by completeness; in the rationals the sequence 1, 1.4, 1.41, 1.414, … of decimal truncations of √2 is bounded and increasing and has no rational limit. That is the sense in which chapter 7’s steps were allowed: they were taken in the real numbers. This chapter checks the property and its consequences on examples; it does not trace each earlier step back to it.