TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)

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.

Every list of $m n + 1$ pairwise distinct reals has a strictly increasing sublist of length $m + 1$ or a strictly decreasing sublist of length $n + 1$

Statement

Let $m, n \in N$ and let $a : (m n + 1) \to R$ be a pairwise distinct finite list of reals of length $m n + 1$ (A finite list of reals, and its strictly increasing and strictly decreasing sublists). Then $a$ has a strictly increasing sublist of length $m + 1$ or a strictly decreasing sublist of length $n + 1$ .

The length $m n + 1$ is at least $1$ for all $m$ and $n$ , so the statement has content at every pair of indices. At $m = 0$ the list has one term and the required increasing sublist has length $1$ , which the single position supplies; at $n = 0$ the same reading holds for the decreasing sublist, and the increasing one of length $1$ is also available.

Facts & Assumptions

Given: Naturals $m$ and $n$ , the length $N : = m n + 1$ , and a pairwise distinct list $a : N \to R$ . For $i < N$ and $L \geq 1$ , call $s : L \to N$ an increasing run ending at $i$ when $s$ is a strictly increasing sublist of $a$ (in both senses of A finite list of reals, and its strictly increasing and strictly decreasing sublists) with $s (L - 1) = i$ , and define a decreasing run ending at $i$ in the same way with the values strictly decreasing.

[L1]

A nonempty subset of $N$ with an upper bound has a greatest element. Let $E \subseteq N$ be nonempty with $E \subseteq σ (M)$ for some $M$ . Every $e \in E$ then satisfies $e \leq M$ by On $N$ the order is membership: $m < n ⟺ m \in n$ , so the set $C : = {c \in N : e \leq c for every e \in E}$ contains $M$ and has a least element $c_{0}$ by The well-ordering principle. If $c_{0} \notin E$ then every $e \in E$ satisfies $e \leq c_{0}$ and $e \neq c_{0}$ , hence $e < c_{0}$ and $σ (e) \leq c_{0}$ by Discreteness: $σ (n)$ is the immediate successor; since $E$ is nonempty, $c_{0} \neq 0$ , so $c_{0} = σ (c_{1})$ for some $c_{1}$ (Every nonzero natural number is a successor) and $e \leq c_{1}$ for every $e \in E$ , putting $c_{1} \in C$ below $c_{0}$ and contradicting minimality. So $c_{0} \in E$ and $c_{0}$ is the greatest element of $E$ .

[L2]

For every $i < N$ there is an increasing run and a decreasing run ending at $i$ , both of length $1$ : take $s : 1 \to N$ with $s (0) = i$ , which is vacuously monotone in both senses (A finite list of reals, and its strictly increasing and strictly decreasing sublists).

[L3]

Every run has length at most $N$ : a run of length $L$ is injective into $N$ , and there is no injection of $L$ into $N$ when $N < L$ (The pigeonhole principle on $N$ , clause 2, Injection, surjection, bijection, A finite list of reals, and its strictly increasing and strictly decreasing sublists).

[L4]

Order facts in $N$ : $k < N ⟺ k \in N$ , $N = {k : k < N}$ and $k < σ (M) ⟺ k \leq M$ (On $N$ the order is membership: $m < n ⟺ m \in n$ , Order on the natural numbers, The natural numbers $N$ (von Neumann)); exactly one of $p < q$ , $p = q$ , $q < p$ holds (Trichotomy of the order on $N$ ); $p < q ⟺ σ (p) \leq q$ (Discreteness: $σ (n)$ is the immediate successor); every nonzero natural is a successor (Every nonzero natural number is a successor); and the truncated difference of Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ , for which $1 \leq L$ gives $(L - 1) + 1 = L$ .

[L5]

$∣ m \times n ∣ = m n$ and $∣ N ∣ = N$ (The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ , clause 1, The cardinality $∣ A ∣$ of a finite set); and there is no injection $σ (K) \to K$ for any $K \in N$ (The pigeonhole principle on $N$ , clause 1). A bijection $m \times n \to m n$ exists because the two sets have the same cardinality (The cardinality $∣ A ∣$ of a finite set, clause (d)).

[L6]

$R$ is an ordered field, so its order is total and $a_{i} \neq a_{j}$ gives $a_{i} < a_{j}$ or $a_{i} > a_{j}$ (Ordered field, Field).

Proof

technique · contradiction

1.1

If $m = 0$ or $n = 0$ , then $N = m n + 1 = 1$ , and the one-term sublist ending at $0$ supplied by [L2] has the required length $1 = m + 1$ or $1 = n + 1$ , respectively. Hence assume $m, n \geq 1$ and suppose, for contradiction, that $a$ has neither required sublist.

L2casesassume-contra

1.2

The two run lengths. For $i < N$ let $I n c (i)$ be the set of lengths of increasing runs ending at $i$ and $D e c (i)$ the set of lengths of decreasing runs ending at $i$ . Both are nonempty by [L2] and both are contained in $σ (N)$ by [L3] and [L4], so both have a greatest element by [L1]; write $i n c (i)$ and $d e c (i)$ for those greatest elements. Both are at least $1$ .

L1L2L3L4construct

2.1

The bound imposed by the supposition. If some $i n c (i)$ were at least $m + 1$ , truncating a longest increasing run ending at $i$ to its first $m + 1$ positions would give a strictly increasing sublist of length $m + 1$ ; so $i n c (i) \leq m$ for every $i < N$ by [L4], and likewise $d e c (i) \leq n$ . Combined with $i n c (i) \geq 1$ and $d e c (i) \geq 1$ from step 1.2, this gives $i n c (i) - 1 < m$ and $d e c (i) - 1 < n$ , so the map $Φ (i) : = (i n c (i) - 1, d e c (i) - 1)$ sends $N$ into $m \times n$ .

step 1.1step 1.2L4construct

2.2

Extending a run. Let $i < j < N$ . If $a_{i} < a_{j}$ and $s$ is an increasing run of length $L : = i n c (i)$ ending at $i$ , then $s^{'} : L + 1 \to N$ defined by $s^{'} ⁣ ↾ ⁣ L : = s$ and $s^{'} (L) : = j$ is again a strictly increasing sublist: its indices increase because $s (L - 1) = i < j$ , and its values increase because $a_{s (p)} < a_{s (L - 1)} = a_{i} < a_{j}$ for $p < L - 1$ . So $L + 1 \in I n c (j)$ and $i n c (j) \geq L + 1 > i n c (i)$ . Symmetrically, if $a_{i} > a_{j}$ then $d e c (j) > d e c (i)$ .

step 1.2L4L6construct

3.1

$Φ$ is injective. Let $i < j < N$ ; since $a$ is pairwise distinct, $a_{i} \neq a_{j}$ , so $a_{i} < a_{j}$ or $a_{i} > a_{j}$ by [L6]. In the first case step 2.2 gives $i n c (i) \neq i n c (j)$ , in the second $d e c (i) \neq d e c (j)$ ; either way $Φ (i) \neq Φ (j)$ , because both run lengths are at least $1$ , so $i n c (i) = (i n c (i) - 1) + 1$ by [L4] and equal first coordinates would force equal run lengths, and likewise for the second coordinate. As $i$ and $j$ were an arbitrary pair of distinct indices, $Φ$ is injective.

step 2.1step 2.2L4L6

4.1

The contradiction. Composing $Φ$ with a bijection $m \times n \to m n$ from [L5] gives an injection of $N = σ (m n)$ into $m n$ , which [L5] forbids. So the supposition of step 1.1 is untenable, and $a$ has a strictly increasing sublist of length $m + 1$ or a strictly decreasing sublist of length $n + 1$ .

step 2.1step 3.1L5discharge-contradiction∎

Remarks

Where pairwise distinctness is spent. Only in step 3.1, to force one of the two strict comparisons between $a_{i}$ and $a_{j}$ . Without it a list may repeat a value, and then two positions carrying that value force neither run length to increase.
Why a greatest element exists at all. The lengths of runs ending at a fixed position form a nonempty set of naturals bounded by the length of the list, and a nonempty bounded set of naturals has a greatest element; that is derived in the facts from the well-ordering principle alone. No maximum of a finite set of reals is involved, and no choice principle is used, since $i n c (i)$ and $d e c (i)$ are determined by $i$ rather than selected.
The bound $m n + 1$ is not improvable, and the witness is a list of $m n$ distinct reals with neither long sublist; it is constructed in For all $m$ and $n$ there is a list of $m n$ pairwise distinct reals with no strictly increasing sublist of length $m + 1$ and no strictly decreasing sublist of length $n + 1$ .

Depends on

Used by

Dependency tree · two levels

42 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

Erdos-Szekeres theorem (Wikipedia) (standard reference, not scraped)
Pigeonhole principle (Wikipedia) (standard reference, not scraped)
Longest increasing subsequence (Wikipedia) (standard reference, not scraped)
Morris, Combinatorics: The Pigeonhole Principle (LibreTexts) (standard reference, not scraped)

Every list of mn+1mn+1 pairwise distinct reals has a strictly increasing sublist of length m+1m+1 or a strictly decreasing sublist of length n+1n+1