Row bumping and its inverse

Row insertion replaces the first entry strictly greater than the inserted letter and bumps that entry to the next row. If there is no such entry, it appends the letter and stops. The strict comparison is essential: repeated letters remain in the row, as required for semistandard tableaux with weakly increasing rows and strictly increasing columns.

TauCeti.rowBump performs this local step on a list over any linearly ordered alphabet. Its split characterization specifies both the changed row and the bumped letter. It preserves weak row order and the combined content of the row and the travelling letter.

Reverse insertion replaces the rightmost entry strictly smaller than the incoming letter. This is the same operation on the reversed row over the order-dual alphabet. TauCeti.reverseRowBump exposes this step in the original row orientation. The recovery theorems prove both inverse directions for bumps in weakly increasing rows, including when a row has repeated entries. These local inverse steps are iterated along the bumping route in the Robinson--Schensted--Knuth correspondence.

References

• W. Fulton, Young Tableaux, Cambridge University Press (1997), for row insertion and reverse row insertion.

def TauCeti.rowBump {α : Type u_1} [LinearOrder α] (x : α) : List α → List α × Option α

Insert a letter into a row, bumping its first strictly larger entry. If no entry is larger, append the letter. The second component is the letter to insert into the next row, if any.

Equations

• TauCeti.rowBump x [] = ([x], none)
• TauCeti.rowBump x (y :: row) = if x < y then (x :: row, some y) else have result := TauCeti.rowBump x row; (y :: result.1, result.2)

@[simp]

theorem TauCeti.rowBump_nil {α : Type u_1} [LinearOrder α] (x : α) : rowBump x [] = ([x], none)

theorem TauCeti.rowBump_cons {α : Type u_1} [LinearOrder α] (x y : α) (row : List α) : rowBump x (y :: row) = if x < y then (x :: row, some y) else (y :: (rowBump x row).1, (rowBump x row).2)

Row bumping stops at the first strictly larger entry.

@[simp]

theorem TauCeti.rowBump_cons_of_le {α : Type u_1} [LinearOrder α] {x y : α} (row : List α) (h : y ≤ x) : rowBump x (y :: row) = (y :: (rowBump x row).1, (rowBump x row).2)

An entry at most the inserted letter is passed without changing it.

@[simp]

theorem TauCeti.rowBump_cons_of_lt {α : Type u_1} [LinearOrder α] {x y : α} (row : List α) (h : x < y) : rowBump x (y :: row) = (x :: row, some y)

A strictly larger entry is replaced and bumped.

theorem TauCeti.rowBump_append {α : Type u_1} [LinearOrder α] (x : α) (before row : List α) (h : ∀ (z : α), z ∈ before → z ≤ x) : rowBump x (before ++ row) = (before ++ (rowBump x row).1, (rowBump x row).2)

A prefix whose letters are at most the inserted letter is unchanged.

@[simp]

theorem TauCeti.rowBump_snd_eq_none_iff {α : Type u_1} [LinearOrder α] (x : α) (row : List α) : (rowBump x row).2 = none ↔ ∀ (z : α), z ∈ row → z ≤ x

Appending occurs precisely when all existing letters are at most the inserted letter.

theorem TauCeti.rowBump_of_forall_le {α : Type u_1} [LinearOrder α] (x : α) (row : List α) (h : ∀ (z : α), z ∈ row → z ≤ x) : rowBump x row = (row ++ [x], none)

If nothing is bumped, the output row is the original row with the inserted letter appended.

theorem TauCeti.rowBump_eq_some_iff {α : Type u_1} [LinearOrder α] (x y : α) (row result : List α) : rowBump x row = (result, some y) ↔ ∃ (before : List α), ∃ (after : List α), row = before ++ y :: after ∧ result = before ++ x :: after ∧ (∀ (z : α), z ∈ before → z ≤ x) ∧ x < y

The full characterization of a bump: a prefix at most x is followed by the first entry y > x, and only that entry is replaced. No ordering hypothesis on the row is needed.

theorem TauCeti.mem_of_rowBump_snd_eq_some {α : Type u_1} [LinearOrder α] {x y : α} {row : List α} (h : (rowBump x row).2 = some y) : y ∈ row

The bumped letter was an entry of the original row.

theorem TauCeti.lt_of_rowBump_snd_eq_some {α : Type u_1} [LinearOrder α] {x y : α} {row : List α} (h : (rowBump x row).2 = some y) : x < y

A bumped letter is strictly greater than the inserted letter.

theorem TauCeti.exists_set_of_rowBump_snd_eq_some {α : Type u_1} [LinearOrder α] {x y : α} {row : List α} (h : (rowBump x row).2 = some y) : ∃ (j : ℕ), ∃ (hj : j < row.length), (rowBump x row).1 = row.set j x ∧ row[j] = y ∧ (∀ (i : ℕ) (hi : i < j), row[i] ≤ x) ∧ x < y

Index form of a bump: it replaces the entry at some position j by x, where every earlier entry is at most x and the replaced entry is strictly greater.

theorem TauCeti.rowBump_perm {α : Type u_1} [LinearOrder α] (x : α) (row : List α) : ((rowBump x row).1 ++ (rowBump x row).2.toList).Perm (x :: row)

Row insertion conserves the letters: the changed row together with the bumped letter has the content of the original row together with the inserted letter.

theorem TauCeti.length_rowBump {α : Type u_1} [LinearOrder α] (x : α) (row : List α) : (rowBump x row).1.length + (rowBump x row).2.toList.length = row.length + 1

A bump preserves row length; appending increases it by one.

theorem TauCeti.sortedLE_rowBump {α : Type u_1} [LinearOrder α] (x : α) {row : List α} (hrow : row.SortedLE) : (rowBump x row).1.SortedLE

Inserting into a weakly increasing row preserves weak increase.

theorem TauCeti.nodup_rowBump {α : Type u_1} [LinearOrder α] (x : α) {row : List α} (hrow : row.Nodup) (hx : ¬x ∈ row) : (rowBump x row).1.Nodup

Inserting a new letter into a row without repetitions introduces no repetition.

theorem TauCeti.sortedLT_rowBump {α : Type u_1} [LinearOrder α] (x : α) {row : List α} (hrow : row.SortedLT) (hx : ¬x ∈ row) : (rowBump x row).1.SortedLT

Inserting a new letter into a strictly increasing row preserves strict increase.

theorem TauCeti.rowBump_bumped_le_of_le {α : Type u_1} [LinearOrder α] {x x' y y' : α} {row : List α} (hrow : row.SortedLE) (hxx' : x ≤ x') (hfirst : (rowBump x row).2 = some y) (hsecond : (rowBump x' (rowBump x row).1).2 = some y') : y ≤ y'

The letters bumped by two successively inserted weakly increasing letters are weakly increasing. This is the one-row comparison used to propagate the order of bumping routes.

def TauCeti.reverseRowBump {α : Type u_1} [LinearOrder α] (y : α) (row : List α) : List α × Option α

Reverse insert a letter by replacing and returning the rightmost strictly smaller entry. If no entry is smaller, prepend the letter and return none. The row is returned in its original orientation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.reverseRowBump_nil {α : Type u_1} [LinearOrder α] (y : α) : reverseRowBump y [] = ([y], none)

theorem TauCeti.reverseRowBump_append {α : Type u_1} [LinearOrder α] (y : α) (row after : List α) (h : ∀ (z : α), z ∈ after → y ≤ z) : reverseRowBump y (row ++ after) = ((reverseRowBump y row).1 ++ after, (reverseRowBump y row).2)

A suffix whose letters are at least the incoming letter is unchanged.

@[simp]

theorem TauCeti.reverseRowBump_append_singleton_of_le {α : Type u_1} [LinearOrder α] {x y : α} (row : List α) (h : y ≤ x) : reverseRowBump y (row ++ [x]) = ((reverseRowBump y row).1 ++ [x], (reverseRowBump y row).2)

A final entry at least the incoming letter is passed without changing it.

@[simp]

theorem TauCeti.reverseRowBump_append_singleton_of_lt {α : Type u_1} [LinearOrder α] {x y : α} (row : List α) (h : x < y) : reverseRowBump y (row ++ [x]) = (row ++ [y], some x)

A strictly smaller final entry is replaced and returned.

@[simp]

theorem TauCeti.reverseRowBump_snd_eq_none_iff {α : Type u_1} [LinearOrder α] (y : α) (row : List α) : (reverseRowBump y row).2 = none ↔ ∀ (z : α), z ∈ row → y ≤ z

Reverse insertion prepends precisely when no entry is strictly smaller.

theorem TauCeti.reverseRowBump_of_forall_le {α : Type u_1} [LinearOrder α] (y : α) (row : List α) (h : ∀ (z : α), z ∈ row → y ≤ z) : reverseRowBump y row = (y :: row, none)

With no smaller entry to replace, reverse insertion prepends the incoming letter.

theorem TauCeti.reverseRowBump_eq_some_iff {α : Type u_1} [LinearOrder α] (x y : α) (row result : List α) : reverseRowBump y row = (result, some x) ↔ ∃ (before : List α), ∃ (after : List α), row = before ++ x :: after ∧ result = before ++ y :: after ∧ (∀ (z : α), z ∈ after → y ≤ z) ∧ x < y

Reverse insertion replaces the rightmost entry x < y, passing a suffix of entries at least y. No ordering hypothesis on the row is needed.

theorem TauCeti.mem_of_reverseRowBump_snd_eq_some {α : Type u_1} [LinearOrder α] {x y : α} {row : List α} (h : (reverseRowBump y row).2 = some x) : x ∈ row

The letter returned by reverse insertion was an entry of the original row.

theorem TauCeti.lt_of_reverseRowBump_snd_eq_some {α : Type u_1} [LinearOrder α] {x y : α} {row : List α} (h : (reverseRowBump y row).2 = some x) : x < y

A letter returned by reverse insertion is strictly smaller than the incoming letter.

theorem TauCeti.exists_set_of_reverseRowBump_snd_eq_some {α : Type u_1} [LinearOrder α] {x y : α} {row : List α} (h : (reverseRowBump y row).2 = some x) : ∃ (d : ℕ), ∃ (hd : d < row.length), (reverseRowBump y row).1 = row.set d y ∧ row[d] = x ∧ (∀ (i : ℕ) (hi : i < row.length), d < i → y ≤ row[i]) ∧ x < y

Index form of a reverse bump: it replaces the entry at some position d by y, where every later entry is at least y and the replaced entry is strictly smaller.

theorem TauCeti.reverseRowBump_perm {α : Type u_1} [LinearOrder α] (y : α) (row : List α) : ((reverseRowBump y row).1 ++ (reverseRowBump y row).2.toList).Perm (y :: row)

Reverse insertion conserves the letters: the changed row together with the returned letter has the content of the original row together with the incoming letter.

theorem TauCeti.length_reverseRowBump {α : Type u_1} [LinearOrder α] (y : α) (row : List α) : (reverseRowBump y row).1.length + (reverseRowBump y row).2.toList.length = row.length + 1

A reverse bump preserves row length; prepending increases it by one.

theorem TauCeti.sortedLE_reverseRowBump {α : Type u_1} [LinearOrder α] (y : α) {row : List α} (hrow : row.SortedLE) : (reverseRowBump y row).1.SortedLE

Reverse inserting into a weakly increasing row preserves weak increase.

theorem TauCeti.nodup_reverseRowBump {α : Type u_1} [LinearOrder α] (y : α) {row : List α} (hrow : row.Nodup) (hy : ¬y ∈ row) : (reverseRowBump y row).1.Nodup

Reverse inserting a new letter into a row without repetitions introduces no repetition.

theorem TauCeti.sortedLT_reverseRowBump {α : Type u_1} [LinearOrder α] (y : α) {row : List α} (hrow : row.SortedLT) (hy : ¬y ∈ row) : (reverseRowBump y row).1.SortedLT

Reverse inserting a new letter into a strictly increasing row preserves strict increase.

theorem TauCeti.reverseRowBump_rowBump_of_sortedLE {α : Type u_1} [LinearOrder α] (x y : α) {row : List α} (hrow : row.SortedLE) (hbump : (rowBump x row).2 = some y) : reverseRowBump y (rowBump x row).1 = (row, some x)

Reverse insertion recovers a forward bump in a weakly increasing row.

theorem TauCeti.rowBump_reverseRowBump_of_sortedLE {α : Type u_1} [LinearOrder α] (x y : α) {row : List α} (hrow : row.SortedLE) (hbump : (reverseRowBump y row).2 = some x) : rowBump x (reverseRowBump y row).1 = (row, some y)

Forward insertion recovers a reverse bump in a weakly increasing row.