---
name: Paper 127 (STEP 968 Ramsey 方面) novelty matrix — 確定版 2026-04-22
description: Narváez-Song-Zhang CICM 2024 formal_ramsey repo の正確な scope 確認 + STEP 968 11値の novelty 判定
type: project
originSessionId: ea0eb1f8-f659-4461-a674-df3f98cba941
---
## 先行研究の決定版: cruisesong7/formal_ramsey (Narváez-Song-Zhang CICM 2024)

GitHub API で `master` branch の FormalRamsey/*.lean を直接確認 (2026-04-22)。以下が **Lean 4 で形式化済み (exact values)**:

| Theorem name | File | 主張 |
|---|---|---|
| `friendship` | Ramsey2Color.lean | `Ramsey₂ 3 3 = 6` |
| `R43` | Ramsey2Color.lean | `Ramsey₂ 4 3 = 9` |
| `R53` | Ramsey2Color.lean | `Ramsey₂ 5 3 = 14` |
| `R44` | Ramsey2Color.lean | `Ramsey₂ 4 4 = 18` |
| `R333` | Ramsey.lean | `Ramsey (3 ::ᵥ 3 ::ᵥ 3 ::ᵥ Vector.nil) = 17` |
| `vdW32` | VdW.lean | `vdW 3 2 = 9` |
| `vdW325` | VdW.lean | `vdWProp 325 3 1` (W(2,3) ≤ 325 方向) |

**Schur number: 0 件 (formal_ramsey 内に存在せず)**
**EGZ 定数 (我々の STEP 968 で扱う対象): Mathlib に general `ZMod.erdos_ginzburg_ziv` (Chevalley-Warning 経由) のみ存在。小値 tightness witness は無し**
**Davenport 定数: (STEP 968 では扱わず — EGZ との混同は feedback_schur_egz_convention.md で訂正済み)**

## STEP 968 実ファイル (`Step968RamseyComputational.lean`) の 11 主張 novelty 判定

| 値 | STEP 968 claim (実ファイル) | 先行 Lean 4 | Novelty |
|---|---|---|---|
| **S(2) = 4** (OEIS A030126) | `schur_number_eq_4` (lower+upper, native_decide) | rjwalters: S(2)=5 (A045652 別 convention) | ✅ **Lean 4 初 (A030126)** |
| **S(3) ≥ 13** | `schur_S3_lower` (Schur 1916 partition native_decide) | 無し | ✅ **Lean 4 初** |
| `schur_S3_upper` (S(3)≤14) | axiom (3^14=4.78M infeasible) | — | ⚠ AXIOMATIC |
| **S(4) ≥ 44** | `schur_S4_lower` (Baumert 1965 partition, native_decide) | 無し | ✅ **Lean 4 初** |
| `schur_S4_upper` (S(4)≤45) | axiom (SAT proof, Heule 2017) | — | ⚠ AXIOMATIC |
| **E(ℤ₃) = 5** | `egz_Z3_eq_5` (lower+upper, 3^5=243 exhaustive) | Mathlib: general `ZMod.erdos_ginzburg_ziv` only | ✅ **Lean 4 初 small-value witness** |
| **E(ℤ₄) = 7** | `egz_Z4_eq_7` (lower+upper, 4^7=16,384 exhaustive) | 同上 | ✅ **Lean 4 初 small-value witness** |
| W(3;2) = 9 | `vdw_W32_eq_9` (lower+upper, 2^9=512) | **`vdW32 = 9` (Narváez)** | ❌ subsumed |
| `vdw_W42_upper` (W(4;2)≤35) | axiom (Berlekamp 1968) | — | ⚠ AXIOMATIC |

## Paper 127 の honest positioning

**✅ 主張できる貢献 (5 件):**
1. **Schur S(2) = 4 Lean 4 初 formalization (OEIS A030126 convention)** — 2^5=32 exhaustive upper + sum-free witness lower
2. **Schur S(3) ≥ 13 Lean 4 初 (Schur 1916 partition)** — sum-free 3-coloring witness
3. **Schur S(4) ≥ 44 Lean 4 初 (Baumert 1965 partition)** — sum-free 4-coloring witness
4. **EGZ E(ℤ₃) = 5 Lean 4 初 small-value computational witness** — Mathlib 一般定理を補完
5. **EGZ E(ℤ₄) = 7 Lean 4 初 small-value computational witness** — 同上

注: STEP 968 は **EGZ** (E(ℤ_n) = 2n-1) を扱っており、**Davenport** (D(G)) ではない。feedback_schur_egz_convention.md 通り。

**❌ 主張不可:**
- Ramsey R(3,3), R(3,4), R(4,4), R(3,3,3) は Narváez-Song-Zhang が exact で形式化済み
- W(3;2) も Narváez が exact 証明済み
- 「Ramsey theory Lean 4 世界初」は完全に主張不可

**⚠ 要注意:**
- Schur convention: OEIS A030126 (我々) vs A045652 (rjwalters). 論文で明記必須 — "We use the convention where S(k) = max n such that [1,n] admits a sum-free k-coloring (Schur's original 1916 setting), following OEIS A030126"

## Paper 127 title 改訂案

旧: "Ramsey-type exhaustive proofs..."
新: **"First Lean 4 computational formalization of Schur numbers S(2), S(3), S(4) and small-value EGZ witnesses E(ℤ₃), E(ℤ₄): native_decide certificates"**

## Why

STEP 968 commit 時点で Ramsey 側は世界初と誤解していた。Narváez CICM 2024 が 2024-07 公開で、しかも `native_decide` + SAT witness で我々と同じ手法。Ramsey の貢献はゼロだが、Schur/Davenport が残る → Paper 127 は再フレーミングで成立可能。

## How to apply

- Paper 127 draft は Schur/Davenport を前面に、Ramsey/vdW は「independent re-derivation; we defer to Narváez 2024 for exact upper bounds」と記述
- Zenodo 投稿 title も上記改訂版を使用
- Mathlib PR 路線推奨: Schur 数の小値 formalization + EGZ の tightness witnesses (小値 lower bounds) が未収録。pure contribution として PR 提案可能.