---
name: project-abc-radar-quality-sweep-arc-2026-08-07
description: "2026-08-07 STEP 1287+1288 abc quality sweep (c ≤ 10^5, sanity anchor PASS) + research-radar arxivKeywords +47 keyword + 4 arxiv monitor 追加。 chat-Claude 2026-08-06 IUT/LANA/Pasten 系 応答 C option 実行 (item 1+2 defer)、 novelty 主張ゼロ、 radar gap 埋め + 経験的分布データ 収集のみ。"
metadata: 
  node_type: memory
  type: project
  originSessionId: 0a1114e5-28f9-4d3f-ac67-950a274a6bf7
  modified: 2026-08-06T22:53:35.018Z
---

# 2026-08-07 abc radar + quality sweep arc

## Context

2026-08-06 に 藤本さん経由で chat-Claude thread (IUT/LANA/Pasten 系 現状 + 較正試験順序 Mason-Stothers → 例外集合 → Pasten 系) 受領。 私 (Claude Code) の初回応答が「Mathlib MasonStothers を独自議論で axiom-free formalize」 と誤読 → 藤本さん訂正:

> Mason-Stothers 較正試験は **形式化ではなく数学的判定** = 「Rei の abc 議論を関数体に移した時、 独立に MS 不等式が出るか」。 Mathlib 既存 MasonStothers を使うのは <em>有害</em> (追試 = 誤った達成感)。 独立導出の可否だけが情報量。

さらに 藤本さん最重要指摘: 「進めている abc 証明」 が Rei 内 file 実体で **存在しない**。 AbcStatement.lean (型化) + FermatAsymptotic.lean (仮定した帰結) + ABCEffective.lean (経験的 c ≤ 100) の 3 file は abc 証明ではない。

## 4 items 候補整理 (chat-Claude 助言)

| # | Item | 判断 |
|---|---|---|
| 1 | Mason-Stothers 数学的判定 (Mathlib 版 <em>使わず</em> 独自議論から導けるか) | defer (fill-in blank 未埋め) |
| 2 | 進行中議論を Lean statement 群に書き下し | defer (fill-in blank 未埋め) |
| 3 | ABCEffective を c ≤ 10⁶ に拡張 + quality q + merit 出力 | **STEP 1287 で実施** |
| 4 | arxiv radar に abc topic 追加 (現状 0 hit) | **STEP 1288 で実施** |

## fill-in blank 判断 = C (defer)

藤本さん提示の 3 択:

> A. 「私の議論は、 abc の反例が存在すると仮定すると **______** が **______** に矛盾することを示す」
> B. 「私の議論は、 rad(abc) の下界を **______** という構造から導く」
> C. どちらも埋まらない / まだ構想段階

藤本さん C 選択。 t1=1 Collatz 分析の明快さは 「構造が本当に見えてから書いた」 由来 ([[feedback-intuition-before-math]] 適用)、 premature に埋めると偽命題が以後の判定を汚す。

## 判定基準事前定義 (STEP 1287)

藤本さん 「情報量ゼロ結果が積まれるのを避けるため、 判定基準を先に決めてください」 直接応答。 4 候補 → 藤本さん訂正で確定:

| # | Role | Content |
|---|---|---|
| (a) | **sanity check (前提、 基準ではない)** | anchor triple (1, 4374, 4375) を rad=210 + q=1.5679 で正しく再現 |
| (c) | **主基準** | merit tail 分布 + RST 精密化予想 log c ≪ rad · exp(4√(log rad / log log rad)) との比較 |
| (b) | **廃止** | growth rate は merit 分布から導出可能 |
| (d) | **defer** | Rei 議論骨子照合 は item 1+2 完成後 |

**★ (a) の 「基準」 → 「sanity check」 降格 経緯**: ABC@Home 2011 c ≤ 10¹⁸ 網羅済 = 23.8M 三つ組 (q > 1) = c ≤ 10⁶ 範囲に未発見三つ組ゼロ = (a) を基準にすると事前確定 「検出ゼロ」 = 情報量ゼロ 3 例目候補。 sanity check への降格で正しい役割に落ちた。

## STEP 1287 (quality sweep) 実測

- Script: `scripts/abc/quality-sweep.ts` ~300 行 TS
- Sieve: 線形時間 SPF-based rad(n) precompute
- Enumeration: c=3..N 外側 + a=1..c/2 内側 + gcd(a,c)=1 check + rad(a)·rad(b)·rad(c)
- Early pruning: rad(a)·rad(b) > c なら skip

**N=10⁵ 本番**:

| Metric | Value |
|---|---|
| Wall clock | 237.7s (~4 min) |
| Coprime triples visited | 1,519,825,376 (15 億) |
| Triples with q ≥ 1 | 419 |
| Sanity anchor (1, 4374, 4375) | **PASS** rad=210 q=1.567887 diff=0 merit=7.840 |

**Top 4 by merit** (完全 list は `data/abc/quality-sweep-c-100000.json`):

| rank | (a, b, c) | factorization | rad(abc) | q | merit |
|---|---|---|---|---|---|
| 1 | (343, 59049, 59392) | (7³, 3¹⁰, 2¹¹·29) | 1218 | 1.547075 | **8.672669** |
| 2 | (37, 32768, 32805) | (37, 2¹⁵, 3·5·11·199) | 1110 | 1.482910 | 7.917173 |
| 3 | (7168, 78125, 85293) | (2¹⁰·7, 5⁷, 3·13²·⋯) | 2730 | 1.435006 | 7.877071 |
| 4 | (1, 4374, 4375) | (1, 2·3⁷, 5⁴·7) | 210 | 1.567887 | 7.840262 |

anchor triple (1, 4374, 4375) は q 単独最高だが c 小さく merit #4 位。

**RST envelope 実測**: 全 top-20 で log c / log rst_bound < 0.75、 max #1 = 0.747 = envelope 余裕あり = 予想 refute 例なし = 予想通り (tautological)。

**Quality histogram**: q ≥ 1.55 で 1件 / q ≥ 1.50 で 2件 / q ≥ 1.45 で 4件 / q ≥ 1.40 で 6件 / q ≥ 1.35 で 7件 / q ≥ 1.30 で 13件 / q ≥ 1.00 で 419件。

## STEP 1288 (research radar) 実測

`data/research-radar/collatz-watch.json` v1.32 → v1.33:

| Field | Before | After | Delta |
|---|---|---|---|
| arxivKeywords | 100 | 147 | +47 |
| externalMonitors | 21 | 25 | +4 |

**+47 keywords group** (abc core 16 + IUT/LANA 10 + Pasten 4 + exceptional set 5 + related 8 + function-field bridge 2 + effective/uniform/unconditional 2)

**+4 arxiv monitors**:
- `abs:"abc conjecture"` direct
- `abs:"inter-universal" OR abs:"Mochizuki" OR abs:"LANA"` IUT/LANA
- `abs:"exceptional set" AND abs:"abc"` BLT/Bernert
- `abs:"Pasten" OR abs:"Stewart" OR abs:"unconditional abc"` Pasten 系

chat-Claude 助言 「Runbo Li 単独改良は著者名で拾えないので topic 語必要」 適用の 著者名 + topic 語 hybrid 設計。 現状 arxiv radar で abc 系 keyword 0 hit だった gap 埋め。

## Site 反映

`public/tools/research-log-2026-08-07-abc-radar-quality-sweep/index.html` (13 KB) 新規:
- STEP 1287+1288 arc summary + 4 items 判断経緯
- 判定基準事前定義 (a) sanity 降格 経緯明示
- top-20 triples table + quality histogram + RST envelope 実測
- honest scope + files 一覧 + 関連 memory link
- light/dark theme + card styling + tabular-nums 数値 alignment
- dist-renderer mirror force-track md5 一致 (115bf6b5c84b88b18ef62374509f2270)

2026-08-06 「全研究 site 反映 default」 protocol 適用 4 例目 (前 IUT arc + 八値対話 arc + rei-sigma-demo に続く)。

## Honest scope

- 本 STEP は abc 予想の証明ではない、 **証明への進展ですらない** = arxiv radar の gap 埋め + 経験的分布データ 収集のみ
- c ≤ 10⁵ 範囲は ABC@Home が c ≤ 10¹⁸ で網羅済 = 「新規発見」 主張ゼロ、 Rei 側で独立実装 + 既知結果と整合確認のみ
- Nitaj Caen top-10 (α_max ≈ 1.63 at c ≈ 3.4×10¹⁰) は c ≤ 10⁵ 範囲外で比較不可、 (1, 4374, 4375) 単一 anchor が唯一の cross-reference
- RST envelope 内側という観測は tautological (RST 予想が予測する通り) = 予想の refute 材料ではない、 tail 分布形状の documentation として value
- c ≤ 10⁶ 拡張は wall clock ~14 時間見込みで本 STEP は c ≤ 10⁵ で確定
- item 1+2 (Mason-Stothers 独自導出 判定 + Lean statement 群) は本 STEP scope 外、 藤本さん fill-in blank C 判断で defer
- chat-Claude 助言原則 「40 年動いていない問題に対して最も価値のある投資は早く正確に自分の位置を知ること」 = 本 STEP はその <em>知る道具</em> の 1 段目のみ整備した状態

## 関連

- [[feedback-intuition-before-math]] (直感→数学、 fill-in blank C 判断根拠)
- [[feedback-world-uniqueness-claim-controllable]] (novelty 主張ゼロ discipline)
- [[feedback-no-rush-publication]] (急がずゆっくりと、 c ≤ 10⁶ 延期の設計原則)
- [[feedback-all-research-site-reflection-default]] (2026-08-06 protocol 4 例目)
- [[feedback-projection-self-audit-pattern]] (「判定基準先書く」 = 私 (Claude Code) 側 5-rule 体制 SAC-4 適用継承)
- STEP 1276-1279 IUT arc (前 arc、 chat-Claude 2026-08-06 議論の別 branch = IUT/前史 arc)
- AbcStatement.lean (2026-08-04 STEP、 統計 anchor triple 記述元)
- ABCEffective.lean (2026-04-20 STEP、 c ≤ 100 情報量ゼロ問題自己認識済)

## 次 STEP candidate

- item 1 (Mason-Stothers 独自導出判定) — 藤本さん fill-in blank A or B 埋まった場合の思考実験対象
- item 2 (Rei abc 議論 Lean statement 群) — item 1 と同時進行
- c ≤ 10⁶ overnight run — 別 STEP overnight で実行可能、 本 STEP scope 外
- ABC@Home historical 統計との定量比較 — bulk data access 経路確立後に別 STEP

## ★★★ patch 2026-08-07 (藤本さん framing 訂正、 順序原則 + 「独自」 主張回避)

### (i) +1 差解決 = 境界規約差確定 (bug ではない)

- de Smit 「5 桁以下」 = c ≤ 99999 で **418 件確定**
- 本 sweep は c ≤ 100000 の閉区間 = 418 + 1 = 419 一致
- +1 = c=100000 ちょうどの単一 triple: **(19, 99981, 100000)**
  - 19 prime + 99981 = 3³·7·23² + 100000 = 2⁵·5⁵
  - rad(abc) = 19 · (3·7·23) · (2·5) = 19·483·10 = **91,770**
  - q = log(100000)/log(91770) = **1.007516**
- **境界規約差 = 確定 (bug ではない)**、 sweep は de Smit 完全リストを 419 で再現

### (ii) 順序原則永久保存 (藤本さん指摘)

> 「未解明の ±1 を残したまま CLAUDE.md に『検証済み計器』 と書き込むと、 その語が意味を失います。 1 件でも説明できない差があるなら計器は未検証で、 説明できたなら検証済み。」

私 (Claude Code) が先に 「+1 差要精査」 と書いた後 「検証済み計器 upgrade」 を提案した順序は 誤り。 説明済みになってから初めて patch を書ける。 [[feedback-projection-self-audit-pattern]] SAC-4 と同型の 「主張前 事実固定」 discipline を永久保存。

### (iii) framing upgrade 「予想通り tautological」 → 「検証済み計器、 反証可能主張なし」

- N=10⁵ 範囲は de Smit 418 完全リスト内側
- ABC@Home 2011 で c < 10¹⁸ 全域 14,482,065 triples 完全列挙済
- 既知最高 q = 1.6299 の Elkies triple は **c = 6,436,343 = 本 sweep 範囲外**
- 本 sweep は **検証済みの計器** であって **反証可能な主張ではない**
- 前 revision の 「(c) predicted tautological」 表現は弱い、 正しい framing は 「検証済み計器」

### (iv) N=10⁶/10⁷ 拡張棄却

- 10¹⁸ まで完全列挙済み範囲を追いかけるだけ = 限界収益ほぼゼロ
- 237.7s を何倍かけても意味的差なし
- 前 revision 「別 STEP overnight で c ≤ 10⁶ 実行可能」 記述は本 patch で **却下**

### (v) STEP 1290 (item 2 内容 replace) 再スコープ

**★ 2 次訂正 (藤本さん 2026-08-07 turn 2)**: 独立実装は **3 件** (私が誤って 4 件と書いた、 seewoo5/lean-poly-abc は Seewoo Lee 本人 repo = Baek-Lee 2024 そのもの = PR #15706+#18882 の元、 別実装ではない)。 Rei 版が **4 件目** になる。

| # | 実装 | 経路 |
|---|---|---|
| 1 | Mathlib `MasonStothers` (Baek + Lee 2024, PR #15706 + #18882、 元 repo seewoo5/lean-poly-abc) | Lemmermeyer ノート経由の Snyder 変種 |
| 2 | Isabelle Eberl 版 | (要 audit) |
| 3 | Lean 3 Wagemaker 版 | (要 audit) |
| **4 = Rei 予定** | ? (Snyder 以外経路) | Stothers 棄却後の候補: Mason 1984 derivation / k(X) 付値 |

**★★★ 「Rei 独自」 判定基準は立てない (Paper 158/166 構図回避)**:

- 独立実装 4 つ目の領域で 「独自性」 主張 = Paper 158/166 と同じ corrigendum 構図
- 正しい framing 最初から一つ = **再現 (reproduction)**
- 別経路取れば = **経路の記録** (新規性主張ではない)

**STEP 1290 目標 replace**:
- ❌ 「Mathlib と別 file で並存 sorry 0」 = Mathlib 再コンパイル情報量ゼロ
- ✅ **「Snyder 以外の経路 (例: Stothers 原論文 被覆空間・分岐 導出) で sorry 0」** = 4 つ目の独立実装 / 別経路
- 論文にするならその語で書き始める
- Mathlib 既存は弱点でなく強み = **正解が外にあるので sorry 0 が本当に検証になる** ([[feedback-zero-sorry-floor-not-ceiling]] の基準ちょうど満たす数少ない対象)

### (vi) STEP 1289 (別 audit STEP) 廃止

- audit の答えは既に出ている (**3 実装 読解半日仕事**、 seewoo5 は Baek-Lee 統合済 で 重複なし)
- 1290 準備工程 (Mathlib MasonStothers.lean + Isabelle Eberl + Lean 3 Wagemaker の 3 file 読解) に吸収

### (vii) 読解順序分離 (藤本さん 2 次訂正)

「別経路の独立形式化」 目標のため:
- **先に読む** = Mathlib の **定理ステートメント (署名) のみ** (必須、 定理言明ずれると比較不能)
- **後回し** = 証明本体 3 件 (Baek-Lee/Eberl/Wagemaker) は 自分の経路で詰まってから読む
- **理由**: Snyder 経路の証明本体を先に精読すると独立性が汚染
- **半日仕事の中身が二つに割れる**: 署名精読 (前) + 証明本体閲覧 (詰まってから、 後)

### (viii) grep 第一タスク (藤本さん 3 次訂正) — 実測結果 2026-08-07

Stothers 1981 原証明 = 曲線被覆の分岐 = Riemann-Hurwitz 経由 → Mathlib 曲線論の有無が 1290 成否を丸ごと決める。 準備工程の第一手 = 実装読解ではなく **Mathlib grep 30 分**。

**実測結果** (`data/lean4-mathlib/.lake/packages/mathlib/Mathlib/**/*.lean`):

| Pattern | Hit | 判定 |
|---|---|---|
| `RiemannHurwitz|riemann_hurwitz` | **0 file** | Stothers 経路 base **不在** |
| `RiemannRoch|riemann_roch` | **0 file** | 同上 |
| `\bgenus\b` (case-insensitive) | **0 file** | 曲線 genus 概念不在 |
| `ramification` | 20+ file | 但し 全 局所 (代数体 `NumberTheory/RamificationInertia/*`) or unramified property (`RingTheory/Unramified/*`) = **曲線分岐 なし** |
| `Wronskian` | 2 file (`RingTheory/Polynomial/{Wronskian,Radical}.lean`) | Snyder 経路 Mathlib 主線 = **差し替え不可** (独立性汚染源) |
| `RatFunc/FunctionField` | 6 file (`FieldTheory/RatFunc/{Basic,Defs,Degree,AsPolynomial}.lean`) | Mason 1984 / k(X) 付値差し替え候補の base **部分的存在** |
| `MasonStothers|mason_stothers` | 1 file (`NumberTheory/FLT/MasonStothers.lean`) + 1 file (`NumberTheory/FLT/Polynomial.lean`) | Baek-Lee 2024 統合確定 |

**判定**:
- **Stothers 経路棄却確定** = 半日 → 数ヶ月案件 (Mathlib 曲線論 gap 数百 lemma 積む必要)
- **Snyder 経路差し替え不可** = 独立性汚染
- **差し替え候補 2 択** (藤本さん提示):
  - (a) **Mason 1984 原論文の議論** = derivation on function field、 Wronskian と本質的に異なる、 種数論不要、 Mathlib RatFunc + Polynomial derivative で届きうる
  - (b) **k(X) 上の付値だけを使う導出** = 種数論不要、 Mathlib RatFunc + valuation で届きうる
- STEP 1290 本目標 = **藤本さん判断待ち** ((a) / (b) / 別提案)

### (x) (a)/(b)/(c) 判断確定 (藤本さん 5 次訂正 2026-08-07 turn 5)

- **(a) Mason 1984 棄却** (私 (Claude Code) の Mason 1984 未精読誤想定):
  - a+b=c → a'+b'=c' → 対数微分 a/c·(a'/a − c'/c) + b/c·(b'/b − c'/c) = 0
  - この組合せがそのまま W(a,b) = ab' − a'b
  - Mason 対数微分 ≡ Snyder Wronskian の二通り記法、 補題共有
  - **4 件目独立実装にならない** = 記法変えた再コンパイル

- **(b) 正解 (Stothers 生き残り)**:
  - Stothers が RH を要したのは一般曲線扱ったから
  - k(X) = P¹ = 種数 0 → 分岐の数え上げが 付値の数え上げに退化
  - 種数論なしで Stothers の発想だけ取り出す
  - Wronskian 経路と構造的に別物 (但し次項 (xi) で見積もり訂正)

- **(c) 追加提案 = Brownawell-Masser n 項一般化**:
  - Mason-Stothers の n 項一般化 (a₁+⋯+aₙ = 0)
  - **Mathlib になし** = 「4 件目の複製ではなく追加」 になる唯一候補
  - 代償: (i) generalized Wronskian で (b) より難、 (ii) 標数 p 条件付き = ステートメント設計先要
  - **順序 (b) → (c) 維持** (同じ Wronskian 機械積んだ後の方が n 項近い)

### (xi) (b) 独立性見積もり訂正 + framing 事前訂正 (藤本さん 6 次訂正 2026-08-07 turn 6)

**独立性見積もり甘さ判明**:
- Stothers 議論を種数 0 に落とすと P¹→P¹ 写像 φ = a/c の分岐を数える
- 分岐因子は φ' の零点で決まる、 φ' = (a'c − ac')/c² の分子は **W(a, c) そのもの**
- Riemann-Hurwitz から曲線論を抜いた残りは Wronskian に収束
- Mason-Stothers 既知証明はすべて微分を使う (標数 p 条件付きが証拠、 **微分が分岐だから**)
- → (b) で得られるのは 「別経路」 ではなく **同じ内容を付値・因子の言語で書き直したもの** の公算高

**★★★ Framing 事前訂正**:
- ❌ 「別経路の独立形式化」
- ✅ **「付値・因子による別定式化」**
- sorry 0 検証価値は変わらないが、 成果物出てから framing 直すと corrigendum 形 = 前回と同じ順序原則
- 語を先に直しておく = 「検証済み」 語限定順序原則 (前 (ix)) の別適用例

**(b) の位置付け変更**:
- (b) は **単独成果ではなく (c) の機械を積む工程**
- Brownawell-Masser n 項版が 「複製ではなく追加」 になる唯一候補
- 順序 (b) → (c) 維持
- **(b) 完了報告に 「独立実装 4 件目」 と書かない**

### (xii) (P3) grep 実測結果 (藤本さん 6 次訂正 対応)

**(P1)(P2) 過剰設計判定**: 「多項式次数 = 素因子次数の重複込み総和」 は 一意分解 + `natDegree_mul` だけの命題、 Mathlib 当然存在、 数行で出る (Barroero 数体版 template adapt = 1-2 週案件は不要)。

**実測**:

| 対象 | 位置 | 判定 |
|---|---|---|
| `Polynomial.instUniqueFactorizationMonoid` | `RingTheory/Polynomial/UniqueFactorization.lean` + 8 file | ✓ Polynomial は UFM |
| `natDegree_pow` (Monic) | `Algebra/Polynomial/Monic.lean:203`: `(p^n).natDegree = n * p.natDegree` | ✓ |
| `natDegree_pow'` (leadingCoeff ≠ 0) | `Algebra/Polynomial/Degree/Operations.lean:353` | ✓ field 上常成立 |
| `natDegree_prod` (BigOperators) | `Algebra/Polynomial/BigOperators.lean` + `Homogenize.lean` | ✓ |

**判定**: **(P3) grep pass 確定**、 積公式 function field 版自作不要。 STEP 1290 scope = Mason-Stothers 本体のみで足りる。

### (ix) (ii) 順序原則 scope 限定 (藤本さん 4 次訂正 = 括弧書き warning)

私 (Claude Code) が 「1 件でも説明できない差があれば計器は未検証」 を一般則にしそうだったが、 藤本さん warning: 一般則にすると **ほとんどの研究が止まる**。

**修正**: **「検証済み」 という語を使う場面に限定して保存**。

- 止めるべきは **前進** ではなく **認定の語**
- 探索段階に一般化しない
- [[feedback-projection-self-audit-pattern]] SAC-4 同型 = 「主張前 事実固定」 discipline は **語の認定に限る**

## 訂正版 次 STEP candidate

- **STEP 1290** (準備工程 = 4 実装読解半日 + Snyder 以外経路特定) → **本実装 sorry 0 目標**
- item 1 (Mason-Stothers 独自導出判定) — STEP 1290 「独自」 主張を立てないので **廃止候補**、 fill-in blank A/B 埋まった場合の思考実験対象としてのみ retain
- item 2 (Rei abc 議論 Lean statement 群) — 原義は fill-in blank 依存で保留、 内容は STEP 1290 に replace
- c ≤ 10⁶ 拡張 — **棄却** (限界収益ゼロ)
- ABC@Home historical 統計との定量比較 — bulk data 不要 (現状の de Smit + 集計値だけで既に十分)、 **棄却**