--- id: 177 slug: bg-full-formalization title: "BG 完全形式化キャンペーン (逐条監査)" created: 2026-08-08 --- # BG 完全形式化キャンペーン (逐条監査) ## 位置づけ 3 冊スコープ (Isaacs / BG / Peterfalvi) の逐条監査の**最後**。 | 書籍 | 件数 | 状態 | issue | |---|---|---|---| | Peterfalvi | 284 | ✅ 完了 (補充 ~20、誤判定 9) | [closed/0172](0172-peterfalvi-full-formalization.md) | | Isaacs | 305 | ✅ 完了 (補充 5、stale 注記訂正 7) | [closed/0176](0176-isaacs-full-formalization.md) | | **BG** | 下記 | ⬜ **本 issue** | 0177 | 方法論は 0172 / 0176 と同一: > 番号の参照地図で当たりを付ける → file header の対応表と `theorem` 一覧で実体確認 > → 書籍ページ画像で条項確定 → 部分被覆/特殊化/packaging 差を補充 ## ⚠ BG は番号体系が前 2 冊と違う Isaacs / Peterfalvi は `N.M.` を行頭に置く形式だったが、**BG は 2 系統ある**: 1. **`(N.M)` を単独行に置くラベル** — これは**証明内の主張ラベル**であって定理番号ではない。 例: §3 の証明中に `(3.6)` `(3.7)` `(3.8)` が並び、後段が「by (3.6)」と参照する。 ⚠ **これを定理番号と取り違えると件数が数倍に膨らむ**。 2. **`Kind N.M.` / `Kind N.M (帰属).`** — こちらが**番号付き結果**。 `Theorem` / `Proposition` / `Lemma` / `Corollary` の 4 種。 さらに BG は **Theorems A–E** (章番号を持たない主定理) と **Appendix A–E** を持つ。 ## 実測ベースライン (2026-08-08) `references/bg/local-analysis.pdftotext.txt` から機械抽出。 抽出パターン (⚠ `N.M.K` 形は Gorenstein の引用なので除外する): ```python pat = re.compile(r'^(Theorem|Proposition|Lemma|Corollary)\s+(\d{1,2})\.(\d{1,2})(?!\.\d)\s*(\(|\.)', re.M) ``` | 節 | 件数 | 欠番 | |---|---|---| | §1 | 22 | なし | | §2 | 7 | なし | | §3 | 10 | なし | | §4 | 19 | ⚠ 4.1 (OCR で header 行が崩れている。本文中には `Lemma 4.1` の引用あり) | | §5 | 7 | なし | | §6 | 7 | なし | | §7 | 5 | ⚠ 7.1 (同上) | | §8 | 1 | — | | §9 | 6 | なし | | §10 | 14 | なし | | §11 | 7 | なし | | §12 | 19 | なし | | §13 | 13 | なし | | §14 | 12 | ⚠ 14.11 | | §15 | 9 | なし | | §16 | 1 | — | | **小計** | **159** | 欠番 3 (いずれも OCR 由来、実在は本文引用で確認済) | 種別内訳: Theorem 71 / Lemma 69 / Proposition 35 / Corollary 34 (重複カウント込み — 章頭の再掲があるため)。 **補章**: `Kind X.N` (X ∈ A-E) が **15 件**。 ⬜ **要確定**: (a) 欠番 3 件の実際の statement (ページ画像で確認)、 (b) Theorems A-E の扱い、(c) 補章の正確な件数。 ## ⚠ この census が測っていないもの (0172 / 0176 と同じ) 1. **特殊化債務** — 書籍より狭い仮説 2. **部分被覆** — 多条項の一部だけ / TFAE の条項数不足 3. **packaging 差** — 条項はすべて在るが書籍の statement の形になっていない 4. **mathlib 被覆の未記録** — Isaacs で主役だった型。BG は FT 固有の内容が多いので 前 2 冊より少ないと予想されるが、§1 (Preliminary Results) は標準的な有限群論なので要確認。 ## 作業手順 - [x] **ステップ 1 (大半完了、2026-08-08)**: 欠番 3 件のうち **2 件を解決**。 - **7.1** — OCR が `L e m m a 7.1.` と**文字分解**。空白許容パターンで解決。 - **4.1** — OCR が `Lemma-4.1.` と**ハイフン**を入れており空白許容でも漏れる。 ⟹ §4 は 20 件。 - ✅ **14.11 解決 (2026-08-08、ページ画像不要)** — header `Lemma 14.11.` が **前段落の最終行の末尾に貼り付いていた** (`…related to those of type 𝓜₂ Lemma 14.11. Suppose that…`) ため、行頭アンカー `^\s*(Kind)` では原理的に取れなかった。 非アンカー版で BG 全文を再走査した結果 **この 1 件だけ**が漏れており、 ⟹ **§14 = 13 件、§1-§16 の総数は 162 件で確定**。 ⚠ **誤判定様式**: 「欠番」を見つけたら**ページ画像より先に非アンカー再走査**をやる。 - **Theorems A–E**: 5 件すべて所在確認 (`Theorem A` L6615 / `B` L6602 / `C` L6653 / `D` L6669 / `E` L6692)。⚠ `Theorem B.4` (補章 B) と混同しないこと。 - **補章**: `Kind X.N` が 14 件。⬜ 各補章の `.1` が未発見で要確認。 - [x] **census note を新設 (2026-08-08)**: [`notes/bg/full_formalization_census_2026_08_08.md`](../../notes/bg/full_formalization_census_2026_08_08.md) - [ ] **ステップ 2 (進行中)**: §1 から文書順に逐条監査。 - **§1 監査完了 (2026-08-08)**: 全 22 件被覆・**補充ゼロ**。 ⚠ **stale 注記 2 件を訂正** — `S01_FrattiniBurnside.lean` の対応表が Thm 1.8 と Thm 1.11 を「**Phase 1 待ち**」のまま残していた (どちらも実装済)。 🚨 とくに **1.8 は同一ファイル内で矛盾**していた (:63 が「Phase 1 待ち」、 :152 が「⭐ sorry-free」)。 ⚠ **1.11 は Isaacs 側のディレクトリに在る** (owner chapter 規則、通算 4 回目)。 - **§2 監査完了 (2026-08-08)**: 全 7 件被覆・**未形式化ゼロ**。 補充 = **packaging 差 1 件** (Lem 2.7 の群形 `elemAbelian_aut_action_group`)。 ⚠ **自己訂正**: 本 issue は一度「Lem 2.7 = §1-§2 で唯一の真の未形式化」と **誤判定した**。実体は 2 系統・独立に 2 回 (issue **0150** と **3009**、 いずれも close 済) 形式化されており、`AxiomsCheck.lean` には 「**BG Lemma 2.7(a)/(b)**」と明示コメント付きで登録されていた。 ⚠ **stale 注記 4 件を訂正** (`S02_RepresentationsBasic.lean` の Lem 2.3 / Prop 2.4 / Thm 2.5 の「stub 未配置」+ 「全 6 結果」という件数)。 - **§3 監査完了 (2026-08-08)**: 全 10 件被覆・**未形式化ゼロ**。実収穫 3 件: 1. **特殊化債務 2 件** (Lem 3.2 / Thm 3.5 — どちらも**書籍自身の Note** が 「`K` が可解という仮説は不要」と書いているのに repo が `IsSolvable ↥K` を 持っていた。Thompson は repo に在るので discharge 可能)。 ⟹ `S03_WithoutSolvableKernel.lean` (`bgLemma32` / `bgThm35`)。 2. **部分被覆 1 件 = Thm 3.10 の (a)** — capstone `bgThm310_nilpotent` は (b)+(c) しか 返しておらず、(a) は module leaf 止まりだった。docstring は「(a) は elsewhere」と 書いていたがその実体は**可換 kernel 専用**で書籍の (a) を満たさない。 ⟹ (a) を dévissage に通し、書籍パッケージ `S03g.bgThm310` を新設。 3. **BG の大域規約 2 本を確定** (下記 ⚠)。 ⚠ **Lem 3.1 の条項 (b) は pdftotext が丸ごと落としていた** — ページ画像 `references/bg/pages/bg-p017.png` (PDF = 書籍 + 13) で `C_K(x) = 1 (x ∈ R^#)` と確定。 ✅ **Prop 3.9 は書籍より強い** (書籍の「`H` は `p'`-群」を落としている)。 - **§4 監査完了 (2026-08-08)**: 全 20 件被覆・**未形式化ゼロ**。 (4.1 のみ mathlib 被覆 `commutative_of_cyclic_center_quotient`。)実収穫 2 件: 1. **部分被覆 2 件 = Thm 4.12 の (a) 一般形と (b) 積分解**。repo の (a) は `[R,A] = R` の特殊形のみ、(b) は交わり `[R,A] ∩ C_R(A) = 1` のみで書籍の `R = [R,A]·C_R(A)` を欠いていた。⚠ **どちらも証明の内部には既に在った** ((a) の一般形は (b) の証明が冒頭 8 行で、積分解は (c) の証明が Prop 1.6(a) で)。 ⟹ `S04b.isMulCommutative_actionCommutator` + 書籍パッケージ `S04b.bgThm412`。 2. **stale 注記 3 件** (Prop 4.3 の「remain to be assembled」+ 存在しない名前、 Lem 4.5(a) の「normality deferred」「一般の場合は deferred」)。 ✅ **書籍より強い形が 3 件** — 4.15 (`p` 奇を落として `p`-一般) / 4.17 (`A` 可解を落とす) / 4.20(a) (「`G'` 冪零」でなく `G' ≤ F(G)`)。 ⚠ **4.20 の 3 条項は S04 でなく S05 に在る** (owner chapter、BG で通算 6 回目)。 - **§5 監査完了 (2026-08-08)**: 全 7 件被覆・**未形式化ゼロ**。実収穫 2 件: 1. **packaging 差 1 件 = Thm 5.3**。書籍は「同値 + narrow のときの (a)(b)(c)(d)」で 1 つの結果だが、repo は (a)(b)(c) を `lemma52` (= Lem 5.2) 経由でしか取れず、 `lemma52` は `E ∈ ℰ²∩ℰ*` を明示引数に要求していた (「narrow ⟹ `E` 存在」を 挟む一手が endpoint に無い)。⟹ `S05.bgThm53` を新設。あわせて (a) を書籍どおり **全称形** (「no element of ℰ²∩ℰ*」) にし、(c) の characteristic 半分 (別 file の instance) を明示した。 2. **stale 注記 1 件** (`S05_NarrowSCN.lean` の「still-deferred general Lemma 4.5(a)」 — §4 監査で無条件形の実在を確定済)。 ✅ 5.2 / 5.5 / 5.6 は多条項が既に 1 statement に揃っていた ((a)(b)(c) / (a)(b)(c) / (a)-(e))。 - **§6 監査完了 (2026-08-08)**: 全 7 件被覆・**未形式化ゼロ**・**stale 注記ゼロ** (BG で初)。 実収穫 = **packaging 差 1 件** (Lem 6.3(a) の 2 条項が分かれており、同じ節の (b) が `lemma63b` として束ねられているのと非対称) ⟹ `S06.lemma63a`。 ✅ **Thm 6.2 は書籍の両版を持っていた** — AxiomsCheck の登録コメントは Puig `L(S)` 版を 「BG Thm 6.2 一般形」と呼ぶので literal `J(S)` 版が無いように読めるが、 `S06_Thm62JS.lean` が 2026-07-21 に無条件で完成させている。 📌 **6.7 の Remark は特殊化債務でない** — 「`p`-length one は Thompson の定理により不要」 と書くが、その Thompson は**外部文献 [18]** で 3 冊スコープ外 (BG 自身も証明を書いていない)。 §3 の Lem 3.2 / Thm 3.5 とは逆のケース (あちらの Thompson は repo に在った)。 - **§7 監査完了 (2026-08-08)**: 全 6 件被覆・**補充ゼロ** (未形式化 / packaging 差 / stale 注記がすべてゼロ — BG で初)。Thm 7.4 は (a)(b)(c)(d)、Prop 7.5 は両分岐 (1)(2) が 既に 1 statement に揃っていた。 ⚠ **Hypothesis 7.1(2) の式を pdftotext が丸ごと落としていた** (Lem 3.1(b) と同じ型)。 ページ画像 `references/bg/pages/bg-p056.png` で `⟨ℋ_X(A;π')⟩ = O_{π'}(X)` と確定 — repo の `Hypothesis71.generated_eq` と完全一致。 ⟹ **番号付き結果だけでなく Hypothesis の定義文も OCR 落ちの危険がある**。 - **§8 監査完了 (2026-08-08)**: 番号付き結果は **Thm 8.1 の 1 件のみ** (2 条項)、 両方 AxiomsCheck 登録済。**補充ゼロ**。 - **§9 監査完了 (2026-08-08)**: 全 6 件被覆・未形式化 / packaging 差 / stale 注記ゼロ。 Thm 9.1 は書籍の (a)/(b) を選言で保持、Thm 9.6 の **"In particular" 条項**も独立の public theorem になっていた (前 2 冊で誤判定様式だった型を回避できている)。 🔴 **実収穫 = §9 が AxiomsCheck に 1 件も登録されていなかった**。数学は全部在ったが、 本監査が第 1 手に置く索引 (CLAUDE.md が「書籍番号 ↔ Lean 実体の最良の索引」と 位置づける) に **Uniqueness Theorem という第 II 章の主結果が無い**状態だった。 ⟹ 7 件 (9.1-9.6 + "In particular") を登録し、**全て axiom-clean を確認**。 ⚠ 「AxiomsCheck に無い ⟹ 未形式化」ではない (§9 が反例)。索引の欠落は **索引の欠陥**として直す。 - **§10 監査完了 (2026-08-08)**: 全 14 件被覆・未形式化ゼロ。 実収穫 = **packaging 差 2 件**: 1. **Thm 10.2 の (d)** (`r(M/M_α) ≤ 2` かつ `M'/M_α` nilpotent) が束から落ちていた。 docstring は「追加予定」と書いていたが stale で、(d) 自体は形式化済だった。 ⟹ `S10.bgThm102` (5 条項)。 2. **Prop 10.11 の (d)** が束から分離。(d) の仮説は (a)(b)(c) への追加なので 書籍どおり含意として束ねられる ⟹ `S10.bgProp1011`。 📌 **束ねない判断を 2 件** (10.9 / 10.14) — 条項ごとに仮説が別物 (共有は `M ∈ ℳ` だけ、 あるいは (d) だけが `M` を参照)。**判断基準を確立**: 条項が statement の仮説を共有する (追加の側条件は可) なら束ねる / 書籍が番号だけを共有する別々の主張なら束ねない。 ⚠ **ページ画像で α/σ を確定** — pdftotext は α と σ を判別不能に潰す。Lem 10.4 は (a)(b)(c) とも **σ(M)** (`references/bg/pages/bg-p074.png`; 同ページに Lem 10.3 = α(M)'、 Lem 10.5 = σ(M)' も並ぶ)。 ✅ 10.1 と 10.7 は **5 条項が既に 1 statement** に揃っていた。 - **§11 監査完了 (2026-08-08)**: 全 7 件被覆・未形式化ゼロ。 実収穫 = **packaging 差 1 件** (Cor 11.6 の (c) が (a)(b) 束から別置き。 Hypothesis 11.1 以外に仮説を持たない = 完全共有なので §10 で確立した基準では 束ねるべき) ⟹ `S11.bgCor116`。 📌 §11 は書籍の standing hypothesis (Hypothesis 11.1) を `Hypothesis111` という **structure** にしてあり、7 結果すべてがそれを取る — §7 の `Hypothesis71` と同じ設計。 - **§12 監査完了 (2026-08-08)**: 全 19 件被覆・未形式化 / packaging 差 / 特殊化債務ゼロ。 **BG 最大の節だが最も整っていた** — Lem 12.1 は **(a)-(g) の 7 条項**、Thm 12.5 は **(a)-(f) の 6 条項**が既に 1 statement。全 21 file が実 sorry ゼロ。 実収穫 = **stale 注記 2 件** (`S12_E.lean` の「Lane proof-gate notes」= 後続セッションが 真っ先に読むヘッダに、Thm 12.12 の `Z_p` 構成と Cor 12.16(b) を「deferred」と記載。 どちらも完全証明済)。 ✅ 「`q`-group **specialization**」と自称する docstring があったが、一般 `σ(M)`-部分群形が 同じファイルに在り債務でなかった — **「specialization」の語を見たら一般形の有無を確認**。 - **§13 監査完了 (2026-08-08)**: 全 13 件被覆・未形式化 / packaging 差 / stale 注記ゼロ。 多条項がすべて 1 statement (13.1/13.2 (a)(b)(c)、13.10 (a)(b)(c)、13.11 (a)(b)(c)(d))。 📌 13.10/13.11 の docstring は「結論は PDF から**画像読みで復元**」と明記 — OCR が 結論を落とす箇所で既にページ画像運用がされていた。 - 🚨 **§13 で deferral 注記の一括走査を実施し、見落としを 2 件回収**: 1. **Lem 10.8(c) の「最大素因子」条項** (§10 の見落とし)。Thm 10.2(d) と完全に同型で、 「quotient 型整備後に追加予定」という言い訳まで同じ。条項自体は直下で証明済。 ⟹ `S10.bgLem108`。 2. **`S02_RepresentationPropositions.lean` の「stub 未配置」4 件** (§2 の見落とし。 §2 監査は同じ節の**別ファイル**しか直していなかった)。 - **§14 監査完了 (2026-08-08)**: 13 件すべてに endpoint あり。 🔴🔴 **BG 監査で唯一の「真の未形式化」を確認** — Prop 14.2 の **(a) 後半** (`K` が abelian Hall `(κ∪σ)'`-部分群 `U` に regular 作用 / `U M_σ` が normal complement) と **(g) 第 3 主張** (`M_σ` が nilpotent)。 ⟹ [issue 0178](0178-bg-prop142-regular-u-and-nilpotent-msigma.md) を起票。 ⚠ 下流 `AppE_*` は `M_σ` 冪零を**仮説 `hMσnil`** として取っており、閉じれば実証明に 置換できる (hard content の仮説 hoist)。 ⚠ **`typeP_structure` の docstring は 7 項目を "deferred" と列挙していたが、そのうち 4 件は既に別宣言で証明済だった** ⟹ **注記を根拠に「未形式化」と書かない。 概念形 grep で不在を確認してから初めて gap と呼ぶ**。 ✅ Thm 14.7 は (b)-(h) を `∃!` で束ね (a) を別宣言に持つ — 全条項あり。 - **§15 / §16 監査完了 (2026-08-08)**: 全 10 件被覆・未形式化 / packaging 差ゼロ。 条項ラベル付き endpoint が非常に密 (Lem 15.1 は (a)-(e)、Thm 15.7 も (a)-(e))。 実収穫 = **stale 注記 2 件** — Cor 15.5(c) の後半 (`M'/M_F` nilpotent) を 2 箇所が 「deferred — quotient API」と書いていたが、実体は §16 の `derivedInG_quotient_maxNilpotentNormalHall_isNilpotent` に在った。 ⚠ ただし証明が **§16 (下流)** なので §15 の束には入れられない (import cycle)。 注記を「証明済だが層の都合で別位置」に訂正 (bundle はしない)。 📌 **「quotient 型 API 整備後に追加予定」は BG で 3 回出て 3 回とも stale** (Thm 10.2(d) / Lem 10.8(c) / Cor 15.5(c)) ⟹ **この文言を見たら即座に実体を探す**。 - **補章 A-E 監査完了 (2026-08-08)**: **census を 14 件 → 19 件に訂正** (A:5 / B:4 / C:3 / D:2 / E:5)。全件 repo に実体あり。 ⚠ 「各補章の `.1` が未発見」の原因は **OCR が数字 `1` を大文字 `I` に化かす** (`Theorem A.I.` / `Lemma B.I.` …)。B.4 / E.3 が漏れていたのは **帰属の括弧が番号直後に入る**ため (`Theorem B.4 (L. Puig, 1976).`) — 本文節の パターンは既に `(` を許していたのに補章用パターンだけ許していなかった。 ✅ 補章 D は de-opacification の模範例 (free `Prop` フィールドで D.1/D.2 が 全 odd CN-群について主張される形になっており、その読みでは両方偽 — 反例まで docstring に記録済)。 - **Theorems A-E の位置と性格を確定 (2026-08-08)**: ⚠ 本 issue の baseline が記録した行番号 (A=L6615 等) は**依存関係の図のラベル**だった。 本文は §16 内の L6479 (A) / L6509 (B) / L6516 (C) / L6532 (D) / L6554 (E)。 性格 = §10-§15 の結果の**要約**で、各条項が既出の番号付き結果の言い換え。 🔴 **Theorem A の逐条対応を実施した結果、issue 0178 の gap が Theorem A(3)(4) そのものだと判明** — 周辺的な条項ではなく BG 主定理の条項。 ⟹ **0178 の優先度を上げる根拠**。 - **Theorems A-E 監査完了 (2026-08-08)**: **書籍自身が依存図で対応表を与えていた** (L6571-6573「their "proof" can be given **schematically**」+ L6575-6675 の図)。 A(1)←Thm 10.2(b) / A(2)←Lem 15.1(a) / A(3)(4)(5)←Prop 14.2(a)(b)(c) / A(6)(7)(8)←Thm 15.2(a)+Cor 15.5+Thm 15.7(a)(b) / B(1)←Lem 12.1(d) / B(2)-(5)←Thm 12.5(b)+Lem 15.1(c)(d)(e) / C(1)-(3)←Cor 14.12+Cor 15.6+Lem 15.1(b) / C(4)(5)←Thm 10.1(b)+Thm 14.7(a)(b)(c)+Prop 14.2(c) / C(6)(7)(8)(11)←Thm 14.7(d)(e)(f)(g)+Prop 14.2(d) / C(9)←Thm A(3)(5)+Prop 14.2(g)+Thm 15.7(a) / D(1)←Cor 15.3(b) / D(2)←Lem 12.17 / D(3)(4)←Thm 14.4(b)+Thm A(8)+Cor 15.9 / E(1)←Lem 14.5(c) / E(2)←Thm 13.9 / E(3)←Cor 14.9。 ⟹ **Theorems A-E の被覆は §10-§15 に完全に帰着し、唯一の穴は issue 0178** — それが **Theorem A(3)(4)** と **Theorem C(9)** として現れる。 📌 **教訓**: 「要約定理」の逐条監査は、**書籍が依存図/schematic proof を持っていないか 先に探す**。BG は持っており、対応表を自分で作る必要はなかった。 ## 🏁 完了 (2026-08-08) | 区分 | 件数 | 状態 | |---|---|---| | §1-§16 の番号付き結果 | **162** | ✅ 全件被覆 | | Theorems A-E | 5 (計 33 条項) | ✅ §10-§15 に還元、対応表確定 | | 補章 A-E | **19** | ✅ 全件被覆 | | **合計** | **186** | | **実形式化 8 件** (すべて axiom-clean): `bgThm310` / `isMulCommutative_actionCommutator` + `bgThm412` / `bgThm53` / `lemma63a` / `bgThm102` / `bgLem108` / `bgProp1011` / `bgCor116`。 **特殊化債務解消 2 件** (§3 の可解性仮説)。**索引補完 7 件** (§9 が AxiomsCheck に不在だった)。 **stale 注記訂正 20 件超**。 **真の未形式化は 0 件** (2026-08-08 確定)。監査中は Prop 14.2 の (a)(g) を「唯一の真の 未形式化」と判定し issue 0178 を起票したが、**実装に入って両方とも packaging 差だと判明** (部品は repo に在り、繋ぐ endpoint だけが無かった)。 ⟹ `S14.typeP2_Msigma_isNilpotent` / `S16.typeP2_exists_regular_abelian_hall` で解消、 [0178 closed](0178-bg-prop142-regular-u-and-nilpotent-msigma.md)。 🚨 (a) の誤判定の原因 = **grep の hit を「別物」と即断した** (`ActsRegularlyOn (E₂ ⊔ E₃) E₁` は返っていたが `E₁ = K`, `E₂⊔E₃ = U` に気づかなかった)。 ⟹ **書籍の変数と repo の setup 変数の対応表を先に作る**。 ⟹ **3 冊の逐条監査 (Peterfalvi 284 / Isaacs 305 / BG 186) がすべて完了**。 ## 📌 BG の大域規約 (2026-08-08 §3 で確定 — 全節の判定に効く) **これを知らないと偽の特殊化債務を起票する**: | 規約 | 出典 | 意味 | |---|---|---| | 「All groups considered in this work will be **finite** except when explicitly stated otherwise」 | 書籍 p.4 (pdftotext L612) | `[Finite G]` は書籍強度 | | 「we consider representations … by **finite-dimensional** linear transformations. … By module we will always mean **finite-dimensional** right module」 | 書籍 p.9, §2 冒頭 (L961-967) | **`[FiniteDimensional F V]` は書籍強度** — module 系 statement (Thm 3.4 / 3.5 等) に付いていても債務でない | ⚠ 個々の statement 本体には書かれていないので、**節冒頭の規約を読まないと 「repo が書籍より狭い」と誤判定する**。 ## 完了条件 BG の全番号付き結果が**書籍強度**の Lean statement を持つか、**mathlib 被覆として対応が 記録されている**。特殊化債務ゼロ・部分被覆ゼロ・packaging 差ゼロ。 各節の監査結果を census note に記録する。 ## 🔎 逐条監査の走査手順 (2026-08-08 §2 で確定 — 順に全部やる) §2 で「実体が在るのに無いと判定した」ので、走査対象を固定する。**(4) だけでは足りない**。 1. **`OddOrder/AxiomsCheck.lean` を書籍番号で grep** — ここが **書籍番号 ↔ Lean 実体の最良の 索引**。`grep -n "Lemma 2.7\|Lem 2.7" OddOrder/AxiomsCheck.lean` で一発で当たった。 2. **`issues/closed/` を番号で grep** — 過去に閉じた形式化 issue が残っている (`0150-bg-lemma-2-7-*`, `3009-lem27-*`)。 3. **結論の形 (概念名) で repo 全体 grep** — 書籍ラベルでの grep は他書と衝突するうえ、 実体のファイル名は概念名 (`ElemAbelianAutAction` / `SingerReducibility`) なので当たらない。 4. 節ディレクトリの file header 対応表 + `theorem` 一覧。 ## ⚠ 誤判定様式 (前 2 冊で計 16 件の実例) 正本 = memory `textbook-coverage-audit-failure-modes` (11 型)。とくに: * **「計画表の欠落 ≠ 実体の欠落」** (§2 Lem 2.7, 2026-08-08)。`S02_RepresentationsBasic.lean` の §2A-§2F 区分に Lem 2.7 が無いのは事実だが、実体は BG ディレクトリの**外** (`GroupTheory/RepresentationTheory/`) に在った。区分表の穴は**当たりを付ける道具**であって 不在の証拠ではない。 * 🚨 **書籍の Note / Remark を statement と一緒に読む** — BG は Lem 3.2 と Thm 3.5 の直後に 「`K` が可解という仮説は不要」という Note を置いており、それを読まずに statement だけ 写した結果 5 宣言に**書籍が明示的に不要と言った仮説**が入っていた (2026-08-08)。 **番号付き結果の直後の Note/Remark は statement の一部として扱う**。 * **注記は当たりを付ける道具であって判定の証拠ではない** — Isaacs では stale 注記の訂正 (7 件) が実際の補充 (5 件) を上回った。 * 🚨 **AxiomsCheck の「(a)+(b)」表記も条項被覆の証拠にならない** (§3 Thm 3.10, 2026-08-08)。 注記が「BG Theorem 3.10 **(a)+(b)**, elementary-abelian GROUP case」と書いていても、 それは「その周辺で (a) も証明済」の意で、**endpoint の結論の型に (a) が入っている 保証ではない**。実際 group form は (a) を捨てて (b)+(c) だけ返していた。 ⟹ **条項照合は注記でなく `theorem` の結論の型を読む**。 * 🚨 **「(x) は M-independent ゆえ elsewhere で提供」型の docstring は行き先を確認する** — Thm 3.10 の "elsewhere" は**可換 kernel 専用**の特殊形で、書籍の条項を満たさなかった。 * 🚨 **「証明の中にある」は被覆でない** (§4 Thm 4.12, 2026-08-08)。(a) の一般形も (b) の 積分解も、**別の条項の証明の内部では現に構成されていた**が endpoint に出ていなかった。 ⟹ 条項照合では `theorem` の**結論の型**だけを数える。proof body は数えない。 * 🚨🚨 **`^theorem ` grep は docstring 内のコードフェンスに当たる** (§2 Prop 2.1, 2026-08-08 に §13 の走査で発覚)。`S02_RepresentationPropositions.lean:84` の `absolutely_irreducible_iff_hom_eq_F` は「**Lean signature 案 (未確定)**」という docstring 内の 草案で、列 0 から始まるため `grep -n "^theorem "` が宣言として拾ってしまっていた。 §2 census はこれを Prop 2.1 の実体として記録していた (実体は別モジュールに在ったので 未形式化ではなかったが、所在記録が誤り)。 ⟹ **実体確認は `grep -rn "" --include=*.lean` で全 hit を見て、その行が本当に宣言かを 確認する** (hit 1 件でそれが docstring 内なら未実装)。 * 🚨 **結論の連言数だけ見て ✅ にしない — 書籍の 1 条項が 2 主張のことがある** (§10 Lem 10.8(c), 2026-08-08)。`isHall_Mbeta` の 4 連言を見て被覆と判定したが、書籍の (c) は 「normal `p`-complement を持つ**かつ** `p` が最大素因子」の 2 主張で、後者が束から漏れていた。 * 📌 **節ごとの監査を終えたら deferral 注記の一括走査をかける** — `grep -rn "追加予定|stub 未配置|remains deferred|deferred proof obligation|TODO|Phase 1 待ち"`。 §13 で実施して §10 と §2 の見落としを 2 件回収した。 * **grep は種別語の略記も含める / 番号だけで引く** — Isaacs 7.4 を `Lem` 略記で取りこぼした。 * **内部段の名前が先に当たっても file の endpoint を確認する** — Pf (9.11) / Isaacs 3.34 / 9.23。 * **検索範囲を章のディレクトリに絞らない** — owner chapter 規則で他章に在る (Isaacs 2.20 / 3.15 / 3.23)。 * **`⊴` と `<` は pdftotext で区別不可** — ページ画像が必須 (Isaacs 1.24)。 * **TFAE/iff は書籍の条項数と一致するか確認** — Isaacs 5.26 は 3 条件中 (1)⇔(3) だけだった。 ## 参照 - 前身: [issue 0172](0172-peterfalvi-full-formalization.md) / [issue 0176](0176-isaacs-full-formalization.md) - 書籍: `references/bg/local-analysis.pdf` - Coq 併読: `coq/theories/BGsectionN.v` (ファイル名が BG の節構成と 1:1 対応)