# Excluding every two-color assignment on a triangle

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-chromatic-number/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

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



## Goal and scope

Prove chi=3 using an upper witness and complete lower-color search.

Exact enumeration at n=3, with no greedy-optimality assumption.





## Givens and symbols


- work


- G1 — V={0,1,2}, E={01,02,12}; two-color labels are 0,1, with assignment vectors ordered by vertices(0,1,2).


- V,E — complete vertex and edge sets
- χ(G) — minimum number of colors





## Rules and sources


- mko_definition · cited — One proper k-coloring proves chi(G)≤k; equality also needs a valid exclusion of (k−1)-colorings. Complete small graphs are checked exhaustively for a lower bound and given an explicit coloring for an upper bound. A greedy result alone is not optimality evidence. The empty vertex graph has chi=0 and a nonempty edgeless graph has chi=1. · mko-chromatic-number
- work · prerequisite — A finite simple undirected graph has loop-free duplicate-free unordered edges; graph properties are audited on all declared V and E. A proper coloring gives distinct colors across every edge; chi is the minimum used-color count over all total proper colorings, and k-colorable means using at most k colors.





## Main derivation

S01 · impliesBefore

c=(0,1,2)

After

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

Conditions: none

Rule: work · Uses: G1, work

Leaf basis: work

Audit every edge of the three-color witness, giving chi≤3.



S02 · impliesBefore

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

After

2^3=8\text{ assignments}

Conditions: none

Rule: work · Uses: G1, S01, work

Leaf basis: work

The complete search has eight vectors and includes one-color assignments as subcases.



S03 · impliesBefore

000,001

After

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

Conditions: none

Rule: work · Uses: G1, S02, work

Leaf basis: work

The first two assignments both conflict on edge 01.



S04 · impliesBefore

010,101

After

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

Conditions: none

Rule: work · Uses: G1, S03, work

Leaf basis: work

Both alternating assignments conflict on02.



S05 · impliesBefore

011,100

After

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

Conditions: none

Rule: work · Uses: G1, S04, work

Leaf basis: work

These two assignments give equal colors to the last two vertices.



S06 · impliesBefore

110,111

After

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

Conditions: none

Rule: work · Uses: G1, S05, work

Leaf basis: work

The final two assignments also fail, exhausting all eight cases.



S07 · impliesBefore

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

After

\chi(G)>2

Conditions: none

Rule: work · Uses: G1, S06, work

Leaf basis: work

Zero- or one-color assignments cannot evade the two-color exclusion, with V nonempty.



S08 · impliesBefore

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

After

\chi(G)=3

Conditions: none

Rule: work · Uses: G1, S07, work

Leaf basis: work

Integrality combines upper and lower bounds into the exact chromatic number.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S07, work — The separate conventions are chi=0 for no vertices and chi=1 for nonempty edgeless graphs.
- S07 · premise_audit · G1, S06, work — This is a global lower bound, not one failed candidate.
- S06 · premise_audit · G1, S05, work — The set is 000,001,010,011,100,101,110,111.
- S05 · premise_audit · G1, S04, work — Swapping color labels does not remove the violation.
- S04 · premise_audit · G1, S03, work — Check02 too; it is an edge despite nonconsecutive labels.
- S03 · premise_audit · G1, S02, work — Both cases are explicitly listed.
- S02 · premise_audit · G1, S01, work — At most two colors does not require both to appear.
- S01 · premise_audit · G1, work — Equality still requires excluding fewer colors.





## Error controls and negative controls

Complete enumerationEach of the eight bit assignments appears once.

BoundsGive three colors, exclude every two-color assignment, then use integrality.


- A three-coloring alone proves chi=3. → reject — It gives only an upper bound; the eight-case exclusion supplies the lower bound.
- 010 is proper on the triangle. → reject — Edge 02 has color0 at both ends.
- A nonempty edgeless graph has chi=0. → reject — Each vertex still needs a color, so the minimum is 1.





## Result and limitations

All eight two-color cases fail and a three-color witness exists, hence chi=3.







## Verification and source binding

2 declared checks for this guide; only the listed expressions are covered.


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

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-chromatic-number-01.json)