# An Euler circuit with an isolated vertex

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

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-eulerian-trail-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Audit every edge exactly once and the nonisolated support condition.

Finite simple undirected; zero edges use the length-zero-circuit convention.





## Givens and symbols


- work


- G1 — V={0,1,2,3}, E={01,12,02};3 is isolated; walk W=(0,1,2,0).


- V,E — complete vertex and edge sets
- W — vertex walk sequence





## 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 — A trail in a finite simple undirected graph may repeat vertices but not edges. The connectivity part of the existence criterion requires only that all nonisolated vertices lie in one component; isolated vertices do not break the edge support. A nonempty vertex set with no edges uses the length-zero-circuit convention; the empty-vertex graph is out of scope. · mko-eulerian-trail
- work · prerequisite — A finite simple undirected graph has loop-free duplicate-free unordered edges; graph properties are audited on all declared V and E. Each walk step uses an original edge; a trail repeats no edge; an Euler trail uses every edge exactly once; a circuit is a closed trail; degree counts incident edges.





## Main derivation

S01 · impliesBefore

E=\{01,12,02\}

After

\deg=(2,2,2,0)

Conditions: none

Rule: work · Uses: G1, work

Leaf basis: work

Compute every degree; all three nonisolated vertices have even degree.



S02 · impliesBefore

\{v:\deg(v)>0\}=\{0,1,2\}

After

0-1-2-0\text{ connects the entire edge support}

Conditions: none

Rule: work · Uses: G1, S01, work

Leaf basis: work

The nonisolated support is connected; isolated 3 does not break it.



S03 · impliesBefore

W_0,W_1=(0,1)

After

\{0,1\}=01\in E

Conditions: none

Rule: work · Uses: G1, S02, work

Leaf basis: work

The first walk step uses a legal original edge.



S04 · impliesBefore

W_1,W_2=(1,2)

After

\{1,2\}=12\in E

Conditions: none

Rule: work · Uses: G1, S03, work

Leaf basis: work

The second step uses distinct edge 12.



S05 · impliesBefore

W_2,W_3=(2,0)

After

\{2,0\}=02\in E

Conditions: none

Rule: work · Uses: G1, S04, work

Leaf basis: work

The third step returns to 0 using02; orientation does not change an undirected edge.



S06 · impliesBefore

\text{edge sequence }(01,12,02)

After

\text{distinct edges and edge set exactly }E

Conditions: none

Rule: work · Uses: G1, S05, work

Leaf basis: work

The three edges are distinct and exhaust E, giving an Euler trail.



S07 · impliesBefore

W_0=W_3=0

After

W\text{ is an Euler circuit}

Conditions: none

Rule: work · Uses: G1, S06, work

Leaf basis: work

Equal start and end close the trail into a circuit.



S08 · impliesBefore

E=\varnothing,\quad V\ne\varnothing

After

W=(v)\text{ is a length-zero Euler circuit for }v\in V

Conditions: none

Rule: work · Uses: G1, S07, work

Leaf basis: work

State the zero-edge convention; empty-vertex graphs are outside scope.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S07, work — The singleton walk repeats no edge and covers empty E.
- S07 · premise_audit · G1, S06, work — Euler concerns all edges, not Hamilton's once-per-vertex requirement.
- S06 · premise_audit · G1, S05, work — Revisiting0 is allowed; a trail forbids repeated edges.
- S05 · premise_audit · G1, S04, work — 02 and 20 denote the same unordered edge.
- S04 · premise_audit · G1, S03, work — It does not reuse01.
- S03 · premise_audit · G1, S02, work — Consecutive walk vertices require an edge.
- S02 · premise_audit · G1, S01, work — The edge-using circuit need not visit3.
- S01 · premise_audit · G1, work — Each undirected edge contributes two to the degree sum.





## Error controls and negative controls

Unordered edgesNormalize2-to0 to02 before comparing edges.

SupportApply connectivity to vertices with positive degree.


- Isolated 3 makes an Euler circuit impossible. → reject — The supplied W already uses every edge.
- A trail cannot revisit0. → reject — A trail forbids repeated edges, not vertices.
- (0,1,0,2) is an Euler trail here. → reject — It uses01 twice and omits12.





## Result and limitations

W=(0,1,2,0) uses all three edges once and is an Euler circuit; isolated 3 is harmless.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: cd1f3d71a3456a1a2c90e91c98b3c616a6c81cfb80bc766effb371a9418f4eed
- original source SHA-256: e58be6b3dd89120f7fd12c07583f1e4197ebffd5d8058f2882ca58fc9b81553c
- 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-eulerian-trail-01.json)