# 三角形全部二色配置的排除

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

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

derivation-mko-chromatic-number-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

以上界與完整低色數搜尋證chi=3。

n=3 exact枚舉；不以greedy最優性代替。





## 已知條件與符號


- work


- G1 — V={0,1,2}，E={01,02,12}；二色labels為0、1，配置向量順序(0,1,2)。


- V,E — 完整頂點與邊集合
- χ(G) — 最小色數





## 規則與來源


- mko_definition · cited — 一個proper k-coloring只證chi(G)<=k；等號還須排除(k-1)-coloring。小型完整圖以exhaustive search給下界並用明示著色給上界；greedy結果不當作最優性。空頂點圖採chi=0，非空無邊圖採chi=1。 · mko-chromatic-number
- work · prerequisite — 有限無向簡單圖的邊為無loop、無重複unordered pairs；圖性質須對完整明示V、E逐一檢查。 proper coloring使每邊兩端異色；χ為全體total proper colorings的最小使用色數，k-colorable表示最多k色。





## 逐步主鏈

S01 · implies操作前

c=(0,1,2)

操作後

c(0)\ne c(1),\quad c(0)\ne c(2),\quad c(1)\ne c(2)

條件：無

規則：work · 依賴：G1, work

葉節點依據：work

三色見證逐邊核，給chi≤3。



S02 · implies操作前

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

操作後

2^3=8\text{ assignments}

條件：無

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

葉節點依據：work

完整搜尋有八個向量，容許一色作二色子情況。



S03 · implies操作前

000,001

操作後

c(0)=c(1)=0\implies01\text{ violated}

條件：無

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

葉節點依據：work

前兩配置均在邊01衝突。



S04 · implies操作前

010,101

操作後

c(0)=c(2)\implies02\text{ violated}

條件：無

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

葉節點依據：work

兩個交替配置都在02衝突。



S05 · implies操作前

011,100

操作後

c(1)=c(2)\implies12\text{ violated}

條件：無

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

葉節點依據：work

兩個配置的後兩頂點同色。



S06 · implies操作前

110,111

操作後

c(0)=c(1)=1\implies01\text{ violated}

條件：無

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

葉節點依據：work

最後兩個配置也違規，八案全部分類。



S07 · implies操作前

\text{no proper map }V\to\{0,1\}

操作後

\chi(G)>2

條件：無

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

葉節點依據：work

任何0色或1色配置也不能繞過二色搜尋，且V非空。



S08 · implies操作前

2<\chi(G)\le3,\quad\chi(G)\in\mathbb N

操作後

\chi(G)=3

條件：無

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

葉節點依據：work

整數性合併上、下界得exact chromatic number。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S07, work — 空圖chi=0、非空無邊chi=1是另明示conventions。
- S07 · premise_audit · G1, S06, work — 兩色排除是全域下界，不是一個失敗候選。
- S06 · premise_audit · G1, S05, work — 配置集合為000、001、010、011、100、101、110、111。
- S05 · premise_audit · G1, S04, work — 0、1色號對換不改違規性。
- S04 · premise_audit · G1, S03, work — 不只檢相鄰編號邊，02也在圖中。
- S03 · premise_audit · G1, S02, work — 兩案分別列出，不留未核尾端。
- S02 · premise_audit · G1, S01, work — 使用最多二色不是必須兩色皆出現。
- S01 · premise_audit · G1, work — 仍需排除較少色數才有等號。





## 錯誤控制與反例

枚舉完整八個bit配置各出現一次。

上下界先三色見證，再排所有二色，最後用整數性。


- 找到三色就直接證chi=3。 → reject — 它只給上界；八案排除才給下界。
- 010在三角形proper。 → reject — 邊02兩端都是0。
- 非空無邊圖chi=0。 → reject — 每頂點仍須有一色，最小為1。





## 結論與限制

完整八案排除二色且有三色見證，故chi=3。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: e067a4fb1baa6f694ba27da6d3b5d80c12c74434d72f796ad27dd14c604b48ad
- original source SHA-256: 1ca25d8841495fe4e298468a1912e58c28402ed9745e1fee11300a1b7c39f7b5
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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