LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

In a connected locally finite graph every ball of the path metric is finite

Statement

In a connected locally finite graph every ball of the path metric is finite.

Facts & Assumptions

Given: The hypotheses of the Statement.

[F1]

A graph is locally finite when every vertex has finitely many neighbours (Locally finite graphs and vertex degree without a finiteness hypothesis).

[L1]

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

[L2]

$B (x, r)$ is the open ball, $\overset{ˉ}{B} (x, r)$ the closed ball and $S (x, r)$ the sphere of centre $x$ and radius $r$ . The radius is always a strictly positive real; a ball of radius $0$ or of negative radius is never written in this library. (Open ball, closed ball and sphere in a metric space).

[L3]

A walk of length $ℓ$ in a simple graph is a finite vertex list $(v_{0}, \dots, 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).

[L4]

A set $A$ is finite when $A \approx n$ for some $n \in N$ . (The cardinality $∣ A ∣$ of a finite set).

[L5]

Every complete ordered field is Archimedean: for every real $x$ there is a natural number $n \geq 1$ with $x < n$ (Every complete ordered field is Archimedean).

[L6]

A subset of a finite set is finite (A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ ).

Proof

technique · induction

1.1

Fix a vertex $x$ . For each natural number $n$ let $C_{n} : = {y : d_{G} (x, y) \leq n}$ . Then $C_{0} = {x}$ , so $C_{0}$ is finite.

L1base

1.2

Assume $C_{n}$ is finite. If $y \in C_{n + 1}$ , choose a path $(v_{0}, \dots, v_{m})$ from $x$ to $y$ of minimal length $m = d_{G} (x, y) \leq n + 1$ . If $m = 0$ then $y = x \in C_{n}$ . If $m \geq 1$ , then $v_{m - 1} \in C_{n}$ and $y$ lies in $N_{G} (v_{m - 1}) \cup {v_{m - 1}}$ . Hence $C_{n + 1} \subseteq ⋃_{v \in C_{n}} (N_{G} (v) \cup {v})$ . Each set $N_{G} (v) \cup {v}$ is finite by local finiteness, so the right-hand side is a finite union of finite sets and is therefore finite; thus $C_{n + 1}$ is finite.

F1L1L3L4ih

2.1

By step 1.2, if $C_{n}$ is finite then so is $C_{n + 1}$ .

step 1.2

3.1

Therefore every $C_{n}$ is finite. Now let $r > 0$ . By the Archimedean property choose a natural number $N \geq 1$ with $r < N$ . Because $d_{G} (x, y)$ is the length of a path, it is a natural number; so $d_{G} (x, y) < r < N$ implies $d_{G} (x, y) \leq N - 1$ . Hence $B (x, r) \subseteq C_{N - 1}$ , and [L6] makes $B (x, r)$ finite.

L1L2L5L6step 1.1step 2.1discharge-induction∎

Depends on

Used by

Balls of a word metric are finite if and only if the generating set is finite Proposition

Dependency tree · two levels

33 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

C. Loh, Geometric Group Theory: An Introduction (2015 course version), 264 pp. (standard reference, not scraped)
C. Drutu and M. Kapovich, Geometric Group Theory (with an appendix by B. Nica), 837 pp. (standard reference, not scraped)