---
name: Schur 数・EGZ 定数・Davenport 定数の正確な定義
description: 2026-04-21 STEP 968 で混同したラムジー型不変量の標準定義
type: feedback
originSessionId: 80a567c3-c92a-4757-ac12-f814a062c754
---
組合せ論的不変量の定義を混同しないこと。STEP 968 初版で混同して native_decide が false を返した。

## Schur 数 S(r) — Wikipedia/標準慣習

**S(r) = largest n s.t. {1,...,n} admits a sum-free r-coloring**

- S(1) = 1, S(2) = 4, S(3) = 13, S(4) = 44, S(5) = 160 (Heule 2017 SAT)
- 「上界 S(r) ≤ N」の意味: 全ての r-coloring of {1,...,N+1} が monochromatic Schur triple (x+y=z) を持つ
- 「下界 S(r) ≥ N」の意味: ∃ sum-free r-coloring of {1,...,N}
- 例: S(2)=4 を完全証明 → 下界は N=4 の witness、上界は N=5 (2^5=32) の exhaustive

(別慣習: smallest n forcing triple = S(r)+1 もあるが standard ではない)

## EGZ 定数 E(ℤ_n) — Erdős-Ginzburg-Ziv 1961

**E(ℤ_n) = smallest m s.t. ∀ length-m sequence in ℤ_n has a length-n subsequence summing to 0 mod n**

- E(ℤ_n) = 2n - 1
- E(ℤ₃) = 5, E(ℤ₄) = 7, E(ℤ₅) = 9
- 「下界 ≥ 2n-1」の witness: length 2n-2 で length-n zero-sum subseq を持たない sequence
- 例: E(ℤ₃) ≥ 5 witness は [0,0,1,1] (length 3 subset の和が 1 か 2 のみ)

## Davenport 定数 D(G) — 別物

**D(G) = smallest d s.t. ∀ length-d sequence in G has non-empty zero-sum subsequence**

- 巡回群: D(ℤ_n) = n (trivial、面白くない)
- D(ℤ₂×ℤ₂) = 3, D(ℤ₃×ℤ₃) = 5
- EGZ と Davenport は**別物**。混同注意 (STEP 968 初版で混同)

**Why:** 2026-04-21 STEP 968 初版で「Davenport D(ℤ₃)=5」と書いたが、これは EGZ E(ℤ₃)=5 のこと。Davenport は D(ℤ₃)=3 で trivial。witness [1,1,2,2] も Davenport 用としては zero-sum を含むため失敗 ({1,2}=3≡0)。EGZ なら length-3 subset 和が 1,2 で正解。

**How to apply:** Ramsey 型不変量を Lean 化する際は、必ず標準定義 (Wikipedia 第一義) を確認してから実装。S(r) は Wikipedia "Schur number" の慣習、E(ℤ_n) は EGZ theorem の慣習を使う。