情報科学 › Claude Code の中身 › 拡張の仕組み
SDK のループへの停止性の適用
Agent SDK で組んだループが、上の対応表のとおりに 第 1 章 の模型の実例であるとする。max_turns を有限の値 に設定すると、そのループのモデルの呼び出しは高々 回で、ループは停止する。max_turns を設定しない（上限なし）場合、模型の上では停止は保証されない。
閉包の状態
✓ 公理まで証明済み
証明が使う定理を 前提 としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 4 件、定義なども含めて 7 件）。
印の意味: ✓公理まで証明済み ・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は 閉包の状況。
前提をたどる 証明が使う定理・定義（直接 1 件）
▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。
ターン上限つきループの停止と呼び出し回数の上界✓定理 4.1・エージェントループ
- ループ変量定義 5.1・契約による設計
変量による停止性：全正当性の規則の健全性✓定理 5.2・契約による設計
これを使っている定理
証明で明示的に参照している定理は、まだありません。