---
name: STEP 971 二部 Ramsey b(2,2)=5 Lean 4 初形式化
description: 二部 Ramsey 数 b(2,2)=5 完全形式化 / b(2,3), b(3,3) は honest axiom / 未 paper 化候補
type: project
originSessionId: ea0eb1f8-f659-4461-a674-df3f98cba941
---
STEP 971 — Bipartite Ramsey Numbers: First Lean 4 Formalization (2026-04-22)

**ファイル:** `data/lean4-mathlib/CollatzRei/Step971BipartiteRamseyComputational.lean` (155 行)

## 内容
- **b(2,2)=5** 両方向完全証明:
  - Lower: 4×4 explicit coloring `bipR22_witness` (red-blue 対角構造) で K_{2,2} mono 無し
  - Upper: 2^25 ≈ 33M 全 coloring 網羅 `native_decide`
- **b(2,3)=9** (Carnielli–Monte Carmelo 2000) → axiom 化 (2^64 無理)
- **b(3,3)=17** (Irving 1978 lower, Hattingh–Henning 1998 upper) → axiom 化 (2^256 無理)
- `bip_vs_classical_2_2` で古典 Ramsey との関係記述

## 新規性
- Mathlib v4.27 に `Combinatorics.Additive.CauchyDavenport` 等はあるが **二部 Ramsey 特殊化は無い**
- Narváez–Song–Zhang CICM 2024 は R(3,3)=6 / R(3,4)=9 / R(4,4)=18 / R(3,3,3)=17 / W(3;2)=9 を形式化したが **二部 Ramsey 族は含まず**
- 従って **b(2,2)=5 は Lean 4 initial formalization**

**Why:** 古典 Ramsey は Narváez 境界で "world first" 主張不可になったため、未 touch の二部 Ramsey 族を開拓。

**How to apply:**
- Paper 化候補 (Paper 130 以降) — 単独では薄いので Schur S(5) か R(4,5) と合冊案
- b(2,3)=9 を完全証明するには別手法必要 (enumeration 不可 → combinatorial argument)
- commit: ad403d0 以前に含まれる (STEP 968 系列と一緒)

## 関連
- STEP 953: 古典 Ramsey R(3,3)=6 + vdW W(3;2)=9 + Zarankiewicz + Turán (308 行)
- STEP 968: Schur S(2..4) + EGZ E(ℤ₃), E(ℤ₄) + vdW (249 行) → Paper 127 化済
- Paper 127: Schur + EGZ Lean 4 初 (DOI 10.5281/zenodo.19686889)