# 完整著色與非最優greedy trace

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-graph-coloring/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-graph-coloring-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

逐邊驗proper coloring並展示上界非自動最優。

只核明示colorings與greedy執行，不作一般最優保證。





## 已知條件與符號


- work


- G1 — V={0,1,2,3}，E={{0,1},{1,2},{2,3}}；c=(1,2,1,2)。greedy依次處理0、3、1、2，取最小未被已著色鄰點使用的正色號。


- V,E — 完整頂點與邊集合
- c,g — 兩個coloring





## 規則與來源

本稿部分規則文字經本輪讀者釐清，屬於改述而非逐字引文；被引用的原始來源內容及雜湊沒有改動。


- mko_definition · cited — 完整核全部邊；非相鄰頂點可同色。一個proper coloring只給chromatic number上界；最優性需另有lower-bound證書，greedy不自動最優。 · mko-graph-coloring
- work · prerequisite — 有限無向簡單圖的邊為無loop、無重複unordered pairs；圖性質須對完整明示V、E逐一檢查。 proper coloring為total頂點色表且每邊兩端異色；使用色數是像集大小；χ為所有proper colorings的最小使用色數。





## 逐步主鏈

S01 · implies操作前

c:V\to\{1,2\}

操作後

c(0)=1,c(1)=2,c(2)=1,c(3)=2

條件：無

規則：work · 依賴：G1, work

葉節點依據：work

四頂點各有一色，total table完整。



S02 · implies操作前

\{0,1\}\in E

操作後

c(0)=1\ne2=c(1)

條件：無

規則：work · 依賴：G1, S01, work

葉節點依據：work

核第一邊。



S03 · implies操作前

\{1,2\}\in E

操作後

c(1)=2\ne1=c(2)

條件：無

規則：work · 依賴：G1, S02, work

葉節點依據：work

核第二邊。



S04 · implies操作前

\{2,3\}\in E

操作後

c(2)=1\ne2=c(3)

條件：無

規則：work · 依賴：G1, S03, work

葉節點依據：work

核第三邊，已遍歷全部E。



S05 · implies操作前

\text{all three edges proper},\quad|c(V)|=2

操作後

\chi(G)\le2

條件：無

規則：mko_definition · 依賴：G1, S04, mko_definition

葉節點依據：mko_definition

一個proper coloring給兩色上界。



S06 · implies操作前

\text{greedy order }0,3,1,2

操作後

g(0)=1,\ g(3)=1,\ g(1)=2,\ g(2)=3

條件：無

規則：work · 依賴：G1, S05, work

葉節點依據：work

前兩點無已著色鄰點；1避0的1；2同時避1的2與3的1。



S07 · implies操作前

g=(1,2,3,1)

操作後

1\ne2,\quad2\ne3,\quad3\ne1\implies g\text{ proper with3 colors}

條件：無

規則：work · 依賴：G1, S06, work

葉節點依據：work

依三條原邊重驗greedy結果合法。



S08 · implies操作前

|g(V)|=3>2=|c(V)|

操作後

g\text{ is not a minimum-color solution}

條件：無

規則：work · 依賴：G1, S07, work

葉節點依據：work

兩色見證明確否定此greedy結果的最優性。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S07, work — 不由一個order推所有greedy都失敗。
- S07 · premise_audit · G1, S06, work — 合法不代表最少，因c已用兩色。
- S06 · premise_audit · G1, S05, work — 這是完整四步trace，不只報最後色數。
- S05 · premise_audit · G1, S04, mko_definition — 這一步不是一般由見證得到等號的規則。
- S04 · premise_audit · G1, S03, work — 沒有要求非相鄰1與3異色。
- S03 · premise_audit · G1, S02, work — 0與2同色合法，因無邊。
- S02 · premise_audit · G1, S01, work — 不能只核大部分邊。
- S01 · premise_audit · G1, work — color label本身可重命名。





## 錯誤控制與反例

all-edge明列三條邊的端點色號。

greedy順序0、3、1、2不是頂點自然順序。


- 非相鄰0、2必須異色。 → reject — 它們在c同色且全部邊合法。
- greedy三色即chi=3。 → reject — c是明示兩色見證。
- 只核邊01與12即可。 → reject — 邊23也有獨立異色義務。





## 結論與限制

c為proper兩色上界；指定greedy用三色而非最優。







## 驗證及來源綁定

2 個本稿宣告算術檢查；只支持所列算式。


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: bd902ee022f3e9a7e028bcbc16fe7a15bfc5763b4e962ada50bb0848119b4213
- original source SHA-256: 77038d6e68dcdd481876b761a977fba847b3a721ba29cab154d3c196492bc827
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-graph-coloring-01.json)