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.
For all and there is a list of pairwise distinct reals with no strictly increasing sublist of length and no strictly decreasing sublist of length
Statement
Let . Then there is a pairwise distinct finite list of reals (A finite list of reals, and its strictly increasing and strictly decreasing sublists) with no strictly increasing sublist of length and no strictly decreasing sublist of length .
Together with the bound , this says that is the least length at which the two alternatives become unavoidable.
At or the list is empty, and there is no sublist of any positive length at all, so the assertion holds for the trivial reason that both required sublists have length at least .
Facts & Assumptions
Given: Naturals and , the finite sets and , and the ordered field with the canonical natural (The canonical natural of a field).
Arithmetic and order of : addition and multiplication are as in Addition of natural numbers and Multiplication of natural numbers; means for a unique , written (Order on the natural numbers, Addition is cancellative, Finite sums and finite products of natural numbers, and in ), and is transitive ( is a linear order on ); if and only if (Discreteness: is the immediate successor); (Order is compatible with addition); addition is commutative (Addition is commutative); (Distributivity and the successor law for multiplication); multiplication is monotone in its first factor, since gives by commutativity and distributivity (Multiplication is commutative, Distributivity and the successor law for multiplication), so implies ; exactly one of , , holds (Trichotomy of the order on ); and (On the order is membership: ).
and for a natural (The product rule: , and , clause 1, The cardinality of a finite set).
An injection between finite sets of equal cardinality is a bijection: it is a bijection onto its image, the image has the same cardinality as the domain, and clause 3 of A subset of a finite set is finite, with , and equality holds if and only if then makes the image the whole codomain (The cardinality of a finite set, Injection, surjection, bijection).
There is no injection of into when (The pigeonhole principle on , clause 2).
is strictly increasing, hence injective (Laws of finite sums and products in , and , clause 7); and is an ordered field (Ordered field, Field).
Sublists (A finite list of reals, and its strictly increasing and strictly decreasing sublists): a sublist of length is a strictly increasing , hence injective; it is strictly increasing, respectively decreasing, when its values do the same.
Proof
If or , then and the empty list has no sublist of the positive lengths and , proving the assertion in these boundary cases. Hence for the construction below assume .
The index bijection. Define by . Its values lie in : from and we get and , so by [L1], whence .
is injective. Suppose with . If then , so by [L1], a contradiction; symmetrically is impossible, so by [L1], and then by cancellation.
The list. By [L2] and [L3], the injection of step 1.3 is a bijection of onto , so every index is for exactly one pair, and defines a list . Write for the block of an index.
Inside a block the values decrease. Let and . Then by [L1], while and with , so and hence by [L1] and [L5].
Across blocks the values increase, and the block is monotone in the index. Let and . Then , the last step because ; so by [L5]. Moreover , by the computation of step 1.3; equivalently, is nondecreasing along the index order.
The list is pairwise distinct. Two indices with different blocks carry different values by step 3.2, and two indices in the same block carry different values by step 3.1; since every index has exactly one block by step 2.1, distinct indices carry distinct values.
No strictly increasing sublist of length . Let be a strictly increasing sublist. The map is injective: if had , then lie in one block, so by step 3.1, contradicting that the sublist increases. Hence by [L4] and natural-order trichotomy, so .
No strictly decreasing sublist of length . Let be a strictly decreasing sublist and let . Then , so by step 3.2; and would give by step 3.2, contradicting that the sublist decreases. Thus, if , all the lie in the block of , say , and is injective into because is injective and is a bijection. If , the empty map is already an injection . In either case [L4] and natural-order trichotomy give , so .
Together with the boundary cases in step 1.1, the list of step 2.1 is therefore a pairwise distinct list of reals with no strictly increasing sublist of length and no strictly decreasing sublist of length , which is the assertion.
Remarks
-
The two block counts are not interchangeable. The construction uses blocks of terms each. An increasing sublist meets each block at most once, so its length is bounded by the number of blocks, ; a decreasing sublist lies inside one block, so its length is bounded by the block size, . Exchanging the roles would bound the increasing sublists by and the decreasing ones by , which is the sharpness statement for the pair and not for .
-
Why the values are written through . The terms of a list of reals are real numbers, and is a natural number, which is a set and not an element of . The strict monotonicity of is what transports the comparisons between the naturals into comparisons between the terms.
-
The degenerate cases are discharged first. If or then and are both empty, and step 1.1 proves directly that the empty list has neither required positive-length sublist.
Depends on
- A finite list of reals, and its strictly increasing and strictly decreasing sublists
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- Laws of finite sums and products in $\mathbb{N}$, and $\iota\big(\sum_{k<n} a_k\big) = \sum_{k<n} \iota(a_k)$
- Multiplication of natural numbers
- Addition of natural numbers
- Order on the natural numbers
- On $\mathbb{N}$ the order is membership: $m < n \iff m \in n$
- Order is compatible with addition
- Addition is cancellative
- Distributivity and the successor law for multiplication
- Multiplication is commutative
- Addition is commutative
- Trichotomy of the order on $\mathbb{N}$
- $\le$ is a linear order on $\mathbb{N}$
- Discreteness: $\sigma(n)$ is the immediate successor
- Ordered field
- Injection, surjection, bijection
- The cardinality $\lvert A\rvert$ of a finite set
- A subset of a finite set is finite, with $\lvert B\rvert \le \lvert A\rvert$, and equality holds if and only if $B = A$
- 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$
- The pigeonhole principle on $\mathbb{N}$
- Finite sums and finite products of natural numbers, $\sum_{k<n} a_k$ and $\prod_{k<n} a_k$ in $\mathbb{N}$
- Field
Used by
- A list of six distinct reals with no strictly increasing sublist of length four and no strictly decreasing sublist of length three Counterexample
- FALSE: every list of mn pairwise distinct reals has a strictly increasing sublist of length m+1 or a strictly decreasing sublist of length n+1 False statement
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 66 results over 22 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)
- Longest increasing subsequence (Wikipedia) (standard reference, not scraped)