情報科学 › Claude Code の中身 › エージェントループ

呼び出し回数：ワークフローは定数で、エージェントは上限なしには有界でない

命題 7.2（「エージェントループ」§7）・ ✓公理まで証明済み

節点の集合が $V$ のワークフローの、1 回の実行でのモデルの呼び出し回数は、入力にもモデルにも依らず $|V|$ 以下である。
上限のない（ $T = \infty$ ）エージェントでは、任意の $K \ge 1$ に対して、モデルの呼び出しがちょうど $K$ 回になるモデルが存在する。したがって、呼び出し回数を入力にもモデルにも依らずに抑える定数は存在しない。
上限 $T$ が有限のエージェントの呼び出し回数は $T + 1$ 以下で、モデルをわたる上限はちょうど $T + 1$ である。

本文で読む（証明と前後の説明）→

閉包の状態

✓ 公理まで証明済み

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

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

前提をたどる証明が使う定理・定義（直接 1 件）

▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。

ターン上限つきループの停止と呼び出し回数の上界✓定理 4.1・エージェントループ
- 数学的帰納法の原理✓定理 3.2・証明の技術
  - 背理法の正当性✓命題 6.2・証明の技術
  - 整列性公理 3.1・証明の技術
- ループ変量定義 5.1・契約による設計
- 変量による停止性：全正当性の規則の健全性✓定理 5.2・契約による設計
  - 整列性公理 3.1・証明の技術
  - 表明への代入定義 3.4・契約による設計

これを使っている定理

証明で明示的に参照している定理は、まだありません。