LemmaStatement: AI-adaptedProof: AI-generatedprecheck 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} \geq k$

Statement

Let $n : N \to 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_{σ (i)}$ for every $i \in N$ , then $n$ is strictly increasing.
Growth. If $n$ is strictly increasing then $n_{k} \geq k$ for every $k \in 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 : N \to N$ , written $k \mapsto n_{k}$ , with $σ$ the successor and the order of Order on the natural numbers; claim 1 is proved under the standing assumption that $n_{i} < n_{σ (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} \geq k$ .

[L1]

Order and successor on $N$ : $m \leq p$ means $m + i = p$ for some $i$ , so $0 \leq m$ for every $m$ because $0 + m = m$ ; and $σ (k) = k + 1$ with $σ (k) \neq k$ , so $k < σ (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 $σ (m) \leq p$ (Discreteness: $σ (n)$ is the immediate successor).

[L3]

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

[L4]

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

Proof

technique · induction

1.1baseA1L1L4

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

1.2ihA1

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

1.3baseA2L1

Base case for claim 2: $P (0)$ states $n_{0} \geq 0$ , which holds because $0 \leq m$ for every natural $m$ .

1.4ihA2

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

2.1step 1.2A1L2L4

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

2.2step 1.4A2L1L2L4

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

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

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.

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} \geq 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} \geq k \geq K$ whenever $k \geq K$ .
Nothing here is about $R$ ; both claims are about $(N, \leq, σ)$ 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} \geq 0$ true ([L1], step 1.3); discreteness (Discreteness: $σ (n)$ is the immediate successor, [L2]), which upgrades $k < n_{σ (k)}$ to $σ (k) \leq n_{σ (k)}$ (step 2.2); and transitivity in its mixed form, which composes $k \leq n_{k}$ with $n_{k} < n_{σ (k)}$ into $k < n_{σ (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: $(Z, \leq)$ is discrete in the same sense, $m < p$ iff $m + 1 \leq p$ , yet $k \mapsto k - 1$ is strictly increasing on $Z$ with $n_{k} < k$ everywhere. What $Z$ lacks is a least element to anchor the induction. A least element alone is not enough either, which is what fails over $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.

A strictly increasing index map satisfies $n_{k} \geq k$

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

A strictly increasing index map satisfies nk≥knk​≥k

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

A strictly increasing index map satisfies $n_{k} \geq k$