# A spanning tree inside a square parent graph

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

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-spanning-tree-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Audit all vertices, edge membership, connectivity and acyclicity.

An unweighted model with no MST claim.





## Givens and symbols


- work


- G1 — V={0,1,2,3}; parent edges are e0={0,1},e1={1,2},e2={2,3},e3={0,3}; select T={e0,e1,e2} while retaining all V.


- V,E — complete vertex and edge sets
- T — selected parent edges





## 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 — Use a fully specified finite connected simple parent graph and a subgraph formed from selected parent edges. Check edge membership, all parent vertices, connectivity and acyclicity. Connectivity plus n−1 edges, or acyclicity plus n−1 edges, certifies a tree; n−1 edges alone do not. Retain the one-vertex case and make no weighted or minimum-spanning-tree claim. · mko-spanning-tree
- work · prerequisite — A finite simple undirected graph has loop-free duplicate-free unordered edges; graph properties are audited on all declared V and E. Connected means every vertex pair has a path; acyclic means no cycle; a tree is connected and acyclic; a spanning tree retains every parent vertex.





## Main derivation

S01 · impliesBefore

T=\{e_0,e_1,e_2\}

After

T\subseteq E,\quad V_T=V

Conditions: none

Rule: work · Uses: G1, work

Leaf basis: work

Every selected edge belongs to the parent and the vertex set is all V.



S02 · impliesBefore

0\to1\to2\to3\text{ using }T

After

\text{every vertex is reachable from }0

Conditions: none

Rule: work · Uses: G1, S01, work

Leaf basis: work

The path prefixes explicitly reach1,2,3 from 0.



S03 · impliesBefore

\text{all vertices reachable from }0

After

(V,T)\text{ connected}

Conditions: none

Rule: work · Uses: G1, S02, work

Leaf basis: work

Reachability witnesses cover all four vertices.



S04 · impliesBefore

(V,T):\quad\deg_T(0)=1

After

0\text{ cannot lie on a cycle}

Conditions: none

Rule: work · Uses: G1, S03, work

Leaf basis: work

A cycle vertex needs two incident cycle edges, whereas0 has only one edge.



S05 · impliesBefore

\text{delete leaf }0\text{ and }e_0

After

1-2-3\text{ remains; delete leaf }1\text{ then edge }\{2,3\}

Conditions: none

Rule: work · Uses: G1, S04, work

Leaf basis: work

Delete leaves successively, removing no possible cycle, until no edges remain.



S06 · impliesBefore

(V,T)\text{ connected and acyclic}

After

T\text{ is a spanning tree},\quad|T|=3=|V|-1

Conditions: none

Rule: work · Uses: G1, S05, work

Leaf basis: work

The tree definition and all-V condition certify spanning; the edge count cross-checks it.



S07 · impliesBefore

H:\ V=\{0,1,2,3\},\ E_H=\{01,12,02\}

After

|E_H|=3=|V|-1,\quad H\text{ disconnected and cyclic}

Conditions: none

Rule: work · Uses: G1, S06, work

Leaf basis: work

A triangle plus isolated 3 completely refutes the n-1-only criterion.



S08 · impliesBefore

V=\{v\},\quad T=\varnothing

After

\text{connected length-zero paths and no cycles}\implies\text{spanning tree}

Conditions: none

Rule: work · Uses: G1, S07, work

Leaf basis: work

Retain the one-vertex case, with zero edges equal to n-1.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S07, work — No weights were given, so no minimum-weight comparison is made.
- S07 · premise_audit · G1, S06, work — The counterexample graph is separate from the original parent.
- S06 · premise_audit · G1, S05, work — The tree claim does not rest merely on counting three edges.
- S05 · premise_audit · G1, S04, work — Any original cycle would survive leaf deletion, contradicting the final state.
- S04 · premise_audit · G1, S03, work — Use T-degrees, not parent degrees.
- S03 · premise_audit · G1, S02, work — The parent also contains T and is connected.
- S02 · premise_audit · G1, S01, work — Undirected paths can reverse, connecting any two vertices via0.
- S01 · premise_audit · G1, work — Spanning requires all V.





## Error controls and negative controls

Two degreesLeaf deletion uses selected-subgraph degrees.

n-1 boundaryProve connectedness and acyclicity rather than relying on edge count alone.


- Every n-1-edge graph is a tree. → reject — A triangle plus an isolate has three edges but is disconnected.
- A singleton with no edges is not a tree. → reject — It is connected and acyclic.
- T is minimum-weight. → reject — No weights or comparison certificate were supplied.





## Result and limitations

T is a spanning tree of the parent; the three-edge count is only a cross-check.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: da0088130c6f6dd6a4f6f6e08bb0139a4ba1ab80dea27a8a789279270b89cb0f
- original source SHA-256: d11ac46e36437f1a939508dc2799a977a5bbb303e3c22bcb76ede0878f29768b
- 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-spanning-tree-01.json)