Research Log 2026-08-07 — abc radar + quality sweep
1. Context
2026-08-06 に chat-Claude と abc / IUT / LANA / Pasten 系 の 現状 map + 較正試験順序 (Mason-Stothers → 例外集合 → Pasten 系) を議論。 監査で 藤本さん 側 「進めている abc 証明」 の Rei 内 file 実体が statement + folklore 帰結 + 経験的 c ≤ 100 検証 のみ = 実質未着手と判明。
4 items の候補整理 (chat-Claude 助言):
- item 1: Mason-Stothers 数学的判定 (Mathlib 版を 使わず 独自議論から独立に導けるか)
- item 2: 進行中議論を Lean statement 群に書き下し
- item 3: ABCEffective を c ≤ 10⁶ に拡張 + quality q + merit 出力
- item 4: arxiv radar に abc topic 追加 (現状 0 hit)
藤本さん判断 = C option (item 1+2 は 議論言語化が premature = fill-in blank 「私の議論は…」 埋まらず defer)。 items 3+4 のみ本 STEP で着手。 item 1+2 は fill-in が埋まってから別 STEP で。
2. STEP 1288 — research-radar abc topic 追加
Change summary
| Field | Before | After | Delta |
|---|---|---|---|
| version | 1.32 | 1.33 | +1 |
| arxivKeywords | 100 | 147 | +47 |
| externalMonitors | 21 | 25 | +4 |
+47 keywords (grouped)
| Group | Keywords |
|---|---|
| abc core | abc conjecture, ABC conjecture, Oesterlé-Masser, Masser-Oesterle, radical of an integer, rad(abc), abc quality, abc merit, abc triple, good abc triple, abc coprime triple |
| IUT / LANA | Mochizuki, inter-universal Teichmuller/Teichmüller, IUT, LANA project, Kato ZMC, ZEN Mathematics Center, Yamashita IUT, Stix Scholze, Peter Scholze abc |
| Pasten / unconditional | Hector Pasten, Pasten abc, Stewart Yu abc, Stewart-Yu, effective abc bound, uniform abc, unconditional abc bound, ABC@Home |
| exceptional set | Bernert abc, Browning Lichtman Teraevainen, Browning-Lichtman-Teräväinen, exceptional set abc, Runbo Li abc |
| abc-type / related | Letendre abc, abc-type conjecture, Robert Tenenbaum, Robert-Stewart-Tenenbaum, Szpiro conjecture, Szpiro inequality, Vojta conjecture, Vojta inequality, Shimura curve |
| function-field bridge | Mason-Stothers, Mason Stothers polynomial abc |
+4 arxiv monitors
abs:"abc conjecture"— abc core direct hitsabs:"inter-universal" OR abs:"Mochizuki" OR abs:"LANA"— IUT / LANA formalization 戦線abs:"exceptional set" AND abs:"abc"— Browning-Lichtman-Teräväinen + Bernert 系 数値改良競争abs:"Pasten" OR abs:"Stewart" OR abs:"unconditional abc"— Pasten 系 保型形式-Arakelov
設計判断: chat-Claude 「Runbo Li のような単独改良は著者名では拾えないので topic 語が要ります」 助言直接適用で、 著者名 + topic 語 hybrid で網羅性確保。 Runbo Li のような未公表著者や後続 anonymous 改良も topic 語で拾える。
3. STEP 1287 — quality sweep c ≤ 10⁵
Setup + judgment criteria (pre-implementation で書き下し)
藤本さん 「情報量ゼロ結果が積まれるのを避けるため、 判定基準を先に決めてください」 → 3 criteria 事前定義:
| # | Role | Content |
|---|---|---|
| (a) | sanity check (prerequisite, NOT criterion) | anchor triple (1, 4374, 4375) を rad(abc) = 210 + q = log(4375)/log(210) ≈ 1.5679 で正しく再現 |
| (c) | main criterion | merit = (log c)² / (log rad · log log rad) の tail 分布 + RST 精密化予想 log c ≪ rad · exp(4 √(log rad / log log rad)) との比較 (log c / log rst_bound 出力) |
| (b) | retired | growth rate は merit 分布から導出可能で独立基準不要 |
| (d) | deferred | Rei 議論骨子との照合は item 1+2 完成後 (現状 defer) |
★ (a) の 「基準」 → 「sanity check」 降格 経緯: ABC@Home 2011 時点 c ≤ 10¹⁸ 網羅済 = 23.8M 三つ組 (q > 1 全網羅)、 c ≤ 10⁶ 範囲に未発見三つ組は存在しない = (a) を基準にすると事前確定 「検出ゼロ」 = 情報量ゼロ 3 例目候補。 sanity check への降格で正しい役割に落ちた (藤本さん指摘)。
Implementation
- Script:
scripts/abc/quality-sweep.ts(~300 行 TypeScript) - Sieve: 線形時間 rad(n) precompute (SPF-based)、 N=10⁵ で
0.02s - Enumeration: c=3..N 外側 loop + a=1..c/2 内側、 gcd(a,c)=1 check + rad(a)·rad(b)·rad(c) 計算
- Early pruning:
rad(a)·rad(b) > cなら skip (q ≤ 1 保証) - Sanity anchor pre-check: sieve 完成後 sweep 前に
rad[4375]+rad[4374]+rad[1]literal 確認
Result (N=10⁵)
| Wall clock | 237.7 s (~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 |
| de Smit list cross-check | MATCH (418 + 1 boundary = 419、 下記) |
Cross-check with de Smit list (patch 2026-08-07)
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 件で再現。
★★ Position correction (2026-08-07 藤本さん framing 訂正): 本 sweep は 検証済みの計器 であって、 反証可能な主張ではない。 c ≤ 10⁵ 範囲は ABC@Home (2011 完了) が c < 10¹⁸ 全域で 14,482,065 triples 完全列挙済 = 完全リストの内側。 既知最高 q = 1.6299 の Elkies triple は c = 6,436,343 = 本 sweep 範囲外。 N=10⁶, 10⁷ 拡張は 棄却 (10¹⁸ まで完全列挙済み範囲を追いかけるだけ = 限界収益ほぼゼロ、 237.7s を何倍かけても意味的差なし)。 前 revision の 「別 STEP overnight で c ≤ 10⁶ 実行可能」 記述は本 patch で 却下。 「(c) main criterion RST envelope 内側」 = tautological の観測は正しいが弱い、 正しい framing = 検証済み計器 + 反証可能主張なし。 判定基準先書き protocol は STEP 1287 の直接産物ではないが、 藤本さん 「1 件でも説明できない差があれば計器は未検証、 説明できたら検証済み」 順序原則を私 (Claude Code) 側で永久保存 (fill-in blank C 判断と同じ、 [[feedback-intuition-before-math]] 継承)。
Top 20 triples by merit
| rank | a | b | c | rad(abc) | q | merit | log c / log rst_bound |
|---|---|---|---|---|---|---|---|
| 1 | 343 | 59,049 | 59,392 | 1,218 | 1.547075 | 8.672669 | 0.746775 |
| 2 | 37 | 32,768 | 32,805 | 1,110 | 1.482910 | 7.917173 | 0.712121 |
| 3 | 7,168 | 78,125 | 85,293 | 2,730 | 1.435006 | 7.877071 | 0.721551 |
| 4 | 1 | 4,374 | 4,375 | 210 | 1.567887 | 7.840262 | 0.671198 |
| 5 | 1 | 59,048 | 59,049 | 4,026 | 1.323545 | 6.870716 | 0.677224 |
| 6 | 1 | 2,400 | 2,401 | 210 | 1.455673 | 6.758162 | 0.623160 |
| 7 | 7 | 32,761 | 32,768 | 2,534 | 1.326588 | 6.699031 | 0.664707 |
| 8 | 3 | 65,533 | 65,536 | 5,538 | 1.286675 | 6.624695 | 0.667252 |
| 9 | 125 | 50,176 | 50,301 | 4,830 | 1.276233 | 6.462166 | 0.658100 |
| 10 | 128 | 59,049 | 59,177 | 6,018 | 1.262657 | 6.412631 | 0.657010 |
| … | 残 top-100 は data/abc/quality-sweep-c-100000.json | ||||||
#1 の (343, 59049, 59392) = (7³, 3¹⁰, 2¹¹·29): rad(abc) = 7·3·2·29 = 1218、 q = log(59392)/log(1218) = 1.547、 merit 8.67 で N=10⁵ の tail 先頭。 #4 が Rei ABCEffective の anchor triple (1, 4374, 4375) = q=1.5679 で q 単独では最高だが c が小さく merit では #4 位。
Quality histogram
| q ≥ | count |
|---|---|
| 1.55 | 1 |
| 1.50 | 2 |
| 1.45 | 4 |
| 1.40 | 6 |
| 1.35 | 7 |
| 1.30 | 13 |
| 1.25 | 30 |
| 1.20 | 51 |
| 1.15 | 92 |
| 1.10 | 152 |
| 1.05 | 240 |
| 1.00 | 419 |
RST envelope 実測
全 top-20 triples で log c / log(rad · exp(4 √(log rad / log log rad))) < 0.75 = 全て envelope 内側で健全 (RST 予想の refute 例なし = 予想通り)。 最大値は #1 = 0.747 = 「envelope に対して余裕あり」 の位置。
4. Item 1+2 は defer (C option 判断)
藤本さん fill-in blank 判断 = C: 「私の議論は、 abc の反例が存在すると仮定すると ___ が ___ に矛盾することを示す」 or 「私の議論は、 rad(abc) の下界を ___ という構造から導く」 のどちらも premature に埋めると偽命題が以後の判定を汚す ([[feedback-intuition-before-math]] 適用)。 t1=1 Collatz 分析の明快さは構造が本当に見えてから書いたから。 書けるなら書く、 書けないなら C。 本 STEP は C 前提で items 3+4 のみ実行。 item 1+2 は fill-in が埋まってから別 STEP で。
5. 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⁵ で確定。 但し patch 2026-08-07 で c ≤ 10⁶/10⁷ 拡張 棄却 (ABC@Home c < 10¹⁸ 完全列挙済範囲で限界収益ほぼゼロ、 藤本さん判断)。
- item 1+2 (Mason-Stothers 独自導出 判定 + Lean statement 群) は本 STEP scope 外。 藤本さん fill-in blank C 判断で defer。 後続 STEP 1290 (patch 2 次 2026-08-07 再々スコープ後): Mathlib MasonStothers (Baek-Lee 2024 PR #15706+#18882, Lemmermeyer/Snyder 経路、 元 repo seewoo5/lean-poly-abc は Seewoo Lee 本人 repo で Baek-Lee 統合済 = 別実装ではない) + Isabelle Eberl 版 + Lean 3 Wagemaker 版 = **既 3 実装存在** (数訂正 = 藤本さん 2 次訂正)、 Rei 版が 4 件目 になる予定。 「Rei 独自」 判定基準は立てない、 再現 (reproduction) framing + Snyder 以外の経路で sorry 0 が target。 ★ Stothers 1981 (被覆空間・分岐) 経路棄却確定: 2026-08-07 patch turn で Mathlib grep 実測 (`RiemannHurwitz` + `RiemannRoch` + `genus` 全 0 hit、 `ramification` は局所のみ 曲線分岐なし) → 半日 → 数ヶ月案件で本 STEP scope 不能。 差し替え候補 判断確定 (藤本さん 5 次訂正、 (a) 棄却 + (b) 正解 + (c) 追加): (a) Mason 1984 は Wronskian と同一恒等式の別記法 (対数微分 ≡ Wronskian、 補題共有) = 4 件目独立実装にならない = **棄却**。 (b) k(X) 上の付値経路 = Stothers 経路の生き残り (P¹ = 種数 0 で分岐 → 付値 退化) = **選択**、 但し ★ 独立性見積もり訂正 (藤本さん 6 次訂正): Stothers 議論を種数 0 に落とすと φ' の分子は W(a, c) そのもの → RH 抜いた残り Wronskian 収束、 Mason-Stothers 既知証明はすべて微分を使う (微分が分岐、 標数 p 条件付きが証拠) → (b) で得られるのは **「別経路」 ではなく 「付値・因子による別定式化」** の公算高。 ★★★ Framing 事前訂正: 「別経路の独立形式化」 → **「付値・因子による別定式化」**、 (b) は単独成果ではなく **(c) 機械積み工程** として意味を持つ、 (b) 完了報告に 「独立実装 4 件目」 と書かない。 (c) = Brownawell-Masser n 項一般化 (Mathlib になし = 「複製ではなく追加」 唯一候補、 代償 = generalized Wronskian + 標数 p 条件付き)、 順序 (b) → (c) 維持。 読解順序分離 (藤本さん 2 次訂正): 先 = Mathlib 定理ステートメント (署名) のみ / 後 = 証明本体 3 件 (Baek-Lee/Eberl/Wagemaker) は自分の経路で詰まってから (独立性汚染回避)。 ★ (P3) grep pass 確定 (藤本さん 6 次訂正 + Rei 実測): 積公式 function field 版は既存補題 (UFM + natDegree_prod + natDegree_pow) 数行組合せで即出る、 (P1)(P2) 過剰設計判定確定、 STEP 1290 scope = Mason-Stothers 本体のみ。 STEP 1289 (別 audit STEP) 廃止、 1290 準備工程 (第 1 = grep 完遂、 第 2 = 3 実装署名精読) に吸収。
- chat-Claude 助言原則: 「40 年動いていない問題に対して最も価値のある投資は早く正確に自分の位置を知ること」 = 本 STEP はその 知る道具 の 1 段目のみ整備した状態。
6. Files
| Path | Purpose |
|---|---|
scripts/abc/quality-sweep.ts | Quality sweep script (CLI: N argument) |
data/abc/quality-sweep-c-100000.json | Full top-100 + histogram + sanity anchor (N=10⁵ result) |
data/abc/quality-sweep-c-100000.md | Human report |
data/abc/quality-sweep-c-10000.json/.md | N=10⁴ smoke test output (retained for regression) |
data/research-radar/collatz-watch.json | v1.32 → v1.33 (+47 keywords, +4 monitors) |
data/lean4-mathlib/CollatzRei/AbcStatement.lean | abc conjecture Prop-level statement (2026-08-04, pre-existing) |
data/lean4-mathlib/CollatzRei/FermatAsymptotic.lean | abc ⇒ asymptotic FLT folklore (2026-08-05, pre-existing) |
data/lean4-mathlib/CollatzRei/ABCEffective.lean | c ≤ 100 empirical (2026-04-20, pre-existing, 情報量ゼロ問題自己認識済) |