ドッティ数
本記事では、方程式 cos(x) = x の不動点として定義される数学定数「ドッティ数」について解説する。この数の発見の経緯、数値近似（約0.739085...）、そしてその美しい反復的性質について掘り下げる。
背景メモ
- 「Dottie数」（約0.739085…）は、方程式 cos(x) = x を満たす唯一の実数。関数cosを何度も反復適用すると、初期値によらずこの値に収束する性質を持つ。
- 名称は、この現象を発見した女性数学教師 Dottie（本名不明）に由来。1980年代の「フラクタル探検隊」コミュニティなどで話題になった。
- この数の面白さは、三角関数cosが「自分自身を入力として再帰的に呼ぶ」不動点である点。超越方程式なので閉じた代数式で書けず、数値的にしか求められない。
- 本記事は、関数型プログラミング言語（おそらく Isabelle/HOL）を用いてこの数の存在と一意性を定理として証明する過程を解説。高階関数・反復適用・不動点定理などの概念が背景にある。