学習の停止性とマージ回数の上界

命題 4.2（「トークン化」§4）・ ✓公理まで証明済み

コーパス $C = (w_1, \ldots, w_K)$ の総記号数を $N := \sum_{k=1}^{K} |w_k|$ とする。定義 2.3 の学習は、 $m$ の値によらず（ $m$ を上限なしにしても）有限回で終了し、行われるマージの回数 $m'$ は

m' \le N - K

を満たす。

閉包の状態

✓ 公理まで証明済み

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

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

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

ループ変量定義 5.1・契約による設計
マージの適用 1 回の性質✓補題 3.1・トークン化
- 完全帰納法✓定理 4.3・証明の技術
  - 数学的帰納法の原理✓定理 3.2・証明の技術
    背理法の正当性✓命題 6.2・証明の技術
    整列性公理 3.1・証明の技術
- マージ規則とその適用定義 2.2・トークン化
トークン数は増えない✓命題 4.1・トークン化
- マージの適用 1 回の性質✓補題 3.1・トークン化（上で展開済み）
- 符号化と復号の往復✓定理 3.2・トークン化
  - 数学的帰納法の原理✓定理 3.2・証明の技術（上で展開済み）
  - マージの適用 1 回の性質✓補題 3.1・トークン化（上で展開済み）
変量による停止性：全正当性の規則の健全性✓定理 5.2・契約による設計
- 整列性公理 3.1・証明の技術
- 表明への代入定義 3.4・契約による設計

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