2026-07-04 学習ログ

Royal Road to Topology の残作業プラン Phase 0〜I を立案し issue 化した日。今回から issue に難易度・推奨モデルを付与し、着手時にモデルをルーティングする仕組みを導入（Phase 0 / issue #10）。

やったこと

残作業プランを 10 個の issue に分割（トラッキング #20 でピン留め）:
- Phase 0 #10: モデルルーティング整備（本日実施・完了）
- Phase F #11: 演習選別 VII〜X（sonnet）→ Phase G #12・#13: 演習解答 VII・VIII / IX・X（opus）
- Phase H #14〜#17: 🎯本命章カード化 XII・XV・XXII(§9)・XXIV（sonnet）
- Phase I #18: Lean 第I・II章の残り（opus）、#19: Lean 第VII〜X章（fable）
Phase 0 の中身:
- ラベル新設: model:haiku|sonnet|opus|fable（Agent ツールの model パラメータ値と一致）＋ difficulty:1〜3 ＋ meta
- .github/ISSUE_TEMPLATE/agent-task.md に「難易度・推奨モデル」節を追加（5 節構成に）
- skills/plan-to-issues/SKILL.md の着手手順にステップ 0 を追加: model:* ラベルと現セッションのモデルが不一致なら、Agent ツールでそのモデルのサブエージェントに issue を丸ごと委譲する
マイルストーン「🎯ターゲット章（XII・XV・XXII・XXIV）」を新設し Phase H を割当。

内容レビューで発見していた「第II章の命題カードが空振りする証明ポインタ `証明 → [[chapter2]]` だけ持つ」問題に対処。書籍第II章 PDF（chp2）を出典に、対象17枚それぞれへ「証明の骨子」（3〜8行）を追記し、空振りポインタを全削除。
- II.1: prop-ii-1-1（収束⟺$\mathcal{N}(x)\subset\Gamma_\varphi$）・lem-ii-1-4（$\Gamma_\varphi\subset\Gamma_\psi$⟺相関が cofinite 保存）
- II.2: prop-ii-2-2（基底の内在的特徴づけ）・2-6（補有限フィルターの適切性）・lem-ii-2-8（自由⟺$\supset(X)_0$）・cor-ii-2-12・prop-ii-2-13/14（自由性・主性のファイバー判定）・2-19（指標）・2-21（可算補有限は列型・自由）・2-22（${A}^\uparrow$ 列型⟺$A$ 可算）
- II.3: prop-ii-3-2（完備束）・3-4（主フィルターの inf）・3-5（主フィルターの sup）・3-6（自由フィルターの inf）・3-7（可算基底⟹列型の inf）・3-10（ウルトラの二分性）
- II.5: prop-ii-5-9/10（subcofinite の標準形 $(B,A)_0$・almost equal 基底）
証明中で他カードの結果を使う箇所は `[[cards/topology/…]]` でリンクし重複記述を回避（lem-ii-2-8→prop-ii-3-6、cor-ii-2-12→prop-ii-2-22、prop-ii-3-2 の inf＝共通部分を prop-ii-3-4/3-6 で再利用等）。

難易度→モデルの割当方針を明文化した: 1=定型・抽出→haiku/sonnet、2=判断あり・前例あり→sonnet、3=数学的証明・Lean→opus/fable（mathlib 形式化は fable）。演習解答（証明を実際に解く）と Lean が難易度 3、選別・カード化は前例が確立しているので難易度 2 に収まる。
issue #22 の「前提」に列挙された対象カード一覧は起票時スナップショットで、実リポジトリと3枚ズレていた（cor-ii-1-2・prop-ii-2-10 は既に証明有 or ポインタ無で対象外、lem-ii-1-4 が対象追加）。着手時に `grep -rl` で実態を再確認し issue コメントで訂正してから作業した——SKILL.md の「着手時の検証を省略しない」を実践。
旧トラッキング #9 は全子 issue クローズ済み。クローズは権限の都合で保留（手動クローズ待ち）。