調整ループの有限収束

命題 6.2（「Docker と Kubernetes」§6）・ ✓公理まで証明済み

対象オブジェクトの有限集合を $\mathcal{O}$ （ $|\mathcal{O}| = M$ ）とし、望ましい状態 $d$ と時刻 $t$ の観測状態 $s_t$ に対して、食い違っているオブジェクトの個数

D(s_t) = \#\{o \in \mathcal{O} : s_t(o) \ne d(o)\}

を考えます。次を仮定します。

(A1) 各ループの操作は $(d, s_t)$ のみから決まる（定義 6.1 のレベルトリガ性）。
(A2) $D(s_t) > 0$ ならば、1 回のループで少なくとも 1 つの食い違いが解消され、かつ一致していたオブジェクトが食い違いに転じることはない。
(A3) ループの実行中に外部からの状態変更（ノード故障や $d$ の書き換え）がない。

このとき $D(s_{t+1}) \le D(s_t) - 1$ が $D(s_t) > 0$ である限り成り立ち、高々 $D(s_0) \le M$ 回のループで $s = d$ に到達します。到達後は、(A2) の後半より状態は変化せず、操作は行われません（冪等性）。

さらに (A1) の下では、ループの入力は現在の $(d, s_t)$ だけなので、過去のイベント通知を取りこぼしても、あるいは同じ通知を複数回受け取っても、収束の主張は変わりません。

閉包の状態

✓ 公理まで証明済み

証明が使う定理を前提としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。

証明は Rikai の他の定理を参照していません（定義と論理だけで示されています）。