ExampleConstruction: AI-adaptedVerification: 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.

Scaling distinguishes sublinear minsize from a fixed perimeter cutoff

Example

Let $X$ be a nonempty geodesic metric space with $m_{X} (P) = o (P)$ . If $λ_{n} > 0$ tends to zero and $P_{n} \geq 0$ with $\sup_{n} λ_{n} P_{n} < \infty$ , then $λ_{n} m_{X} (P_{n}) \to 0$ . A fixed bound on the unscaled perimeters also forces vanishing after rescaling, even without sublinearity, but gives no conclusion for perimeters of order $1 / λ_{n}$ . The Euclidean right triangles of scale $n + 1$ at $λ_{n} = 1 / (n + 1)$ display this distinction for every $n \in N$ , including $n = 0$ .

Facts & Assumptions

Given: Fix positive scales tending to zero; for the first assertion assume the displayed sublinearity and bounded rescaled perimeters.

[F1]

For perimeter at most $P$ , every admissible side triple has diameter at most $P$ , so $0 \leq m_{X} (P) \leq P$ . (Real trees, tripod triangles, slimness and minsize).

[F2]

An ordinarily convergent bounded real sequence has that value as its ultralimit for every free ultrafilter. (Free tail ultrafilters and bounded real ultralimit calculus).

[F3]

The Euclidean distance on $R^{2}$ is the square root of the sum of squared coordinate differences. ( $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it).

[F4]

Nonnegative square roots exist and are unique, including $\sqrt{2} > 0$ . (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

Verification

technique · direct

1.1

Put $H = \sup_{n} λ_{n} P_{n} < \infty$ . Given $ε > 0$ , sublinearity supplies $P_{0} > 0$ with $m_{X} (P) \leq ε P$ whenever $P \geq P_{0}$ . For $P < P_{0}$ , F1 gives $m_{X} (P) \leq P_{0}$ . Separating these cases for each $P_{n}$ yields the single bound $0 \leq λ_{n} m_{X} (P_{n}) \leq ε λ_{n} P_{n} + λ_{n} P_{0} \leq ε H + λ_{n} P_{0} .$ There is no assumption that $P_{n}$ tends to infinity.

givenF1

1.2

For each $n \in N$ in $R^{2}$ , take vertices $(0, 0), (n + 1, 0), (0, n + 1)$ . The axis-side parameterizations $(u, 0)$ and $(0, u)$ for $0 \leq u \leq n + 1$ have distance $∣ u - v ∣$ . The third parameterization $(u / \sqrt{2}, n + 1 - u / \sqrt{2})$ for $0 \leq u \leq (n + 1) \sqrt{2}$ has squared distance $2 ((u - v) / \sqrt{2})^{2} = (u - v)^{2}$ . Thus these really are geodesic triangles and their perimeters are $P_{n} = (2 + \sqrt{2}) (n + 1)$ .

F3F4

2.1

To make the last expression less than any $η > 0$ , first take $ε = η / (2 (H + 1))$ , obtain its $P_{0}$ , and then take $n$ so large that $λ_{n} P_{0} < η / 2$ . This proves ordinary convergence to zero, and also ultralimit zero for any free ultrafilter by F2. If instead $P_{n} \leq M$ for a fixed finite $M$ , the simpler bound $0 \leq λ_{n} m_{X} (P_{n}) \leq λ_{n} M \to 0$ works without sublinearity.

step 1.1F1F2

3.1

For any triple $p = (u, 0)$ , $q = (0, v)$ , $r = (t, n + 1 - t)$ on these sides, the diameter is at least $\max (n + 1 - t, t) \geq (n + 1) / 2$ : the two terms are lower bounds for $d (p, r)$ and $d (q, r)$ respectively. Conversely the triple $(0, 0), (0, 0), (n + 1, 0)$ has diameter $n + 1$ . At $λ_{n} = 1 / (n + 1)$ the rescaled minsize of these triangles therefore lies in $[1 / 2, 1]$ , and their rescaled perimeter is the constant $2 + \sqrt{2}$ . They do not vanish, whereas any fixed triangle in the very same plane has both its perimeter and its minsize multiplied by $1 / (n + 1)$ and tending to zero. This is the claimed witness that controlling only a fixed unscaled perimeter cutoff cannot establish sublinear behavior at the moving scale.

F1F3F4step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

39 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 pp. 443–445; explicit scaling calculation and independent Euclidean witness (standard reference, not scraped)