--- id: 176 slug: isaacs-full-formalization title: "Isaacs 完全形式化キャンペーン (逐条監査)" created: 2026-08-08 --- # Isaacs 完全形式化キャンペーン (逐条監査) ## 位置づけ [issue 0172](0172-peterfalvi-full-formalization.md) (Peterfalvi 全 284 件) が 2026-08-08 に完了したので、**同じ逐条監査を Isaacs に適用する**。3 冊スコープの文書順 (Isaacs → BG → Peterfalvi) に従い、次は最上流の Isaacs。 方法論は 0172 と同一: > 書籍ページ画像で条項を確定 → repo の statement と突合 → 部分被覆/特殊化/言及のみを補充 ## 実測ベースライン (2026-08-08) ### 書籍側の番号 census `references/isaacs/finite-group-theory.pdftotext.txt` から機械抽出 (⚠ OCR が `T h e o r e m` / `2 . 1 4 .` のように文字・数字を分解するので、**空白許容の 正規表現が必須**。素朴な `^\d+\.\d+\.\s*(Theorem|...)` だと 29 件取りこぼす)。 | 章 | 件数 | 欠番 | |---|---|---| | Ch.1 Sylow | 46 | なし | | Ch.2 Subnormality | 20 | なし | | Ch.3 Split Extensions | 36 | なし | | Ch.4 Commutators | 38 | なし | | Ch.5 Transfer | 30 | なし | | Ch.6 Frobenius Actions | 24 | なし | | Ch.7 Thompson Subgroup | 8 | なし | | Ch.8 Permutation Groups | 44 | なし | | Ch.9 More on Subnormality | 31 | なし | | Ch.10 More Transfer | 28 | なし | | **合計** | **305** | **各章 1..max が連続、欠番ゼロ** | 種別は全件 **Theorem / Lemma / Corollary** (Theorem 135 / Lemma 105 / Corollary 65)。 Definition / Example / Notation は別番号系ではなく同じ連番に混ざらない。 ### repo 側の cite 突合 `OddOrder/**/*.lean` の docstring を grep (`OddOrder/Isaacs/**` は素の `N.M`、それ以外は 同一行に "Isaacs" を要求): | 層 | 件数 | |---|---| | cite あり | **292 / 305** | | **cite ゼロ** | **13** — すべて Ch.8 | cite ゼロ 13 件 = **8.11, 8.12, 8.13, 8.14, 8.15, 8.17, 8.19, 8.20, 8.21, 8.22, 8.27, 8.28, 8.30** = block / primitivity / Jordan set のクラスタ + `Aₙ` 単純性。 ⚠ **cite ゼロ ≠ 未形式化** (0172 の最大の教訓)。実際、**mathlib に `MulAction.IsBlock` / `IsPreprimitive` / `Mathlib/GroupTheory/GroupAction/Jordan.lean` が在り**、 repo の `Ch08_PermutationGroups` も既に `IsPreprimitive` を使っている。⟹ 多くは **mathlib 被覆**の可能性が高く、その場合の正しい対処は CLAUDE.md のラッパー方針どおり 「薄いラッパーを書かず、**対応表を section docstring か `notes/` に記録**」。 ## ⚠ この census が測っていないもの (0172 と同じ) 「cite あり」= 番号が docstring に現れるだけ。番号 grep で検出できない残債: 1. **特殊化債務** — 書籍より狭い仮説で述べている 2. **部分被覆** — (a)(b)(c) の一部だけ / bundled statement が条項を運搬しない 3. **言及のみ** — 散文 cite で statement が無い 4. **mathlib 被覆の未記録** — Isaacs 固有 (Peterfalvi には無かった型)。書籍の結果が mathlib にそのまま在る場合、repo に実体が無くても**被覆済**だが、対応が記録されていないと 監査で「未形式化」に誤分類される ⟹ 本体は番号埋めでなく逐条照合。 ## 作業手順 - [x] **ステップ 1 ✅ 完了 (2026-08-08)**: cite ゼロ 13 件を分類した。対応表の正本 = [`notes/isaacs/ch08_permutation.md`](../../notes/isaacs/ch08_permutation.md)。 | 分類 | 件数 | 内訳 | |---|---|---| | **mathlib 被覆** | **12** | 8.11-8.15, 8.17, 8.19-8.22, 8.27, 8.30 | | **真の未形式化** | **1** | 8.28 → **2026-08-08 に形式化済** (下記) | ⭐ **8.20 は mathlib のほうが一般** — 書籍は「部分群 `H` の軌道 `X` で `H` が原始的、 `|X| > |Ω|/2`」だが mathlib の `IsPreprimitive.of_card_lt` は**任意の同変写像** `f : X →ₑ[φ] Y` で `|Y| < 2·|range f|`。 ⚠ **8.21 は mathlib のほうが狭い** — 書籍は任意の 2 つの Jordan 集合 `X, Y` だが mathlib の `is...ofFixingSubgroup_inter` は 2 つ目を `g • s` (translate) に限定。 消費点 (8.22) は translate 版で足りるので実害は無いが、**mathlib 側の特殊化債務**。 - [x] **8.28 を形式化 (2026-08-08)**。`OddOrder/Isaacs/Ch08_PermutationGroups/SymmetricNormalSubgroups.lean`: ``` center_perm_eq_bot Z(Sym Ω) = 1 (|Ω| ≥ 3) normal_perm_eq_bot_or_alternating_or_top (8.28) 本体 ``` ⚠ `Z(Sym Ω) = 1` も mathlib に無かった (mathlib の `Equiv.Perm.alternatingGroup.center_eq_bot` は**交代群**の中心)。両方 axiom-clean。 - [x] **census note を新設 (2026-08-08)**: [`notes/isaacs/full_formalization_census_2026_08_08.md`](../../notes/isaacs/full_formalization_census_2026_08_08.md) - [ ] **ステップ 2 (進行中)**: Ch.1 から文書順に逐条監査。 - **Ch.1 の第 1 パス完了 (2026-08-08)**: 46/46 に cite あり。docstring の**アンカー位置** (`**Isaacs Thm 1.N**`) に cite が無い 9 件 (1.1, 1.5, 1.6, 1.7, 1.10, 1.11, 1.17, 1.24, 1.25) を調査し、**9 件すべて mathlib 被覆**と確定 (対応表は census note §3)。 - [x] **1.24 の「正規」条項を確定・補充 (2026-08-08)**。書籍 p.24 のページ画像で `L ⊴ P` を確認 ⟹ mathlib は存在しか返さないので**部分被覆**だった。 `Ch01.IsPGroup.exists_normal_card_eq_pow` を追加 (axiom-clean)。 ⚠ **pdftotext では判別不可能** (`⊲` → `<`)。ページ画像が必須だった。 隣の **1.25** は書籍自身が正規性を主張しないので mathlib がそのまま書籍強度 — **隣接する 2 つの系で片方だけ条項が違う**類の差は番号 grep では絶対に出ない。 - ⬜ **残り 37 件の条項ごとの突合は未実施**。とくに 1.12-1.15 / 1.18-1.22 / 1.30-1.31 は **1 つの file-header docstring が複数番号を列挙**しているだけなので、番号ごとの statement の有無を個別確認する (Peterfalvi の「file docstring の散文が定理の代わり」型)。 - **Ch.1 監査完了 (2026-08-08)**: 全 46 件。補充 2 件 (**1.24** の正規条項 / **1.40(ii)** 非単純性)、誤判定 1 件 (1.30(ii)、撤回済)。 - **Ch.2 監査完了 (2026-08-08)**: 全 20 件。補充 1 件 (**2.4** `S ∩ T ⊴⊴ G`)。 ⚠ file-header が実在しない `Subgroup.IsSubnormal.inf` を挙げていたのが検出経路。 ⚠ 2.20 (Lucchini) の本体は owner chapter 規則で **Ch04** に在る。 - **Ch.3 監査完了 (2026-08-08)**: 全 36 件被覆・**補充ゼロ**。訂正は stale な 自己注記 3 件のみ (進捗表「3.11 まで」/ 3.11 の「TODO・新規実装候補」/ 3.23-3.24 の「placeholder ~8-12 週」— いずれも実装済だった)。 - **Ch.4 監査完了 (2026-08-08)**: 全 38 件被覆・**補充ゼロ**。4.9 は mathlib `commutator_commutator_eq_bot_of_rotate`、4.14-4.19 (Mann) は `Mann.lean` の file header が全件対応づけ済、4.33 は `oPiCore_compl_le_oPiCore_compl_of_isPLocal`。 - **Ch.5 監査完了 (2026-08-08)**: 全 30 件被覆。補充 1 件 = **5.26 (Frobenius)** の 書籍どおり 3 条件 TFAE (`frobenius_normal_p_complement_tfae`)。repo は (1)⇔(3) だけを theorem として持ち、条件 (2) は Lemma 5.27 の前後段に分かれていた (Peterfalvi (3.8) と同型の packaging 差)。 - **Ch.6 監査完了 (2026-08-08)**: 全 24 件被覆・**補充ゼロ**。6.18 (3 条項) は 既に書籍の形に束ねた合成定理として名付けられており、6.22/6.24 (Frobenius 核の 冪零性、Thompson) も実体あり。 - **Ch.7 監査完了 (2026-08-08)**: 全 8 件被覆・**補充ゼロ**。7.8 (Burnside `p^a q^b`) は指標を使わない Goldschmidt–Bender–Matsuyama の 9 段証明で `burnside_p_pow_q_pow`。 ⚠ 7.4 は repo が `Isaacs Lem 7.4` と略記しており grep パターンが取りこぼした。 - **Ch.9 監査完了 (2026-08-08)**: 全 31 件被覆・**補充ゼロ**。9.21 (Schenkman)、 9.23 (Thompson の corefree bound)、9.24 (Thompson–Wielandt) とも endpoint あり。 - **Ch.10 監査完了 (2026-08-08)**: 全 28 件被覆・**補充ゼロ**。10.28 (Alperin–Kuo) まで実体あり。⚠ この章の注記は日付つき (2026-07-17) で実体と一致していた (**stale でない自己注記の実例**)。 - **⟹ ステップ 2 完了。Ch.1-Ch.10 の全 305 件を逐条監査した。** ## 完了条件 — **達成 (2026-08-08)** > Isaacs の全 305 件が **書籍強度**の Lean statement を持つか、**mathlib 被覆として対応が > 記録されている**。特殊化債務ゼロ・部分被覆ゼロ。各章の監査結果を census note に記録する。 **Ch.1-Ch.10 の全 305 件を逐条監査した。** | 章 | 件数 | 補充 | stale 注記の訂正 | |---|---|---|---| | Ch.1 Sylow | 46 | **2** (1.24 正規条項 / 1.40(ii) 非単純性) | 2 | | Ch.2 Subnormality | 20 | **1** (2.4 `S ∩ T ⊴⊴ G`) | 1 | | Ch.3 Split Extensions | 36 | 0 | 3 | | Ch.4 Commutators | 38 | 0 | 0 | | Ch.5 Transfer | 30 | **1** (5.26 Frobenius 3 条件 TFAE) | 1 | | Ch.6 Frobenius Actions | 24 | 0 | 0 | | Ch.7 Thompson Subgroup | 8 | 0 | 0 | | Ch.8 Permutation Groups | 44 | **1** (8.28 `Sₙ` の正規部分群) | 0 | | Ch.9 More on Subnormality | 31 | 0 | 0 | | Ch.10 More Transfer | 28 | 0 | 0 | | **合計** | **305** | **5** | **7** | 補充した 5 件はすべて axiom-clean で AxiomsCheck 登録済。 節別の詳細は [census note](../../notes/isaacs/full_formalization_census_2026_08_08.md) §3 が正本。 ### ⚠ Isaacs 監査で最も多かった問題 — 自己注記の腐り **補充 5 件に対し stale 注記の訂正が 7 件**。Peterfalvi 監査 (issue 0172) では 「未形式化と記録されていたが既に在った」が 9 件だったが、Isaacs では**書き手自身の 進捗記録が実体から乖離している**のが主因だった: * Ch.1 の進捗表が全節「TODO」(章は広範に実装済) * Ch.2 が**実在しない補題名** `Subgroup.IsSubnormal.inf` を挙げていた * Ch.3 の 3.23/3.24 が「placeholder」「~8-12 週の大規模」(全 4 条項実装済) * Ch.5 が「Lem 5.27, 5.28 **完成後**の theorem 化を参照」(同ファイル下部に実体) ⟹ **注記は当たりを付ける道具であって判定の証拠ではない**。ただし Ch.10 のように 日付つきで実体と一致している注記もあるので、無視するのも誤り。 ### Isaacs 特有だった残債型 — mathlib 被覆の未記録 標準的な有限群論の章 (Ch.1 / Ch.8) では**書籍の結果が mathlib にそのまま在る**ことが多く、 repo に実体が無くても被覆済。Ch.8 の cite ゼロ 13 件のうち **12 件がこれ**だった。 対処は CLAUDE.md のラッパー方針どおり「薄いラッパーを書かず対応表を記録」。 ### 残る作業 なし。次フロンティアは **BG** (Bender–Glauberman) の逐条監査 (3 冊スコープの最後)。 ## 参照 - 前身: [issue 0172](0172-peterfalvi-full-formalization.md) (Peterfalvi、完了) - 書籍: `references/isaacs/finite-group-theory.pdf` (⚠ **PDF ページ = 書籍ページ + 13**)、 ページ画像は `references/isaacs/pages/` - ⚠ 誤判定様式は 0172 で 9 件検出済 — 番号表記の揺れ / assembly を endpoint と誤認 / stale な自己注記の連鎖。**自分の過去の「未形式化」ラベルを一次証拠にしない**。