LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Basic subsequences of the first row

Statement

Let $w = (w_{1}, \dots, w_{N})$ be a word of pairwise distinct real numbers and let $P (w)$ be its insertion tableau, built by Row insertion and the bumping route. For $j \geq 1$ let $S_{j}$ be the list, in the order of insertion, of those letters which at the moment of their insertion are placed in position $j$ of the first row (equivalently, the letters that pass through the $j$ -th position of the first row). Then:

each $S_{j}$ is a strictly decreasing subsequence of $w$ ;
for every $x \in S_{j}$ with $j \geq 2$ , the entry $y$ occupying position $j - 1$ of the first row at the moment $x$ is inserted belongs to $S_{j - 1}$ , was inserted earlier than $x$ , and satisfies $y < x$ .

The lists $S_{1}, S_{2}, \dots$ are the basic subsequences of $w$ .

Facts & Assumptions

Given: A word $w = (w_{1}, \dots, w_{N})$ of pairwise distinct real numbers, its insertion tableaux $P_{k} = P (w_{1}, \dots, w_{k})$ , and for each $j \geq 1$ the list $S_{j}$ of letters placed at position $j$ of the first row at their own insertion.

[L1]

At each step the insertion of $w_{k}$ processes the first row once: either it appends $w_{k}$ at the end of the first row, at position $λ_{1} + 1$ , or it replaces the leftmost first-row entry exceeding $w_{k}$ , at some position $j \leq λ_{1}$ , and passes that displaced entry to the second row. Both alternatives place exactly one letter in the first row, and positions of the first row are filled from the left: a position $j$ can receive a letter only at a step, and thereafter its occupant is whatever was placed there last (Row insertion and the bumping route).

[L2]

$P_{k}$ is a standard tableau and its first row is strictly increasing, so its entry in position $j - 1$ is smaller than its entry in position $j$ whenever both positions exist (Monotonicity of the bumping route and standardness of the output, Tableaux and standard tableaux).

Proof

technique · direct

1.1L1

A letter is placed at position $j$ of the first row only when position $j$ already exists and is replaced, or when it is appended as the new last position $j = λ_{1} + 1$ ; in the replacement case the placed letter is strictly smaller than the entry it replaces, by the leftmost-greater rule, and in the append case position $j$ had no previous occupant.

1.2L1given

The lists $S_{j}$ consist of distinct steps of the word in increasing order, because at each step at most one letter is placed in the first row; therefore each $S_{j}$ is a subsequence of $w$ .

1.3L1L2given

Let $x \in S_{j}$ with $j \geq 2$ , inserted at step $k$ , and let $y$ be the entry occupying position $j - 1$ of the first row immediately before the insertion of $w_{k}$ . Position $j - 1$ exists because $j \leq λ_{1} + 1$ at that moment, and $y < x$ : in a replacement this follows from the leftmost entry exceeding $x$ being at position $j$ , so every earlier entry is smaller than $x$ ; in an append it follows from $x$ exceeding every old row entry.

2.1step 1.1L1

Since the occupant of position $j$ is always the last letter placed there (step 1.1), each successive element of $S_{j}$ is strictly smaller than its predecessor: the predecessor is the occupant replaced at the successor's insertion step. Hence $S_{j}$ , read in the order of insertion, is strictly decreasing.

3.1step 2.1step 1.2step 1.3L1

The entry $y$ was placed at position $j - 1$ at some earlier step $k^{'} < k$ : by step 1.1 every occupant of a position of the first row is placed there at a step, and $y$ is the current occupant before step $k$ , so its placement step precedes $k$ . Hence $y \in S_{j - 1}$ and $y$ is inserted earlier than $x$ , which together with $y < x$ proves (2).

4.1step 2.1step 1.2step 3.1∎

Consequently every element of $S_{j}$ with $j \geq 2$ has an earlier smaller predecessor in $S_{j - 1}$ , while each $S_{j}$ is strictly decreasing; this is the assertion of the lemma.

Depends on

Used by

The Schensted theorem on longest increasing and decreasing subsequences Theorem

Dependency tree · two levels

5 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

C. Schensted, Longest Increasing and Decreasing Subsequences, Canadian Journal of Mathematics 13 (1961), 179-191 (13 pp.) (standard reference, not scraped)
Donald E. Knuth, Permutations, Matrices, and Generalized Young Tableaux, Pacific Journal of Mathematics 34 (1970), 709-727 (standard reference, not scraped)