Alphabeta Math
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.

For all mm and nn there is a list of mnmn pairwise distinct reals with no strictly increasing sublist of length m+1m+1 and no strictly decreasing sublist of length n+1n+1

Statement

Let m,nNm, n \in \mathbb{N}. Then there is a pairwise distinct finite list of reals a:(mn)Ra : (mn) \to \mathbb{R} (A finite list of reals, and its strictly increasing and strictly decreasing sublists) with no strictly increasing sublist of length m+1m+1 and no strictly decreasing sublist of length n+1n+1.

Together with the bound mn+1mn+1, this says that mn+1mn+1 is the least length at which the two alternatives become unavoidable.

At m=0m = 0 or n=0n = 0 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 11.

Facts & Assumptions

Given: Naturals mm and nn, the finite sets m×nm \times n and mnmn, and the ordered field R\mathbb{R} with the canonical natural ι:NR\iota : \mathbb{N} \to \mathbb{R} (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field).

[L1]

Arithmetic and order of N\mathbb{N}: addition and multiplication are as in Addition of natural numbers and Multiplication of natural numbers; pqp \le q means p+j=qp + j = q for a unique jj, written qpq - p (Order on the natural numbers, Addition is cancellative, Finite sums and finite products of natural numbers, k<nak\sum_{k<n} a_k and k<nak\prod_{k<n} a_k in N\mathbb{N}), and \le is transitive (\le is a linear order on N\mathbb{N}); p<qp<q if and only if p+1qp+1\le q (Discreteness: σ(n)\sigma(n) is the immediate successor); p+k<q+k    p<qp + k < q + k \iff p < q (Order is compatible with addition); addition is commutative (Addition is commutative); σ(b)n=bn+n\sigma(b)\cdot n = b\cdot n + n (Distributivity and the successor law for multiplication); multiplication is monotone in its first factor, since p+d=qp + d = q gives qn=nq=np+nd=pn+dnq\,n = n\,q = n\,p + n\,d = p\,n + d\,n by commutativity and distributivity (Multiplication is commutative, Distributivity and the successor law for multiplication), so pqp \le q implies pnqnp\,n \le q\,n; exactly one of p<qp<q, p=qp=q, q<pq<p holds (Trichotomy of the order on N\mathbb{N}); and k<N    kNk < N \iff k \in N (On N\mathbb{N} the order is membership: m<n    mnm < n \iff m \in n).

[L3]

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 BA\lvert B\rvert \le \lvert A\rvert, and equality holds if and only if B=AB = A then makes the image the whole codomain (The cardinality A\lvert A\rvert of a finite set, Injection, surjection, bijection).

[L4]

There is no injection of LL into KK when K<LK < L (The pigeonhole principle on N\mathbb{N}, clause 2).

[L6]

Sublists (A finite list of reals, and its strictly increasing and strictly decreasing sublists): a sublist of length LL is a strictly increasing s:Lmns : L \to mn, hence injective; it is strictly increasing, respectively decreasing, when its values do the same.

Proof

technique · constructive
1.1

If m=0m=0 or n=0n=0, then mn=0mn=0 and the empty list has no sublist of the positive lengths m+1m+1 and n+1n+1, proving the assertion in these boundary cases. Hence for the construction below assume m,n1m,n\ge1.

givenL1L2
1.2

The index bijection. Define β:m×nN\beta : m \times n \to \mathbb{N} by β(b,j):=bn+j\beta(b,j) := b\,n + j. Its values lie in mnmn: from j<nj < n and b<mb < m we get j+1nj + 1 \le n and b+1mb + 1 \le m, so β(b,j)+1=bn+(j+1)bn+n=σ(b)nmn\beta(b,j) + 1 = bn + (j+1) \le bn + n = \sigma(b)\cdot n \le mn by [L1], whence β(b,j)<mn\beta(b,j) < mn.

L1construct
1.3

β\beta is injective. Suppose β(b,j)=β(b,j)\beta(b,j) = \beta(b',j') with (b,j),(b,j)m×n(b,j), (b',j') \in m \times n. If b<bb < b' then σ(b)b\sigma(b) \le b', so β(b,j)<bn+n=σ(b)nbnβ(b,j)\beta(b,j) < bn + n = \sigma(b)\,n \le b'n \le \beta(b',j') by [L1], a contradiction; symmetrically b<bb' < b is impossible, so b=bb = b' by [L1], and then j=jj = j' by cancellation.

L1construct
2.1

The list. By [L2] and [L3], the injection β\beta of step 1.3 is a bijection of m×nm \times n onto mnmn, so every index i<mni < mn is β(b,j)\beta(b,j) for exactly one pair, and aβ(b,j)  :=  ι(bn+nj)(b<m, j<n)a_{\beta(b,j)} \;:=\; \iota\big(b\,n + n - j\big) \qquad (b<m,\ j<n) defines a list a:(mn)Ra : (mn) \to \mathbb{R}. Write blk(β(b,j)):=b\mathrm{blk}(\beta(b,j)) := b for the block of an index.

step 1.2step 1.3L2L3construct
3.1

Inside a block the values decrease. Let b<mb < m and j<j<nj < j' < n. Then β(b,j)<β(b,j)\beta(b,j) < \beta(b,j') by [L1], while nj1n - j' \ge 1 and nj=(nj)+(jj)n - j = (n-j') + (j'-j) with jj1j'-j \ge 1, so nj<njn-j' < n-j and hence aβ(b,j)<aβ(b,j)a_{\beta(b,j')} < a_{\beta(b,j)} by [L1] and [L5].

step 2.1L1L5
3.2

Across blocks the values increase, and the block is monotone in the index. Let b<b<mb < b' < m and j,j<nj, j' < n. Then bn+njbn+n=σ(b)nbn<bn+(nj)bn + n - j \le bn + n = \sigma(b)\,n \le b'n < b'n + (n - j'), the last step because nj1n - j' \ge 1; so aβ(b,j)<aβ(b,j)a_{\beta(b,j)} < a_{\beta(b',j')} by [L5]. Moreover β(b,j)<β(b,j)\beta(b,j) < \beta(b',j'), by the computation of step 1.3; equivalently, blk\mathrm{blk} is nondecreasing along the index order.

step 1.3step 2.1L1L5
4.1

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.

step 2.1step 3.1step 3.2
4.2

No strictly increasing sublist of length m+1m+1. Let s:Lmns : L \to mn be a strictly increasing sublist. The map blks:Lm\mathrm{blk}\circ s : L \to m is injective: if p<q<Lp < q < L had blk(s(p))=blk(s(q))\mathrm{blk}(s(p)) = \mathrm{blk}(s(q)), then s(p)<s(q)s(p) < s(q) lie in one block, so as(p)>as(q)a_{s(p)} > a_{s(q)} by step 3.1, contradicting that the sublist increases. Hence LmL \le m by [L4] and natural-order trichotomy, so Lm+1L \ne m+1.

step 2.1step 3.1L1L4L6
4.3

No strictly decreasing sublist of length n+1n+1. Let s:Lmns : L \to mn be a strictly decreasing sublist and let p<q<Lp < q < L. Then s(p)<s(q)s(p) < s(q), so blk(s(p))blk(s(q))\mathrm{blk}(s(p)) \le \mathrm{blk}(s(q)) by step 3.2; and blk(s(p))<blk(s(q))\mathrm{blk}(s(p)) < \mathrm{blk}(s(q)) would give as(p)<as(q)a_{s(p)} < a_{s(q)} by step 3.2, contradicting that the sublist decreases. Thus, if L>0L>0, all the s(p)s(p) lie in the block of s(0)s(0), say s(p)=β(b,jp)s(p)=\beta(b,j_p), and pjpp\mapsto j_p is injective into nn because ss is injective and β\beta is a bijection. If L=0L=0, the empty map is already an injection LnL\to n. In either case [L4] and natural-order trichotomy give LnL\le n, so Ln+1L\ne n+1.

step 1.1step 2.1step 3.2L1L4L6
5.1

Together with the boundary cases in step 1.1, the list of step 2.1 is therefore a pairwise distinct list of mnmn reals with no strictly increasing sublist of length m+1m+1 and no strictly decreasing sublist of length n+1n+1, which is the assertion.

step 1.1step 4.1step 4.2step 4.3discharge-construct

Remarks

  • The two block counts are not interchangeable. The construction uses mm blocks of nn terms each. An increasing sublist meets each block at most once, so its length is bounded by the number of blocks, mm; a decreasing sublist lies inside one block, so its length is bounded by the block size, nn. Exchanging the roles would bound the increasing sublists by nn and the decreasing ones by mm, which is the sharpness statement for the pair (n,m)(n,m) and not for (m,n)(m,n).

  • Why the values are written through ι\iota. The terms of a list of reals are real numbers, and bn+njbn+n-j is a natural number, which is a set and not an element of R\mathbb{R}. The strict monotonicity of ι\iota is what transports the comparisons between the naturals into comparisons between the terms.

  • The degenerate cases are discharged first. If m=0m = 0 or n=0n = 0 then m×nm \times n and mnmn are both empty, and step 1.1 proves directly that the empty list has neither required positive-length sublist.

Depends on

Used by

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