Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedSession-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.

The Svarc-Milnor lemma

Statement

Let G act geometrically on a geodesic metric space X, and fix x0X. Then G is finitely generated. More precisely, if S:={gG:dX(x0, gx0)2D+1} is the finite generating set obtained from Cobounded proper geodesic actions produce finite generating sets, then the orbit map ϕx0:(G,dS)X,ϕx0(g):=gx0, is a quasi-isometry.

Facts & Assumptions

Given: A geometric action of G on a geodesic metric space X, a point x0X, and a real D0 such that every point of X lies within distance at most D of the orbit Gx0.

[L1]

The set S:={gG:dX(x0, gx0)2D+1} is a finite generating set of G (Cobounded proper geodesic actions produce finite generating sets).

[L2]

For this generating set, the orbit map satisfies dX(gx0, hx0)MdS(g,h) for some constant M0 (Orbit maps of isometric actions are coarse Lipschitz).

[L3]

A subset is coarsely dense when every point of the space lies within a fixed distance of it, and a quasi-isometry is a coarse Lipschitz map admitting a coarse Lipschitz quasi-inverse (Coarsely dense subsets, quasi-inverses and quasi-isometries).

[L4]

The word metric is dS(g,h)=g1hS (The word metric of a group with respect to a generating set).

Proof

technique · direct
1.1

By [L1], the set S is finite and generates G, so dS is a word metric on G. Step [L2] gives the coarse-Lipschitz upper bound for ϕx0.

L1L2L4
1.2

The orbit ϕx0(G)=Gx0 is D-dense in X by the choice of D, so it is coarsely dense in the sense of [L3].

L3given
1.3

For gG, the proof of [L1] writes g as a product of at most m elements of S, where m is the least natural number with dX(x0, gx0)m. Therefore gSdX(x0, gx0)+1. Applying this to g1h and using isometricity gives dS(g,h)=g1hSdX(gx0, hx0)+1.

L1L4algebra
2.1

For each xX, choose r(x)G with dX(x, r(x)x0)D; this is possible by step 1.2.

step 1.2choose
3.1

For x,yX, step 1.3 with g=r(x) and h=r(y) gives dS(r(x),r(y))dX(r(x)x0, r(y)x0)+1dX(x,y)+2D+1. So r:XG is coarse Lipschitz.

step 1.3step 2.1algebra
3.2

For every xX, step 2.1 gives dX(ϕx0(r(x)),x)D. For every gG, step 1.3 and step 2.1 with x=gx0 give dS(r(gx0),g)dX(r(gx0)x0, gx0)+1D+1. Thus rϕx0 and idG, and also ϕx0r and idX, are at bounded distance.

step 1.3step 2.1algebra
4.1

Step 1.1 shows that ϕx0 is coarse Lipschitz, and step 3.2 gives a coarse Lipschitz quasi-inverse. Hence the orbit map is a quasi-isometry by [L3].

L3step 1.1step 3.1step 3.2

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