LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)

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.

A strictly increasing index map satisfies $n_k \ge k$

Statement

Let $n : \mathbb{N} \to \mathbb{N}$ be a function, written $k \mapsto n_k$ , and recall that $n$ is strictly increasing when $n_j < n_k$ whenever $j < k$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Order on the natural numbers).

Consecutive comparisons suffice. If $n_i < n_{\sigma(i)}$ for every $i \in \mathbb{N}$ , then $n$ is strictly increasing.
Growth. If $n$ is strictly increasing then $n_k \ge k$ for every $k \in \mathbb{N}$ .

Claim 1 is what one checks in practice when exhibiting a subsequence; claim 2 is what every later subsequence argument uses.

Facts & Assumptions

Given: A function $n : \mathbb{N} \to \mathbb{N}$ , written $k \mapsto n_k$ , with $\sigma$ the successor and the order of Order on the natural numbers; claim 1 is proved under the standing assumption that $n_i < n_{\sigma(i)}$ for every $i$ , and claim 2 under the standing assumption that $n$ is strictly increasing (Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[A1]

$Q(k)$ denotes the statement: $n_j < n_k$ for every $j < k$ .

[A2]

$P(k)$ denotes the statement: $n_k \ge k$ .

[L1]

Order and successor on $\mathbb{N}$ : $m \le p$ means $m + i = p$ for some $i$ , so $0 \le m$ for every $m$ because $0 + m = m$ ; and $\sigma(k) = k + 1$ with $\sigma(k) \ne k$ , so $k < \sigma(k)$ (Order on the natural numbers, Addition of natural numbers, Left identity for addition, No natural number equals its own successor).

[L2]

Discreteness: $m < p$ if and only if $\sigma(m) \le p$ (Discreteness: $\sigma(n)$ is the immediate successor).

[L3]

Induction principle: if $R(0)$ holds and $R(k)$ implies $R(\sigma(k))$ for every $k$ , then $R(k)$ holds for every $k \in \mathbb{N}$ (The principle of mathematical induction).

[L4]

The order on $\mathbb{N}$ is reflexive, antisymmetric, transitive and total, and satisfies trichotomy ( $\le$ is a linear order on $\mathbb{N}$ , Trichotomy of the order on $\mathbb{N}$ ).

Proof

technique · induction

1.1

Base case for claim 1: $Q(0)$ holds vacuously, since no $j$ satisfies $j < 0$ ; indeed $0 \le j$ always holds, and $j < 0$ together with $0 \le j$ would contradict antisymmetry.

baseA1L1L4

1.2

Inductive hypothesis for claim 1: fix $k \in \mathbb{N}$ and assume $Q(k)$ , that is $n_j < n_k$ for every $j < k$ .

ihA1

1.3

Base case for claim 2: $P(0)$ states $n_0 \ge 0$ , which holds because $0 \le m$ for every natural $m$ .

baseA2L1

1.4

Inductive hypothesis for claim 2: fix $k \in \mathbb{N}$ and assume $P(k)$ , that is $k \le n_k$ .

ihA2

2.1

Inductive step for claim 1: let $j < \sigma(k)$ . By trichotomy either $k < j$ , or $j = k$ , or $j < k$ . The case $k < j$ is impossible, since it gives $\sigma(k) \le j$ by [L2], which together with $j < \sigma(k)$ contradicts antisymmetry. If $j = k$ then $n_j = n_k < n_{\sigma(k)}$ by the standing assumption. If $j < k$ then $n_j < n_k$ by step 1.2 and $n_k < n_{\sigma(k)}$ by the standing assumption, so $n_j < n_{\sigma(k)}$ by transitivity. In every admissible case $n_j < n_{\sigma(k)}$ , so $Q(\sigma(k))$ holds.

step 1.2A1L2L4

2.2

Inductive step for claim 2: $k < \sigma(k)$ by [L1], so strict increase gives $n_k < n_{\sigma(k)}$ ; combined with $k \le n_k$ from step 1.4 this yields $k < n_{\sigma(k)}$ , hence $\sigma(k) \le n_{\sigma(k)}$ by [L2], which is $P(\sigma(k))$ .

step 1.4A2L1L2L4

3.1

Both inductions are complete, so by the induction principle $Q(k)$ holds for every $k$ , which is claim 1, and $P(k)$ holds for every $k$ , which is claim 2.

step 1.1step 1.3step 2.1step 2.2L3discharge-induction∎

Remarks

Claim 2 is sharp: the identity map $n_k = k$ is strictly increasing with $n_k = k$ throughout, so no better bound than $n_k \ge k$ holds for all strictly increasing index maps.
Claim 2 is exactly what makes a subsequence inherit a limit (Subsequences inherit the limit): a threshold $K$ that works for the original sequence works unchanged for the subsequence, because $n_k \ge k \ge K$ whenever $k \ge K$ .
Nothing here is about $\mathbb{R}$ ; both claims are about $(\mathbb{N}, \le, \sigma)$ alone. Both are proved by induction ([L3]), and that is the method, not an order property. Claim 2 needs three order facts on top of the induction: that $0$ is least, which is what makes its base case $n_0 \ge 0$ true ([L1], step 1.3); discreteness (Discreteness: $\sigma(n)$ is the immediate successor, [L2]), which upgrades $k < n_{\sigma(k)}$ to $\sigma(k) \le n_{\sigma(k)}$ (step 2.2); and transitivity in its mixed form, which composes $k \le n_k$ with $n_k < n_{\sigma(k)}$ into $k < n_{\sigma(k)}$ ([L4], step 2.2). Claim 1 additionally uses trichotomy and antisymmetry ([L4]).
Of those three, neither the least element nor discreteness may be dropped. Discreteness alone is not enough: $(\mathbb{Z}, \le)$ is discrete in the same sense, $m < p$ iff $m + 1 \le p$ , yet $k \mapsto k - 1$ is strictly increasing on $\mathbb{Z}$ with $n_k < k$ everywhere. What $\mathbb{Z}$ lacks is a least element to anchor the induction. A least element alone is not enough either, which is what fails over $\mathbb{Q}$ : on the nonnegative rationals $x \mapsto x/2$ is strictly increasing and fixes the least element $0$ , but $x/2 < x$ at every positive rational.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 42 results over 14 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

CMU 21-269 notes, Compactness — subsequences (standard reference, not scraped)
University of Wisconsin Math 521, Homework 5 (standard reference, not scraped)
Subsequence (Wikipedia) (standard reference, not scraped)
Mathematical induction (Wikipedia) (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §6.6 (standard reference, not scraped)

A strictly increasing index map satisfies nk≥kn_k \ge knk​≥k