LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-07-31

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.

Shortest-path distance is a metric on every connected component

Statement

Let $C$ be the vertex set of a connected component of a graph $G$ . The function $d_G:C\times C\to\mathbb N$ satisfies, for all $u,v,w\in C$ ,

$d_G(u,v)\ge0$ , with $d_G(u,v)=0$ if and only if $u=v$ ;
$d_G(u,v)=d_G(v,u)$ ;
$d_G(u,w)\le d_G(u,v)+d_G(v,w)$ .

These are the metric axioms, so shortest-path distance is a metric on $C$ .

Facts & Assumptions

Given: Vertices $u,v,w$ in one connected component $C$ of $G$ .

[F1]

$d_G(x,y)$ is the least length of an $x$ to $y$ path, and the length is a natural number (Graph distance within a component, eccentricity, diameter and girth, including the acyclic convention).

[L1]

Every walk contains a path between the same endpoints whose length is no greater (Every walk between two vertices contains a path between the same endpoints).

[F2]

Reversing a path preserves its length, and concatenating an $x$ to $y$ path of length $a$ with a $y$ to $z$ path of length $b$ gives an $x$ to $z$ walk of length $a+b$ .

Proof

technique · direct

1.1

Every path length is a natural number, hence $d_G(u,v)\ge0$ . The length- $0$ path $(u)$ gives $d_G(u,u)=0$ . Conversely a path of length $0$ has one vertex, so $d_G(u,v)=0$ forces $u=v$ .

1.2

Reversing a shortest $u$ to $v$ path gives a $v$ to $u$ path of the same length, so $d_G(v,u)\le d_G(u,v)$ ; reversing the roles gives the opposite inequality, hence equality.

F1F2

1.3

Concatenate shortest paths from $u$ to $v$ and from $v$ to $w$ . This is a $u$ to $w$ walk of length $d_G(u,v)+d_G(v,w)$ , and [L1] supplies a $u$ to $w$ path of no greater length. Minimality in [F1] gives $d_G(u,w)\le d_G(u,v)+d_G(v,w)$ .

F1F2L1

2.1

Steps 1.1, 1.2 and 1.3 establish separation, symmetry and the triangle inequality directly on $C$ , so $d_G$ is a metric there.

step 1.1step 1.2step 1.3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 16 results over 12 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

R. Diestel, Graph Theory, Chapter 1 preview (standard reference, not scraped)