Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck 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.

Orbit maps of isometric actions are coarse Lipschitz

Statement

Let a finitely generated group G with finite generating set S act isometrically on a metric space X, and fix x0∈X. Then the orbit map ϕx0:(G,dS)⟶X,ϕx0(g):=g⋅x0, is coarse Lipschitz. In fact, if M:=max⁡({0}∪{ dX(x0, s⋅x0):s∈S∪S−1 }), then dX(g⋅x0, h⋅x0)≤M dS(g,h)for all g,h∈G.

Facts & Assumptions

Given: A finite generating set S of G, an isometric action of G on a metric space X, and a point x0∈X.

[L1]

A group is finitely generated when some finite subset generates it (Finitely generated groups).

[L2]

An isometric action satisfies d(g⋅x, g⋅y)=d(x,y) for all g∈G and x,y∈X (Isometric, proper, and cobounded actions on metric spaces).

[L3]

The word metric is dS(g,h)=∣g−1h∣S (The word metric of a group with respect to a generating set), and ∣u∣S is the least length of an expression of u as a product of elements of S∪S−1 (Word length of a group element with respect to a generating set).

[L4]

A map is coarse Lipschitz when its output distances are bounded by A times the input distance plus an additive constant B, for some reals A,B≥0 (Coarse Lipschitz maps and quasi-isometric embeddings).

Proof

technique · direct
1.1L1choose

Because S∪S−1 is finite by [L1], adjoining 0 gives a nonempty finite set of real numbers, so the maximum M exists.

2.1L2L3step 1.1algebra

Let u:=g−1h, and write u=s1⋯sn with n=∣u∣S=dS(g,h) and each si∈S∪S−1 by [L3]. Repeated use of the triangle inequality gives dX(x0, u⋅x0)≤∑i=1ndX(x0, si⋅x0)≤nM. Applying the isometry g and [L2] yields dX(g⋅x0, h⋅x0)=dX(x0, u⋅x0)≤M dS(g,h).

3.1L4step 2.1∎

The displayed estimate is a coarse-Lipschitz bound with multiplicative constant M and additive constant 0, so the orbit map is coarse Lipschitz by [L4].

Depends on

Used by

Dependency tree · two levels

15 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