Row insertion and the bumping route

Let $T$ be a standard tableau whose entries are distinct real numbers (Tableaux and standard tableaux) and let $x\in \mathbb{R}$ be a number that is not an entry of $T$. The row insertion $T\leftarrow x$ is the following procedure. Put $x_1:=x$ and consider row $1$. At row $i$: if row $i$ is empty or $x_i$ is larger than every entry of row $i$, append $x_i$ in a new box at the right end of row $i$ and stop; otherwise let $r_i$ be the position of the leftmost entry $y_i$ of row $i$ with $y_i>x_i$, replace that entry by $x_i$, put $x_{i+1}:=y_i$, and continue with row $i+1$.

For distinct real alphabets, the phrase "standard tableau" in this insertion packet means an injective filling whose rows and columns strictly increase. Its unique increasing rank relabelling is a standard tableau with entries $1,\dots ,m$ in the published convention. Each comparison in this procedure is preserved and reflected by increasing relabelling, so all positions and carried labels correspond under that relabelling, by induction over the finite procedure.

The procedure terminates, and the bound is proved rather than assumed. If $r_i$ is defined for a nonempty row $i$, then either row $i+1$ has length $<r_i$, in which case the next step either bumps an entry in that shorter row, at a position $r_{i+1}\le {\lambda }_{i+1}$, or appends at $r_{i+1}={\lambda }_{i+1}+1$; in either case $r_{i+1}\le r_i$, or row $i+1$ has length $\ge r_i$; in the latter case its entry in position $r_i$ lies strictly below $y_i$ and is therefore larger than $y_i$, so again the next replacement position, when it exists, satisfies $r_{i+1}\le r_i$. Hence the route positions weakly decrease, and after at most $k+1$ row visits, where $k$ is the number of nonempty rows of $T$, the letter is appended (at the latest in the empty row $k+1$).

The output is a filling of $[\mathrm{shape}(T)]\cup \{b\}$, where the new box is $b=(s,r_s)$ with $r_s={\lambda }_s+1$ in the row $s$ in which the route stopped, or $b=(k+1,1)$ if a new row was opened. The sequence $(r_1,\dots ,r_s)$ is the bumping route and $x=x_1<x_2<\cdots <x_s$ are the bumped letters; the strict increase of the bumped letters is proved in Monotonicity of the bumping route and standardness of the output. The procedure is deterministic, so $T\leftarrow x$ is well defined; standardness of the output is not part of the definition but is proved in the same lemma.