Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26
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.

The path metric of a connected simple graph is a metric on its vertex set

Statement

The path metric of a connected simple graph is a metric on its vertex set.

Facts & Assumptions

Given: The hypotheses of the Statement.

[F1]

The path metric of a connected simple graph assigns to two vertices the least length of a path joining them (The path metric of a connected simple graph).

[F2]

A walk of length in a simple graph is a finite vertex list (v0,,v) with consecutive vertices adjacent; a path is a walk with distinct vertices; the graph is connected when it is nonempty and every two vertices are joined by a path (Walks, paths, connectedness and components in a simple graph on an arbitrary vertex set).

[L1]

Every walk in a simple graph contains a path with the same endpoints and of no greater length (Every walk contains a path between the same endpoints, of no greater length).

[L2]

A metric on a set satisfies separation, symmetry and the triangle inequality (Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric).

[L3]

A simple graph is a pair (V,E) with V any set and E a set of two-element subsets of V (Simple graphs on an arbitrary vertex set).

Proof

technique · direct
1.1

The only path of length zero joins a vertex to itself, so the distance vanishes exactly on the diagonal.

F1F2L3
1.2

Reversing a path preserves its length, so the distance is symmetric.

F1F2
1.3

Concatenating two shortest paths gives a walk of the summed length, which the previous lemma replaces by a path no longer, giving the triangle inequality.

F1F2L1
2.1

Steps 1.1, 1.2 and 1.3 establish separation, symmetry and the triangle inequality, so the path metric is a metric.

L2step 1.1step 1.2step 1.3

Depends on

Used by

Dependency tree · two levels

16 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