色數
有限簡單圖的色數是proper頂點著色所需顏色數的最小值,需同時具備上界與下界證書。
mko-chromatic-number · definition · v0.10.0
數學敘述
一個proper k-coloring只證chi(G)<=k;等號還須排除(k-1)-coloring。小型完整圖以exhaustive search給下界並用明示著色給上界;greedy結果不當作最優性。空頂點圖採chi=0,非空無邊圖採chi=1。
代表公式(精確 TeX)
chi(G)
成立條件
- 完整有限無loop簡單無向圖,頂點標號0至n-1。
- exact-number題限定n<=9並完整搜尋所有較少顏色配置。
符號作用域
chi— 色數G— 有限簡單圖
直觀、定義與常見誤解
k-colorable表示最多k色,不表示恰需k色。
等號由constructive upper bound與valid lower bound合成。
greedy著色只是一個上界演算法。
找到proper k-coloring便直接宣稱chi(G)=k。
已採用的推導導讀
三角形全部二色配置的排除原始 MKO 保留;導讀有自己的追加式修訂與驗證界線,不代表新 Lean 證明。
前置知識
驗證界線
exact搜尋只覆蓋完整明示的小型有限圖;不作一般複雜度或近似保證。
not_formalized
這不表示內容錯誤;只表示尚未登錄可重播的計算或形式證據。
下一個義務
加入perfect graph與chromatic polynomial。
同源結構化資料
本頁與互動版共用同一個物件與既有語言 edition;未新增證明或人工審定。
原始 MKO JSON · 純文字 Markdown