LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10

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.

Limits of geodesic segments, rays and lines

Statement

Assume AC. A rescaled ultralimit of pointed geodesic spaces is geodesic. Suppose oriented finite segments $S_{n}$ meet a uniformly bounded rescaled neighbourhood of the basepoints on a large set. Their represented limit means the classes with a representative belonging to $S_{n}$ on a large set. Replace segments outside that large set by the constant segment at $e_{n}$ when forming the following parameters. Choose origins $o_{n} \in S_{n}$ in that neighbourhood, so $λ_{n} d_{n} (o_{n}, e_{n}) \leq R$ for one finite $R$ on the large set, and take $o_{n} = e_{n}$ elsewhere. Write their original-distance parameterizations as $γ_{n} : [- α_{n}, β_{n}] \to S_{n}$ , with $γ_{n} (0) = o_{n}$ and $α_{n}, β_{n} \geq 0$ . If $a = \lim_{ω} λ_{n} α_{n}$ and $b = \lim_{ω} λ_{n} β_{n}$ , allowing $+ \infty$ , their represented limit is isometric to $[- a, b] \cap R$ . Every admissible sequence of points on $S_{n}$ lies on this limit. The possibilities are a closed interval (including a point), a ray, or a line.

Facts & Assumptions

Given: Positive scales $λ_{n}$ , a supplied ultrafilter, pointed geodesic spaces and segments meeting the rescaled R-ball about e_n; assume AC.

[F1]

The quotient metric exists; changes off a large set preserve a class. (The rescaled ultradistance defines a metric).

[F2]

Bounded real limits preserve absolute values and order. (Free tail ultrafilters and bounded real ultralimit calculus).

[F3]

A geodesic preserves differences of distance parameters. (Geodesics and geodesic metric spaces).

[F4]

Ray and line domains are respectively a half-line and the real line. (Oriented geodesic rays, lines, parameters and tails).

[F5]

AC selects from each member of a family of nonempty sets. (The Axiom of Choice).

Proof

technique · direct

1.1

If the bounded-neighbourhood hypothesis holds only on a large set $A$ , replace $S_{n}$ by ${e_{n}}$ for $n \notin A$ . The represented limit is unchanged: intersect a representative's membership set with $A$ and replace its other coordinates by $e_{n}$ ; F1 identifies the old and new classes. The new family meets the same rescaled ball for every $n$ . By AC choose $o_{n} \in S_{n}$ with $λ_{n} d_{n} (o_{n}, e_{n}) \leq R$ , and orient the given distance parameter around $o_{n}$ . Put $a_{n} = λ_{n} α_{n}$ , $b_{n} = λ_{n} β_{n}$ . The bounded sequence $a_{n} / (1 + a_{n})$ has limit $q \in [0, 1]$ . If $q < 1$ , define $a = q / (1 - q)$ ; continuity of this rational function near $q$ gives the finite extended ultralimit. If $q = 1$ , then for each finite $H$ , $a_{n} > H$ on a large set, since $a_{n} \leq H$ implies $a_{n} / (1 + a_{n}) \leq H / (1 + H) < 1$ . Define $a = + \infty$ in this case, and define $b$ identically.

F1F2F3F5

2.1

For $t \in J = [- a, b] \cap R$ , set $c_{n} (t) = \max (- a_{n}, \min (t, b_{n}))$ and $x_{n} (t) = γ_{n} (c_{n} (t) / λ_{n})$ . Clamping is in rescaled units; the argument of $γ_{n}$ is in original units. Since $0 \in [- a_{n}, b_{n}]$ , $∣ c_{n} (t) ∣ \leq ∣ t ∣$ and $λ_{n} d_{n} (x_{n} (t), e_{n}) \leq ∣ t ∣ + R$ , so $x (t)$ is admissible. The finite endpoint limits, or the eventual bound at any fixed finite $t$ for an infinite endpoint, show $c_{n} (t) \to_{ω} t$ , including $t = - a$ or $t = b$ when finite.

step 1.1F3algebra

3.1

The exact identity $λ_{n} d_{n} (x_{n} (s), x_{n} (t)) = ∣ c_{n} (s) - c_{n} (t) ∣$ and real limit calculus give $d_{ω} ([x (s)], [x (t)]) = ∣ s - t ∣$ . Thus $t \mapsto [x (t)]$ is an isometric embedding of $J$ .

step 2.1F1F2F3

3.2

Conversely let $z_{n} = γ_{n} (u_{n})$ be admissible points on $S_{n}$ and set $t_{n} = λ_{n} u_{n}$ . Then $∣ t_{n} ∣ = λ_{n} d_{n} (z_{n}, o_{n}) \leq λ_{n} d_{n} (z_{n}, e_{n}) + R$ is bounded, so $t = \lim_{ω} t_{n}$ exists. From $- a_{n} \leq t_{n} \leq b_{n}$ follows $t \in J$ , including the finite endpoint inequalities. Projection onto an interval satisfies $∣ t_{n} - c_{n} (t) ∣ \leq ∣ t_{n} - t ∣$ when $t_{n}$ lies in that interval (check $t$ below, in, or above it). Hence $λ_{n} d_{n} (z_{n}, x_{n} (t)) \to_{ω} 0$ and $[z] = [x (t)]$ .

step 1.1step 2.1F1F2algebra

4.1

If $a, b$ are finite, translate $J$ to $[0, a + b]$ ; if only one is infinite, translate and possibly reverse it to $[0, \infty)$ ; if both are infinite, $J = R$ . These are exactly the asserted interval, ray and line possibilities. When $a = b = 0$ , the image is one point.

step 3.1step 3.2F4

5.1

For any two ultralimit classes choose representative sequences $v_{n}, w_{n}$ . AC chooses a segment joining each pair. Take $o_{n} = v_{n}$ , so $a_{n} = 0$ and $b_{n} = λ_{n} d_{n} (v_{n}, w_{n})$ is uniformly bounded and has limit $d_{ω} ([v], [w])$ . step 3.1 and step 3.2 give a segment with exactly these endpoints, also if that distance is zero. Thus the ultralimit is geodesic.

step 3.1step 3.2F1F3F5∎

Depends on

Used by

Dependency tree · two levels

19 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

Drutu–Kapovich, Geometric Group Theory — §10.4 Lemmas 10.48 and 10.51, PDF pp.366–367 (standard reference, not scraped)