情報科学 › Claude Code の中身 › 文脈を保つ・減らす・分ける
圧縮とキャッシュ
圧縮の直前の要求をトークン列 ( は会話より前の層、 は会話の層)とし、 の末尾までがキャッシュに書かれているとする。
- 要約を作る要求が ( の末尾に要約の指示 を足したもの)の形なら、 はその接頭辞で、キャッシュが有効期間内なら の末尾のブレークポイントに命中する。前章の模型のとおり、新しく足した部分を末尾のブレークポイントまで書き込むとすると、このときの入力コストは 、有効期間が切れていれば である。
- 圧縮のあとの要求を ( は要約、 は新しい追記)とする。 と の最初に食い違う位置より後ろにあるブレークポイントは、どれも命中しない。 なら の末尾までのブレークポイントは命中しうるが、 なら、食い違う位置より後ろはすべて命中しない。
閉包の状態
✓ 公理まで証明済み
証明が使う定理を 前提 としてたどると、Rikai の中の証明だけで定義・公理(物理では基本仮定)までつながっています(前提の定理類 2 件、定義なども含めて 2 件)。
印の意味: ✓公理まで証明済み ・ △証明あり(閉包未完)・ ※主張のみ。テーマごとの集計は 閉包の状況。
前提をたどる 証明が使う定理・定義(直接 2 件)
▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。
- 追記だけの会話の入力コスト✓定理 4.2・コンテキストウィンドウとプロンプトキャッシュ
- 位置 j の変更は j 以降を無効にし、j より前は影響を受けない✓命題 3.3・コンテキストウィンドウとプロンプトキャッシュ
これを使っている定理
証明で明示的に参照している定理は、まだありません。