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.

Tree cones force uniform control of sides with a common endpoint

Statement

Assume AC and fix a free ultrafilter $ω$ . Let $X$ be geodesic and suppose ${Cone}_{ω} (X, e, λ)$ is a real tree for every basepoint sequence and every positive ordinary-null scale sequence. There exists $M > 0$ such that, for every $x, y, z$ and all choices of the two segments,

$d (y, z) > 1 ⟹ d_{H} ([x, y], [x, z]) \leq M d (y, z) .$

Facts & Assumptions

Given: A geodesic X with the stated all-basepoint/all-scale tree-cone hypothesis for fixed free omega; AC.

[F1]

Every represented point on a sequence of sides belongs to its parameterized interval, ray or line limit. (Limits of geodesic segments, rays and lines).

[F2]

Finite side distances attain extrema; in a tree finite-Hausdorff rays of common origin and finite-Hausdorff lines coincide. (Triangle extrema and the tripod and branch rules for real trees).

[F3]

AC permits selection of countably many violating triangles and nearest points. (The Axiom of Choice).

Proof

technique · direct

1.1

If no such $M$ exists, for each $n \geq 1$ select two sides with $q_{n} = d (y_{n}, z_{n}) > 1$ and $D_{n} = d_{H} ([x_{n}, y_{n}], [x_{n}, z_{n}]) > n q_{n}$ . Extrema exist on the finite sides. Exchange the endpoint names when necessary and select $a_{n} \in [x_{n}, y_{n}]$ attaining $d (a_{n}, [x_{n}, z_{n}]) = D_{n}$ . Select a nearest point $b_{n}$ on the other side. AC supplies these countable choices.

F2F3

2.1

Base at $a_{n}$ and scale by $1 / D_{n}$ . Since $D_{n} > n$ , the scales tend to zero ordinarily, so the cone is a real tree. Both sides meet its bounded basepoint neighbourhood, at $a_{n}$ and $b_{n}$ . Each point on either side has a point on the other within $D_{n}$ . For any bounded represented sequence, such nearest points are bounded by the triangle inequality. Thus their limit images $S, T$ satisfy $d_{H} (S, T) \leq 1$ and $d (a, T) = 1$ , where $a = [a_{n}]$ : every represented point of $T$ has distance at least one from $a$ , and $[b_{n}]$ attains one.

step 1.1F1F2F3

3.1

The rescaled distances of $y_{n}, z_{n}$ from $a_{n}$ differ by at most $q_{n} / D_{n} < 1 / n$ . They therefore are both finite in the extended ultralimit or both infinite; in the finite case their classes are equal. The common endpoint $x_{n}$ likewise either has finite rescaled distance or escapes. Finite values can be made uniformly bounded by replacing coordinates off a large set; endpoint distance limits classify the side domains by [F1].

step 1.1step 2.1F1

4.1

If both ends are finite, $S, T$ are segments with the same two endpoints and coincide by tree uniqueness. If precisely one end is finite, $S, T$ are rays with the same finite endpoint and finite Hausdorff distance, so coincide. If both ends escape, they are lines at finite Hausdorff distance, so again coincide. These cases exhaust the endpoint limits, and every case contradicts $a \in S$ and $d (a, T) = 1$ . Hence the asserted finite $M$ exists; enlarging it if necessary makes it positive.

step 2.1step 3.1F1F2∎

Depends on

Used by

Tree cones at all basepoints and scales imply uniform slimness Theorem

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

Drutu–Kapovich, Geometric Group Theory — §11.20 Lemma 11.168(a), PDF p.443 (standard reference, not scraped)