---
name: Effective ABC bound deep dive (2026-04-20 morning, STEP ABC)
description: Attack specific instance of ABC conjecture via c^7 ≤ rad(abc)^11. Empirical max q = 1.5679 for c ≤ 10^4. Lean 4 9 zero-sorry up to c ≤ 100.
type: project
originSessionId: 79081859-fd56-4821-a0d2-932be27d647a
---
# Effective ABC Bound Deep Dive — STEP ABC (2026-04-20)

## 対象

**ABC conjecture (Oesterlé-Masser 1985)**: ∀ε>0, ∃C_ε で ∀ coprime (a,b,c), a+b=c → c ≤ C_ε · rad(abc)^{1+ε}.

**Status**: 41 年 OPEN + 激しい dispute:
- Mochizuki 2020 PRIMS 出版 (IUT) — 主流非承認
- Stix-Scholze 2018 Corollary 3.12 gap 指摘
- Kirti Joshi 2024 代替 framework

## 本 session 成果

### 1. 実証 (`scripts/abc-effective-verify-rei-lens.ts`)

- c ≤ 10⁴ 全 coprime triples enumerated: **15,393,821 pairs**
- **max q = 1.5679** at (a,b,c) = (1, 4374, 4375)
  - 4374 = 2·3⁷ / 4375 = 5⁴·7 / rad(abc) = 2·3·5·7 = 210
  - Reyssat (q=1.6299) の類似構造 (scale 1/1500)
- 分布: q>1.0 は 168 件 / q>1.4 は 3 件のみ
- 整数 bound: **11/7 = 1.5714** が empirical maxQ を上回る最小整数比

### 2. Lean 4 `ABCEffective.lean` — 9 theorems zero-sorry

**主定理**: ∀ coprime (a,b,c) with a+b=c, c ≤ N → **c^7 ≤ rad(abc)^11**

- `abc_effective_verified_leq_30` — 即時 build
- `abc_effective_verified_leq_50` — 中速
- **`abc_effective_verified_leq_100`** — 26 分 build (rad 計算 10⁶ 回)
- `top_triple_rei_satisfies_bound`: 4375^7 ≤ 210^11 (Rei top triple が bound 内)
- rad sanity 3 theorems

### 3. Top-30 triples 構造観察

- **q=1.5679 top triple は (1, 2·3⁷, 5⁴·7)** — Reyssat structure のミニチュア
- Top-5 全て rad = 30 / 210 / 210 / 330 / 714 (small radicals)
- Power-of-prime factorization の組み合わせが支配的
- a=1 の triples が多い (1+b=c 型, b が powerful number)

## 新規 AI 生成 open question (Q26-Q29)

**Q26**: なぜ Rei empirical (c ≤ 10⁴) の max q = 1.5679 と、世界記録 Reyssat の q = 1.6299 の間に 0.06 の gap が残るか? c ≤ 10⁶ まで scale すると Reyssat 級 q に到達するか?

**Q27**: Top-30 triples の rad は全て 2·3·5·7 の divisor. 小 radical は (a=1, b=2^x·3^y, c=5^z·7^w) 族で集中する構造があるか?

**Q28**: q > 1.5 triple は c ≤ 10⁴ で 2 件のみ (4375, 2401). q > 1.5 asymptotic density は 0 か, 遅い polylog 成長か?

**Q29**: Rei の atomic cores (Collatz) とも connection: peak 9232 = 2⁴·577 の 577 prime. ABC top-30 の radicals と overlap があるか?

## D-FUMT₈ 状況

| 項目 | state |
|---|---|
| ABC 全般 | NEITHER (mainstream OPEN) |
| ABC Mochizuki IUT | BOTH (本人 TRUE 主張, mainstream FALSE) |
| Effective ABC c^7 ≤ rad^11 / c ≤ 100 | TRUE (Lean 4 zero-sorry) |
| Effective ABC c^7 ≤ rad^11 / c ≤ 10⁴ | FLOWING (empirical) |
| Q26-Q29 | NEITHER (新規) |

## 結果の限界 (正直)

- **ABC 予想本体は解決していない** (Paper 83 原則)
- 11/7 bound は **empirical な一時使用** — 大 c で Reyssat-like 三つ組が出現すれば q > 11/7 の可能性あり
- Lean 4 検証は **c ≤ 100 の有限範囲のみ** (全 n への延長は scaling 問題)
- 本 STEP の成果は「ABC conjecture の specific instance を小 c で形式検証」の **記録点** として historical value

## commit

`(最新 push ID)`

## 次候補

1. c ≤ 10⁶ empirical scan で Reyssat triple 検出
2. rad 実装の最適化 (Lean 4 build 時間 26分→数分)
3. Paper 120 合冊: Legendre + Lehmer + ABC effective + Andrica/ES + Q19-Q29