情報科学 › Claude Code の中身 › エージェントループ
ループは対応の不変条件を保つ
定義 3.1 の模型で、モデル ・ツールの実行・関門 ・上限 が何であっても、初期状態から到達できるすべての状態 で、 は を満たす。特に、モデルの呼び出し に渡されるメッセージ列は、つねに を満たす。
閉包の状態
✓ 公理まで証明済み
証明が使う定理を 前提 としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 3 件、定義なども含めて 5 件）。
印の意味: ✓公理まで証明済み ・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は 閉包の状況。
前提をたどる 証明が使う定理・定義（直接 2 件）
▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。
- データ型の実装・表現不変条件・抽象化関数定義 6.1・契約による設計
表現不変条件の帰納法✓定理 6.2・契約による設計
これを使っている定理 証明で参照している 3 件
- 拒否された呼び出しもループを止めない✓命題 3.5・エージェントループ
- エラーを結果として返すと、ループの不変条件が保たれる✓命題 3.7・拡張の仕組み
- フックの実行はモデルの出力に依らない✓命題 4.5・拡張の仕組み