CounterexampleConstruction: AI-adaptedVerification: 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.

A list of six distinct reals with no strictly increasing sublist of length four and no strictly decreasing sublist of length three

Statement refuted

Refuted claim: FALSE: every list of $m n$ pairwise distinct reals has a strictly increasing sublist of length $m + 1$ or a strictly decreasing sublist of length $n + 1$ at $m = 3$ and $n = 2$ , that is, the assertion that every pairwise distinct list of $m n = 6$ reals has a strictly increasing sublist of length $m + 1 = 4$ or a strictly decreasing sublist of length $n + 1 = 3$ .

The witness is the list $a : 6 \to R$ with values

$(a_{0}, a_{1}, a_{2}, a_{3}, a_{4}, a_{5}) = (ι (2), ι (1), ι (4), ι (3), ι (6), ι (5)),$

that is $2, 1, 4, 3, 6, 5$ read through the canonical natural (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field). It is the instance at $m = 3$ , $n = 2$ of the construction of 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$ : three blocks of two positions each, decreasing inside a block and increasing across blocks.

Its longest strictly increasing sublist has length $3$ , for example $a_{0}, a_{2}, a_{4}$ , and its longest strictly decreasing sublist has length $2$ , for example $a_{0}, a_{1}$ .

Facts & Assumptions

Given: The list $a : 6 \to R$ above, and the three index blocks $P_{0} : = {0, 1}$ , $P_{1} : = {2, 3}$ , $P_{2} : = {4, 5}$ , with $b l k (i) : = b$ for $i \in P_{b}$ .

[L1]

A sublist of length $L$ is a strictly increasing $s : L \to 6$ . It is strictly increasing when $a_{s (p)} < a_{s (q)}$ for every $p < q < L$ , and strictly decreasing when $a_{s (p)} > a_{s (q)}$ for every such pair (A finite list of reals, and its strictly increasing and strictly decreasing sublists, Injection, surjection, bijection).

[L2]

$ι$ is strictly increasing, so the comparisons between the six values are those between $1, 2, 3, 4, 5, 6$ in $N$ ; natural order satisfies trichotomy, so distinct indices can be put in increasing order and $K < L$ fails exactly when $L \leq K$ (Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ , clause 7, Ordered field, Order on the natural numbers, Trichotomy of the order on $N$ ).

[L3]

If a finite set $S$ has $∣ S ∣ = K < L$ , there is no injection $L \to S$ : composing one with a bijection $S \to K$ supplied by finite cardinality would contradict the natural-number pigeonhole principle (The cardinality $∣ A ∣$ of a finite set, Injection, surjection, bijection, The pigeonhole principle on $N$ , clause 2).

[L4]

Counterexample

technique · constructive

1.1

The list is pairwise distinct: its values are $ι (2), ι (1), ι (4), ι (3), ι (6), ι (5)$ , and the naturals $1, 2, 3, 4, 5, 6$ are pairwise distinct, so their canonical naturals are too by [L2].

givenL2construct

1.2

Inside a block the values decrease. $a_{0} = ι (2) > ι (1) = a_{1}$ , $a_{2} = ι (4) > ι (3) = a_{3}$ and $a_{4} = ι (6) > ι (5) = a_{5}$ , by [L2].

givenL2

1.3

Across blocks the values increase. Every value at a position of $P_{0}$ is $ι (1)$ or $ι (2)$ , every value at a position of $P_{1}$ is $ι (3)$ or $ι (4)$ , and every value at a position of $P_{2}$ is $ι (5)$ or $ι (6)$ ; so $b < b^{'}$ implies that every value on $P_{b}$ is smaller than every value on $P_{b^{'}}$ , by [L2]. Also $i < i^{'}$ implies $b l k (i) \leq b l k (i^{'})$ , since the blocks list the positions in increasing order.

givenL2

2.1

No strictly increasing sublist of length $4$ . Let $s : L \to 6$ be a strictly increasing sublist. If $p < q < L$ had $b l k (s (p)) = b l k (s (q))$ , then $s (p) < s (q)$ lie in one block, so $a_{s (p)} > a_{s (q)}$ by step 1.2, contradicting that the values increase. Natural trichotomy in [L2] makes this sufficient for $b l k \circ s$ to be an injection of $L$ into $3$ ; [L3] and [L2] then give $L \leq 3$ , hence $L \neq 4$ .

step 1.2L1L2L3

2.2

No strictly decreasing sublist of length $3$ . Let $s : L \to 6$ be a strictly decreasing sublist and let $p < q < L$ . Then $s (p) < s (q)$ , so $b l k (s (p)) \leq b l k (s (q))$ by step 1.3; and a strict inequality there would give $a_{s (p)} < a_{s (q)}$ by step 1.3, contradicting that the values decrease. So all positions of $s$ lie in one block, and $s$ is an injection of $L$ into a two-element set; [L3] and natural trichotomy in [L2] give $L \leq 2$ , hence $L \neq 3$ .

step 1.3L1L2L3

3.1

The list of step 1.1 is therefore a pairwise distinct list of $6 = 3 \cdot 2$ reals with neither of the two sublists the refuted claim asserts, so that claim is false at $m = 3$ , $n = 2$ ; what holds instead is [L4] at length $3 \cdot 2 + 1 = 7$ .

step 1.1step 2.1step 2.2L4discharge-construct∎

Remarks

The two bounds come from the two block counts. An increasing sublist takes at most one position from each block, so its length is bounded by the number of blocks; a decreasing sublist stays inside one block, so its length is bounded by the block size. Exchanging the roles of the block count and the block size would give a witness for the pair $(2, 3)$ instead.
Both bounds are attained, by $a_{0}, a_{2}, a_{4}$ and by $a_{0}, a_{1}$ respectively, so the witness is not merely short of the two thresholds: it sits exactly one below each.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

46 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)
Longest increasing subsequence (Wikipedia) (standard reference, not scraped)