The Dottie Number

Machine Logic

At the junction of computation, logic and mathematics

The Dottie Number

26 Jun 2026

examples

Isar

locales

Archive of Formal Proofs

Once upon a time, goes the story, a lady named Dottie got bored and started playing with her calculator, pressing the cosine key over and over again. At first the numbers fluctuated wildly, but over time they always settled down to approximately 0.739085. (This only works if your calculator is set to radians, not degrees.) She had discovered the unique fixed point of the cosine function. The Dottie number has several further properties: it is a global attractor, meaning the limit is the same no matter what number you start with, and it is transcendental. It is a great example for showing off a range of computer algebra techniques in Isabelle, such as differentiation and unlimited precision real computations. Let’s prove those properties just mentioned and calculate (by proof!) its value to 12 decimal places.

Getting started

We begin by defining dottie to be the unique fixed point of cos. But this definition, using the definite descriptor THE, will be good for nothing until both existence and uniqueness of a fixed point have been proved.

definition dottie :: real where "dottie ≡ THE x. cos x = x"

Those claims will be proved with the help of the function $g(x)=\cos x - x$. Note that it slopes downwards.

We can see that it has a unique root near $\frac{\pi}{4}$, but now we have to prove it. Several different theorems need facts about $g$, so to avoid duplication we create a locale where we can work with $g$.

locale Dottie = fixes g :: "real ⇒ real" defines "g ≡ λx::real. cos x - x"

begin

Thanks to the begin, we are now working inside the locale. We have access to the function $g$ and can accumulate facts about it. Our first task is to investigate its derivative.

lemma g_has_negative_deriv: assumes "¦t¦ ≤ 1" shows "∃d. (g has_real_derivative d) (at t) ∧ d 0" proof (intro exI conjI) show "(g has_real_derivative (- sin t - 1)) (at t)" unfolding g_def by (auto intro!: derivative_eq_intros) show "- sin t - 1 0" using assms pi_gt3 le_arcsin_iff [of _ t] by fastforce qed

Isabelle is capable of calculating derivatives automatically. The trick, as we see above, is to hit the goal repeatedly with derivative_eq_intros, which is a collection of facts about derivatives of various operators. The effect is practically the same as the schoolbook method. If you know the derivative already, as here, it makes things easier to mention it. Here we prove that the derivative of $g(t)$, which is $-\sin t-1$, is strictly negative over the given interval $[-1,1]$.

Although computer algebra systems are not always sound, we can use them to write correct Isabelle proofs. Via the fundamental theorem of calculus, we can handle tough integrals. We give the hard work to the computer algebra system; Isabelle merely has to take the derivative of the claimed integral and compare that with the original integrand.

Existence

Existence is proved using the intermediate value theorem, which states that a function $g$ that is continuous on a given closed interval $[a,b]$ attains all the points between $g(a)$ and $g(b)$. Our $g$ is continuous. Since $g(0) = 1$ and $g(1) = \cos 1 - 1 lemma dottie_exists: "∃x::real. 0 x ∧ x 1 ∧ cos x = x" proof - have g_cont: "continuous_on {0..1} g" unfolding g_def by (intro continuous_intros) obtain "g 0 = 1" "g 1 0" using cos_1_lt_1 by (simp add: g_def) with IVT2'[of g 1 0 0] g_cont obtain x where hx: "0 ≤ x" "x ≤ 1" "g x = 0" by (metis less_eq_real_def zero_le_one) hence cos_eq: "cos x = x" by (simp add: g_def) with hx show ?thesis by (metis cos_1_lt_1 cos_zero order_less_le) qed

In the proof above, we see a trick for proving continuity. It resembles the trick for taking derivatives, only we hit the goal with a different list of theorems, namely continuous_intros. Then we show the $g$ crosses 0 to prove the existence of a fixed point satisfying $0We proved above that the derivative of $g(x) = \cos x - x$ is strictly negative for $x \in [-1,1]$, i.e. $g$ is strictly decreasing, so $g$ can have at most one zero on that interval. And since $[-1,1]$, is the range of the cosine function, uniqueness over the entire real line immediately follows.

lemma dottie_unique: fixes x y :: real assumes "cos x = x" "cos y = y" shows "x = y" proof (rule ccontr) assume "x ≠ y" have gx: "g x = 0" and gy: "g y = 0" using assms by (auto simp: g_def) show False proof (cases "¦x¦ > 1 ∨ ¦y¦ > 1") case True then show ?thesis by (metis assms abs_cos_le_one not_less) next case False then have "¦x¦ ≤ 1 ∧ ¦y¦ ≤ 1" by simp moreover have "x y ∨ y x" using ‹x ≠ y› by linarith ultimately show ?thesis using DERIV_neg_imp_decreasing [OF _ g_has_negative_deriv] gx gy by force qed qed

More precisely, given the two claimed fixed points, $x$ and $y$, we first trivially establish that both must lie within the interval $[-1,1]$. Then, assuming for contradiction that...

The Dottie Number

Related Articles

US Government directive to suspend access to Fable 5 and Mythos 5

Is AI ruining our skills? Early results are in – and they're not good

The Anatomy of an AI-Native Org

Apertus – Open Foundation Model for Sovereign AI

How to Earn a Billion Dollars