A spanning tree inside a square parent graph

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

T=\{e_0,e_1,e_2\}

T\subseteq E,\quad V_T=V

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

\text{every vertex is reachable from }0

\text{all vertices reachable from }0

(V,T)\text{ connected}

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

0\text{ cannot lie on a cycle}

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

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

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

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

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

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

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

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

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 degrees

Leaf deletion uses selected-subgraph degrees.

n-1 boundary

Prove 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)