# A complete coloring and a nonoptimal greedy trace

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

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-graph-coloring-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Audit a proper coloring edgewise and show an upper bound need not be optimal.

Only supplied colorings and one greedy execution, with no general optimality guarantee.





## Givens and symbols


- work


- G1 — V={0,1,2,3}, E={{0,1},{1,2},{2,3}}, c=(1,2,1,2). Greedy processes0,3,1,2 and uses the least positive color absent from colored neighbors.


- V,E — complete vertex and edge sets
- c,g — the two colorings





## Rules and sources

Some rule statements have reader clarifications in this revision: they are paraphrases, not verbatim quotations. Referenced original source bytes and hashes are unchanged.


- mko_definition · cited — Check every edge in the fully specified graph. Nonadjacent vertices may share a color. One proper coloring supplies only a chromatic-number upper bound; optimality needs a separate lower-bound certificate, and a greedy result is not automatically optimal. · mko-graph-coloring
- 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 is a total vertex-color table with distinct endpoint colors on every edge; its color count is its image size; chi is the minimum color count over all proper colorings.





## Main derivation

S01 · impliesBefore

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

After

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

Conditions: none

Rule: work · Uses: G1, work

Leaf basis: work

Each of the four vertices has one color, giving a complete total table.



S02 · impliesBefore

\{0,1\}\in E

After

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

Conditions: none

Rule: work · Uses: G1, S01, work

Leaf basis: work

Audit the first edge.



S03 · impliesBefore

\{1,2\}\in E

After

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

Conditions: none

Rule: work · Uses: G1, S02, work

Leaf basis: work

Audit the second edge.



S04 · impliesBefore

\{2,3\}\in E

After

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

Conditions: none

Rule: work · Uses: G1, S03, work

Leaf basis: work

Audit the third edge, exhausting E.



S05 · impliesBefore

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

After

\chi(G)\le2

Conditions: none

Rule: mko_definition · Uses: G1, S04, mko_definition

Leaf basis: mko_definition

One proper coloring gives an upper bound of two.



S06 · impliesBefore

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

After

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

Conditions: none

Rule: work · Uses: G1, S05, work

Leaf basis: work

The first two vertices have no previously colored neighbors. Vertex 1 avoids color 1 at vertex 0. Vertex 2 avoids color 2 at vertex 1 and color 1 at vertex 3.



S07 · impliesBefore

g=(1,2,3,1)

After

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

Conditions: none

Rule: work · Uses: G1, S06, work

Leaf basis: work

Reaudit the three original edges to validate the greedy result.



S08 · impliesBefore

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

After

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

Conditions: none

Rule: work · Uses: G1, S07, work

Leaf basis: work

The two-color witness explicitly refutes optimality of this greedy result.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S07, work — This one order does not imply that every greedy execution fails.
- S07 · premise_audit · G1, S06, work — Validity does not mean minimum, since c uses two colors.
- S06 · premise_audit · G1, S05, work — This is a complete four-step trace, not just a color count.
- S05 · premise_audit · G1, S04, mko_definition — This step does not generally turn a witness into equality.
- S04 · premise_audit · G1, S03, work — Nonadjacent 1 and 3 need not have different colors.
- S03 · premise_audit · G1, S02, work — 0 and 2 may share a color because they have no edge.
- S02 · premise_audit · G1, S01, work — Checking most edges is insufficient.
- S01 · premise_audit · G1, work — Color labels themselves may be renamed.





## Error controls and negative controls

All edgesList endpoint colors for all three edges.

Greedy orderThe order0,3,1,2 differs from natural vertex order.


- Nonadjacent 0,2 must differ in color. → reject — They share a color in c while every edge is proper.
- Greedy using three colors gives chi=3. → reject — c is an explicit two-color witness.
- Checking01 and 12 suffices. → reject — Edge 23 has its own distinct-color obligation.





## Result and limitations

c supplies a proper two-coloring and hence an upper bound; the specified greedy run uses three colors and is not optimal.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: bd902ee022f3e9a7e028bcbc16fe7a15bfc5763b4e962ada50bb0848119b4213
- original source SHA-256: 77038d6e68dcdd481876b761a977fba847b3a721ba29cab154d3c196492bc827
- 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-graph-coloring-01.json)