LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 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.

Growth comparison is a preorder

Statement

On nondecreasing functions $N \to N$ , the relation $≼$ of Growth comparison and growth type is reflexive and transitive. Consequently $≃$ is an equivalence relation.

Facts & Assumptions

Given: Nondecreasing functions $f, g, h : N \to N$ .

[L1]

The relation $f ≼ g$ means that some natural number $C \geq 1$ satisfies $f (n) \leq C g (C n + C) + C$ for every $n \in N$ , and $f ≃ g$ means both $f ≼ g$ and $g ≼ f$ (Growth comparison and growth type).

Proof

technique · direct

1.1L1given

Reflexivity holds with $C = 1$ , since $f (n) \leq f (n + 1) + 1$ for every $n$ and $f$ is nondecreasing. So $f ≼ f$ .

1.2L1givenalgebra

Suppose $f ≼ g$ via $C_{1}$ and $g ≼ h$ via $C_{2}$ . Put $C : = C_{1} C_{2} + C_{1} + C_{2}$ , which is again a natural number with $C \geq 1$ . Then $f (n) \leq C_{1} g (C_{1} n + C_{1}) + C_{1} \leq C_{1} C_{2} h (C_{2} (C_{1} n + C_{1}) + C_{2}) + C_{1} C_{2} + C_{1} + C_{2}$ , and the argument of $h$ is at most $C n + C$ . Since $h$ is nondecreasing and $C \geq C_{1} C_{2}$ , this gives $f (n) \leq C h (C n + C) + C$ for every $n$ . Hence $f ≼ h$ .

2.1L1step 1.1step 1.2∎

Steps 1.1 and 1.2 make $≼$ a preorder. The relation $≃$ is therefore an equivalence relation by definition.

Depends on

Growth comparison and growth type

Used by

Polynomial, subexponential, exponential, and intermediate growth Definition

Dependency tree · two levels

2 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

C. Löh, Geometric Group Theory, Sections 5.1-5.3 (standard reference, not scraped)
C. Drutu and M. Kapovich, Lectures on Geometric Group Theory, Chapter 5 (standard reference, not scraped)