TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 $mn+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 \mathbb{N}$ and let $a : (mn+1) \to \mathbb{R}$ be a pairwise distinct finite list of reals of length $mn+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 $mn+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 := mn+1$ , and a pairwise distinct list $a : N \to \mathbb{R}$ . For $i < N$ and $L \ge 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 $\mathbb{N}$ with an upper bound has a greatest element. Let $E \subseteq \mathbb{N}$ be nonempty with $E \subseteq \sigma(M)$ for some $M$ . Every $e\in E$ then satisfies $e\le M$ by On $\mathbb{N}$ the order is membership: $m < n \iff m \in n$ , so the set $C := \{\, c \in \mathbb{N} : e \le c \text{ 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 \le c_0$ and $e \ne c_0$ , hence $e < c_0$ and $\sigma(e) \le c_0$ by Discreteness: $\sigma(n)$ is the immediate successor; since $E$ is nonempty, $c_0 \ne 0$ , so $c_0 = \sigma(c_1)$ for some $c_1$ (Every nonzero natural number is a successor) and $e \le 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 $\mathbb{N}$ , clause 2, Injection, surjection, bijection, A finite list of reals, and its strictly increasing and strictly decreasing sublists).

[L4]

Order facts in $\mathbb{N}$ : $k < N \iff k \in N$ , $N = \{k : k<N\}$ and $k < \sigma(M) \iff k \le M$ (On $\mathbb{N}$ the order is membership: $m < n \iff m \in n$ , Order on the natural numbers, The natural numbers $\mathbb{N}$ (von Neumann)); exactly one of $p<q$ , $p=q$ , $q<p$ holds (Trichotomy of the order on $\mathbb{N}$ ); $p<q \iff \sigma(p) \le q$ (Discreteness: $\sigma(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 $\mathbb{N}$ , for which $1 \le L$ gives $(L-1)+1 = L$ .

[L5]

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

[L6]

$\mathbb{R}$ is an ordered field, so its order is total and $a_i \ne 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=mn+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\ge1$ and suppose, for contradiction, that $a$ has neither required sublist.

L2casesassume-contra

1.2

The two run lengths. For $i < N$ let $\mathrm{Inc}(i)$ be the set of lengths of increasing runs ending at $i$ and $\mathrm{Dec}(i)$ the set of lengths of decreasing runs ending at $i$ . Both are nonempty by [L2] and both are contained in $\sigma(N)$ by [L3] and [L4], so both have a greatest element by [L1]; write $\mathrm{inc}(i)$ and $\mathrm{dec}(i)$ for those greatest elements. Both are at least $1$ .

L1L2L3L4construct

2.1

The bound imposed by the supposition. If some $\mathrm{inc}(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 $\mathrm{inc}(i) \le m$ for every $i < N$ by [L4], and likewise $\mathrm{dec}(i) \le n$ . Combined with $\mathrm{inc}(i) \ge 1$ and $\mathrm{dec}(i) \ge 1$ from step 1.2, this gives $\mathrm{inc}(i)-1 < m$ and $\mathrm{dec}(i)-1 < n$ , so the map $\Phi(i) := \big(\mathrm{inc}(i)-1,\ \mathrm{dec}(i)-1\big)$ 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 := \mathrm{inc}(i)$ ending at $i$ , then $s' : L+1 \to N$ defined by $s'\!\restriction\!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 \mathrm{Inc}(j)$ and $\mathrm{inc}(j) \ge L+1 > \mathrm{inc}(i)$ . Symmetrically, if $a_i > a_j$ then $\mathrm{dec}(j) > \mathrm{dec}(i)$ .

step 1.2L4L6construct

3.1

$\Phi$ is injective. Let $i < j < N$ ; since $a$ is pairwise distinct, $a_i \ne a_j$ , so $a_i < a_j$ or $a_i > a_j$ by [L6]. In the first case step 2.2 gives $\mathrm{inc}(i) \ne \mathrm{inc}(j)$ , in the second $\mathrm{dec}(i) \ne \mathrm{dec}(j)$ ; either way $\Phi(i) \ne \Phi(j)$ , because both run lengths are at least $1$ , so $\mathrm{inc}(i) = (\mathrm{inc}(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, $\Phi$ is injective.

step 2.1step 2.2L4L6

4.1

The contradiction. Composing $\Phi$ with a bijection $m \times n \to mn$ from [L5] gives an injection of $N = \sigma(mn)$ into $mn$ , 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 $\mathrm{inc}(i)$ and $\mathrm{dec}(i)$ are determined by $i$ rather than selected.
The bound $mn+1$ is not improvable, and the witness is a list of $mn$ distinct reals with neither long sublist; it is constructed in For all $m$ and $n$ there is a list of $mn$ 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 65 results over 25 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

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+1mn+1 pairwise distinct reals has a strictly increasing sublist of length m+1m+1m+1 or a strictly decreasing sublist of length n+1n+1n+1