指示ファイルの連結順の一意性と、取り込みの展開の停止

命題 4.2（「文脈を保つ・減らす・分ける」§4）・ ✓公理まで証明済み

作業ディレクトリへの道をルートから順に $D_0, D_1, \ldots, D_k$ （ $D_k$ が作業ディレクトリ）とし、ファイルの種類を $j \in \{0, 1\}$ （ $0$ は CLAUDE.md、 $1$ は CLAUDE.local.md）とする。見つかったファイルの集合 $M \subseteq \{0, \ldots, k\} \times \{0, 1\}$ に対し、「ルートから作業ディレクトリへ、同じディレクトリでは種類 $0$ が先」という規則は $M$ の上の全順序を定める。したがって連結の結果は、 $M$ と各ファイルの内容だけで一意に決まり、ファイルを見つけた順序に依らない。
取り込みの深さの上限を $h$ 、1 つのファイルに書ける取り込みの数の上限を $b \ge 1$ とする。取り込みを「深さが $h$ のファイルの取り込みは展開しない」という規則で展開すると、取り込みが循環していても展開は停止し、展開で読まれるファイルの数（重複を含めて数える）は 1 つの指示ファイルにつき高々 $\sum_{j=0}^{h} b^j$ である。

閉包の状態

✓ 公理まで証明済み

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

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

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

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