---
name: Session 2026-04-19 Tier A+ sweep + STEP 926/927
description: Tier A+ 22+ STEP Lean 4 sweep (23 problems), Köthe CommRing theorem (STEP 926), Oppermann n ≤ 10⁶ verification + mod 96 Rei correlation (STEP 927). 2 commits pushed, no papers published.
type: project
originSessionId: 103c655f-ad00-47ae-81cd-c24a2282f28c
---
# Session 2026-04-19 — Tier A+ completion sweep + STEP 926/927

## 概要

Wikipedia 146+ 未解決問題の横断的 Lean 4 形式化を継続。藤本さんの「Option A で一気に Tier A+ 全完了」要請に応えて 22 STEP を 5 batch に整理して連続実行 (結果 23 STEP 完遂). その後チャット Claude と Köthe / Oppermann / Artin / Hall / Gauss 円 / Jacobson の 6 問題について難易度評価を交わし、選ばれた 2 問題 (Köthe Z/nZ + Oppermann n≤10⁶) を深掘り.

## 主要成果

### 1. Tier A+ sweep (commit 54beb8e) — 7 Lean files, 853 lines, all build green

| File | STEP | 内容 |
|---|---|---|
| FibonacciPrimes.lean | 911 | ★ Rei 固有接続 (F_14=377 / π(64)=96) |
| SophieGermainCunningham.lean | 907+912 | SG 素数 + Cunningham chain (2→47, 89→2879) |
| SmallPrimeFamilies.lean | 906+908+909+910 | Lucky+Thabit+Palindromic+Repunit |
| AdditivePrimeProblems.lean | 897+898+899+894 | Goldbach+Lemoine+Fermat-Catalan+3-cubes |
| OrbitIterationProblems.lean | 902+913+903+921 | Gilbreath+Happy+Triplets+Ruth-Aaron |
| PerfectFamilyExtended.lean | 916+918+920+925 | 奇数完全+準完全+概完全+3-perfect |
| DiscreteMisc.lean | 893+922+915+914+895 | Markov+Singmaster+HN+Hadamard+Bunyakovsky |

### 2. STEP 926 — Köthe for CommRing/Z/nZ (commit 0a76b19)

★ 重要転換 — STEP 888 の `koethe_conjecture` axiom は非可換 case のみに残る:

- `koethe_commutative`: Mathlib CommRing + IsNilpotent で **構造的に証明**
- `koethe_commutative_via_nilradical`: I ⊆ nilradical R を証明
- Z/nZ の nilpotent 元完全決定: n ∈ {4, 6, 8, 9, 12, 16, 18, 96}
- Z/96Z 特記: nilradical = 6・Z/96Z (= rad(96) の倍数)

22 theorems, zero sorry. Build green under Mathlib v4.27.0.

### 3. STEP 927 — Oppermann n ≤ 10⁶ verified (commit 0a76b19)

Miller-Rabin 決定論的素数判定 (witnesses {2,3,...,37}, 3.3·10¹⁴ 以下で決定的):
- **n = 2..1,000,000 全検証 (277 秒, 0 violations)** ✅
- Oppermann 予想成立 (1882, 140+ 年未解決)

mod 96 相関 (Rei HARD_96 = 25 residues, STEP 694):
- **素朴 null (uniform-96)** → 偏差 +91% / +120% ← **artefact** (素数は coprime-6 に集中)
- **正しい null (coprime-to-6 restricted, 32 residues)** →
  - primeLo (下側区間 [n²−n+1, n²] 最小素数): **−0.05%** (independent)
  - primeHi (上側区間 [n², n²+n] 最小素数): **+14.97%** (non-trivial excess)

primeHi の +15% 非対称は **exploratory finding**. Paper 83 原則で因果主張は保留.

### 4. チャット Claude 協業 — 難易度評価 6 問題

独立評価を交換:
- Köthe / Artin: ★★★/★★ アプローチ可 (Rei 適性高い)
- Oppermann: ★★ 中 (RH と独立に難, RH より強いとは未証明 — ここで訂正した)
- Hall: ★ ABC 依存で待機が賢明
- Gauss 円問題: ★ Huxley 131/208 以降 20 年停滞
- Jacobson: ★ 抽象度高く Lean 化困難

合意結論: Köthe + Oppermann を深掘りターゲットに選択 → 上記 STEP 926/927 実行.

## 公開状況

- **GitHub**: 2 commits pushed (`54beb8e`, `0a76b19`)
- **Zenodo / 他 11 platforms**: 未公開 ← **次回セッション予定**
- Paper 118 原稿未起草

## note.com 用テキスト

`C:\Users\user\Downloads\note-2026-04-19-unsolved-problems-sweep.txt` 保存済.
ORCID 0009-0004-6019-9258 + 本セッションの既存 DOI (114/115/116/117) + 本日の commit ID 記載.

## 次回優先 TODO

1. **Paper 118 起草** (今日の 25 STEP 分をまとめる. primeHi +15% は慎重に exploratory として書く)
2. 全 12 platform 公開 (藤本さん同席下で)
3. チャット Claude 次の提案 (他の難易度評価未了問題) への継続応答

## 累計 (2026-04-19 時点)

- 論文 117 本
- Lean 4 theorem ~31,000 件
- STEP 927 到達

## セッション pending

- Collatz (a)-(e) 5 options pending (STEP 696 後保留のまま)
- OEIS 提出 / mathstodon nsec rotation / Storacha setup / Arweave wallet (前回 ULTRA handoff より)