Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A minimum spanning tree lower-bounds metric-TSP optimum

Statement

For a metric-TSP instance, let T be a minimum spanning tree of its complete weighted graph. Then w(T)≤OPT⁡TSP.

Facts & Assumptions

Given: A metric-TSP instance with vertex set V, ∣V∣=n≥3, complete graph K on V, nonnegative symmetric rational lengths d, and the optimal tour cost OPT⁡TSP; and a minimum spanning tree T of K of weight w(T).

[F1]

A feasible tour is a cyclic ordering vπ(1),…,vπ(n) visiting every vertex exactly once, its cost sums the consecutive lengths including the closing edge, and OPT⁡TSP is the minimum of these costs, attained over the finitely many cyclic orderings; all lengths are nonnegative and every two distinct vertices are joined by an edge. (Metric traveling-salesperson problem)

[F2]

A minimum spanning tree of a connected weighted graph G is a spanning tree T with w(T)≤w(S) for every spanning tree S of G, where w(T)=∑e∈E(T)d(e). (Real edge-weighted graphs, total tree weight and minimum spanning trees)

[F3]

A finite graph is connected if and only if it has a spanning tree, and a spanning tree of G is a spanning subgraph with V(S)=V(G), E(S)⊆E(G) that is connected and acyclic. (A finite graph is connected if and only if it has a spanning tree, Spanning trees of a graph)

Proof

technique · direct
1.1F1givenconstruct

Take an optimal tour and write its cyclic ordering as v1,v2,…,vn with the closing edge {vn,v1}, so ∑i=1n−1d(vi,vi+1)+d(vn,v1)=OPT⁡TSP. Delete the closing edge and let Q be the subgraph of K with vertex set V and edge set {v1v2,v2v3,…,vn−1vn}. The subgraph Q spans V and is connected: for i<j the walk vi,vi−1,…,v1,v2,…,vj lies in Q and joins vi to vj. Its total length is w(Q)=∑i=1n−1d(vi,vi+1)=OPT⁡TSP−d(vn,v1)≤OPT⁡TSP, because lengths are nonnegative.

2.1F1F3step 1.1algebra

Since Q is a finite connected graph, [F3] provides a spanning tree S of Q with V(S)=V and E(S)⊆E(Q). All lengths are nonnegative, so deleting edges cannot increase total length and w(S)=∑e∈E(S)d(e)≤∑e∈E(Q)d(e)=w(Q)≤OPT⁡TSP. In particular S is also a spanning tree of the complete graph K, since E(S)⊆E(Q)⊆E(K) and V(S)=V.

3.1F2step 2.1algebra

The tree T is a minimum spanning tree of the complete graph K, and S is a spanning tree of K, so by [F2] w(T)≤w(S)≤OPT⁡TSP.

4.1step 1.1step 3.1algebra∎

Therefore every metric-TSP instance satisfies w(T)≤OPT⁡TSP for a minimum spanning tree T of its complete weighted graph. The argument uses one optimal tour only as a comparison object; it computes no optimal tour and gives a lower bound on OPT⁡TSP, not an upper bound.

Depends on

Used by

Dependency tree · two levels

14 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources