Elementary grid stabilization moves

A grid stabilization inserts one row and one column near a marking. In the resulting local 2 × 2 block, the chosen marking is split across two opposite corners and one marking of the other type occupies a third corner. Deleting the new row and column recovers the original diagram.

This file first gives the two permutation operations underlying this construction. GridState.insertPoint inserts one point at the intersection of the new row and column, while GridState.splitPoint replaces a chosen old point by the other two corners of that local block. It then constructs stabilizations that split either an O- or an X-marking.

The predicates GridDiagram.IsOStabilization and GridDiagram.IsXStabilization require the new row and column to be cyclically adjacent to the row and column of the split marking. Allowing either cyclic orientation in each coordinate gives the four corner types for each marking, hence the eight standard stabilization types. GridDiagram.IsStabilization combines the two marking types, and GridDiagram.IsDestabilization reverses the relation.

Main definitions

• TauCeti.GridState.insertPoint: insert a point into a permutation graph.
• TauCeti.GridState.splitPoint: split one old point across the other corners of an inserted row and column.
• TauCeti.GridDiagram.stabilizeO, TauCeti.GridDiagram.stabilizeX: the two marking-level stabilization constructions.
• TauCeti.GridDiagram.IsStabilization, TauCeti.GridDiagram.IsDestabilization: elementary stabilization and destabilization relations.

Main results

• TauCeti.GridDiagram.stabilizeO_castSucc_eq_stabilizeX_succ and TauCeti.GridDiagram.stabilizeO_succ_eq_stabilizeX_castSucc: with the new column next to the split column, an O-stabilization is the X-stabilization of the same column with the new column on the other side.
• TauCeti.GridDiagram.stabilizeX_castSucc_swapColumns and TauCeti.GridDiagram.stabilizeX_swapRows: swapping the new column or row of an X-stabilization with an adjacent old one moves it to the other side.
• TauCeti.GridDiagram.rotate_stabilizeX_succ: reversing both coordinates exchanges the two corner types of X-stabilization, whose new O-marking is the north-east or the south-west corner of the new block.
• TauCeti.GridDiagram.stabilizeX_last_relabelRows, TauCeti.GridDiagram.stabilizeX_last_relabelColumns and TauCeti.GridDiagram.stabilizeO_last_relabelColumns: a cyclic permutation moves a new last row or column to the front.

References

This supplies the stabilization half of the standing convention in TauCetiRoadmap/CombinatorialHeegaardFloer/README.md that a link is initially a grid diagram modulo grid moves. The local three-marking construction and its eight types follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3.

def TauCeti.GridState.insertPoint {n : ℕ} (x : GridState n) (newColumn newRow : Fin (n + 1)) : GridState (n + 1)

Insert a new point (newColumn, newRow) into a grid state.

Every old point (c, x c) is sent to (newColumn.succAbove c, newRow.succAbove (x c)).

@[simp]

theorem TauCeti.GridState.insertPoint_apply_newColumn {n : ℕ} (x : GridState n) (newColumn newRow : Fin (n + 1)) : (x.insertPoint newColumn newRow).toPerm newColumn = newRow

The inserted column contains the inserted row.

@[simp]

theorem TauCeti.GridState.insertPoint_apply_succAbove {n : ℕ} (x : GridState n) (newColumn newRow : Fin (n + 1)) (c : Fin n) : (x.insertPoint newColumn newRow).toPerm (newColumn.succAbove c) = newRow.succAbove (x.toPerm c)

An old column contains the embedded image of its old row after inserting a point.

theorem TauCeti.GridState.insertPoint_injective {n : ℕ} (newColumn newRow : Fin (n + 1)) : Function.Injective fun (x : GridState n) => x.insertPoint newColumn newRow

Inserting the same point into two grid states gives equal states only if the states were equal.

theorem TauCeti.GridState.exists_insertPoint_eq {n : ℕ} {newColumn newRow : Fin (n + 1)} {y : GridState (n + 1)} (h : y.toPerm newColumn = newRow) : ∃ (x : GridState n), x.insertPoint newColumn newRow = y

Every grid state containing the point (newColumn, newRow) is obtained by inserting that point into a grid state of the smaller grid.

def TauCeti.GridState.splitPoint {n : ℕ} (x : GridState n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) : GridState (n + 1)

Split the point in column splitColumn across an inserted row and column.

The old point at (splitColumn, x splitColumn) is replaced by the two points (newColumn, newRow.succAbove (x splitColumn)) and (newColumn.succAbove splitColumn, newRow). All other old points are embedded as in GridState.insertPoint.

@[simp]

theorem TauCeti.GridState.splitPoint_apply_newColumn {n : ℕ} (x : GridState n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) : (x.splitPoint newColumn newRow splitColumn).toPerm newColumn = newRow.succAbove (x.toPerm splitColumn)

The new column of a split point contains the embedded old row of the split point.

@[simp]

theorem TauCeti.GridState.splitPoint_apply_splitColumn {n : ℕ} (x : GridState n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) : (x.splitPoint newColumn newRow splitColumn).toPerm (newColumn.succAbove splitColumn) = newRow

The embedded old column of a split point contains the new row.

@[simp]

theorem TauCeti.GridState.splitPoint_castSucc_apply_succ {n : ℕ} (x : GridState n) (newRow : Fin (n + 1)) (splitColumn : Fin n) : (x.splitPoint splitColumn.castSucc newRow splitColumn).toPerm splitColumn.succ = newRow

When the new column is inserted immediately before the split column, the split column moves to its successor and contains the new row.

@[simp]

theorem TauCeti.GridState.splitPoint_apply_succAbove {n : ℕ} (x : GridState n) (newColumn newRow : Fin (n + 1)) (splitColumn c : Fin n) : (x.splitPoint newColumn newRow splitColumn).toPerm (newColumn.succAbove c) = if c = splitColumn then newRow else newRow.succAbove (x.toPerm c)

Away from the split column, splitPoint embeds old points in the inserted grid.

@[simp]

theorem TauCeti.GridState.insertPoint_apply_eq_iff {n : ℕ} (x : GridState n) (newColumn newRow c : Fin (n + 1)) : (x.insertPoint newColumn newRow).toPerm c = newRow ↔ c = newColumn

After inserting a point, the new row is occupied only in the new column.

@[simp]

theorem TauCeti.GridState.splitPoint_apply_eq_iff {n : ℕ} (x : GridState n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) (c : Fin (n + 1)) : (x.splitPoint newColumn newRow splitColumn).toPerm c = newRow ↔ c = newColumn.succAbove splitColumn

After splitting a point, the new row is occupied only in the embedded split column.

theorem TauCeti.GridState.splitPoint_castSucc_eq_insertPoint {n : ℕ} (x : GridState n) (s : Fin n) (newRow : Fin (n + 1)) : x.splitPoint s.castSucc newRow s = x.insertPoint s.succ newRow

Splitting the point of column s across a column inserted just before it is inserting the point (s.succ, newRow): the old point of column s moves to the new column s.castSucc, and every other column is embedded alike by s.castSucc.succAbove and s.succ.succAbove.

theorem TauCeti.GridState.splitPoint_succ_eq_insertPoint {n : ℕ} (x : GridState n) (s : Fin n) (newRow : Fin (n + 1)) : x.splitPoint s.succ newRow s = x.insertPoint s.castSucc newRow

Splitting the point of column s across a column inserted just after it is inserting the point (s.castSucc, newRow): the old point of column s moves to the new column s.succ.

theorem TauCeti.GridState.insertPoint_castSucc_swapColumns {n : ℕ} (x : GridState n) (s : Fin n) (newRow : Fin (n + 1)) : swapColumns s.castSucc s.succ (x.insertPoint s.castSucc newRow) = x.insertPoint s.succ newRow

Swapping an inserted column s.castSucc with the old column s just after it moves the inserted column to s.succ.

theorem TauCeti.GridState.insertPoint_succ_swapColumns {n : ℕ} (x : GridState n) (s : Fin n) (newRow : Fin (n + 1)) : swapColumns s.castSucc s.succ (x.insertPoint s.succ newRow) = x.insertPoint s.castSucc newRow

Swapping an inserted column s.succ with the old column s just before it moves the inserted column to s.castSucc.

theorem TauCeti.GridState.transpose_insertPoint {n : ℕ} (x : GridState n) (newColumn newRow : Fin (n + 1)) : (x.insertPoint newColumn newRow).transpose = x.transpose.insertPoint newRow newColumn

Reflecting in the diagonal exchanges the roles of the inserted row and column.

theorem TauCeti.GridState.transpose_splitPoint {n : ℕ} (x : GridState n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) : (x.splitPoint newColumn newRow splitColumn).transpose = x.transpose.splitPoint newRow newColumn (x.toPerm splitColumn)

Diagonal reflection splits the transposed point across the exchanged row and column.

theorem TauCeti.GridState.rotate_insertPoint {n : ℕ} (x : GridState n) (newColumn newRow : Fin (n + 1)) : (x.insertPoint newColumn newRow).rotate = x.rotate.insertPoint newColumn.rev newRow.rev

Reversing both coordinates of a grid state with an inserted point reverses the coordinates of the inserted point.

theorem TauCeti.GridState.rotate_splitPoint {n : ℕ} (x : GridState n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) : (x.splitPoint newColumn newRow splitColumn).rotate = x.rotate.splitPoint newColumn.rev newRow.rev splitColumn.rev

Reversing both coordinates of a grid state with a split point reverses the inserted row and column and the split column.

theorem TauCeti.GridState.insertPoint_swapRows {n : ℕ} (x : GridState n) (newColumn : Fin (n + 1)) (k : Fin n) : swapRows k.castSucc k.succ (x.insertPoint newColumn k.castSucc) = x.insertPoint newColumn k.succ

Swapping an inserted row k.castSucc with the old row k just above it moves the inserted row to k.succ.

theorem TauCeti.GridState.splitPoint_swapRows {n : ℕ} (x : GridState n) (newColumn : Fin (n + 1)) (k s : Fin n) : swapRows k.castSucc k.succ (x.splitPoint newColumn k.castSucc s) = x.splitPoint newColumn k.succ s

Swapping an inserted row k.castSucc with the old row k just above it moves the inserted row of a split point to k.succ.

theorem TauCeti.GridState.insertPoint_last_relabelRows {n : ℕ} (x : GridState n) (newColumn : Fin (n + 1)) : relabelRows (finRotate (n + 1)) (x.insertPoint newColumn (Fin.last n)) = x.insertPoint newColumn 0

Cyclically permuting the rows moves an inserted top row to the bottom.

theorem TauCeti.GridState.splitPoint_last_relabelRows {n : ℕ} (x : GridState n) (newColumn : Fin (n + 1)) (s : Fin n) : relabelRows (finRotate (n + 1)) (x.splitPoint newColumn (Fin.last n) s) = x.splitPoint newColumn 0 s

Cyclically permuting the rows moves the inserted top row of a split point to the bottom.

theorem TauCeti.GridState.insertPoint_last_relabelColumns {n : ℕ} (x : GridState n) (newRow : Fin (n + 1)) : relabelColumns (finRotate (n + 1)) (x.insertPoint (Fin.last n) newRow) = x.insertPoint 0 newRow

Cyclically permuting the columns moves an inserted last column to the front.

theorem TauCeti.GridState.splitPoint_last_relabelColumns {n : ℕ} (x : GridState n) (newRow : Fin (n + 1)) (s : Fin n) : relabelColumns (finRotate (n + 1)) (x.splitPoint (Fin.last n) newRow s) = x.splitPoint 0 newRow s

Cyclically permuting the columns moves the inserted last column of a split point to the front.

def TauCeti.GridDiagram.stabilizeO {n : ℕ} (G : GridDiagram n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) : GridDiagram (n + 1)

Stabilize a grid diagram by splitting the O-marking in splitColumn.

The O state uses the two off-diagonal corners of the inserted row and column, while the new X-marking occupies their intersection. The elementary-move predicate below separately requires the inserted row and column to be adjacent to the split marking.

def TauCeti.GridDiagram.stabilizeX {n : ℕ} (G : GridDiagram n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) : GridDiagram (n + 1)

Stabilize a grid diagram by splitting the X-marking in splitColumn.

The X state uses the two off-diagonal corners of the inserted row and column, while the new O-marking occupies their intersection. The elementary-move predicate below separately requires the inserted row and column to be adjacent to the split marking.

@[simp]

theorem TauCeti.GridDiagram.stabilizeO_O {n : ℕ} (G : GridDiagram n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) : (G.stabilizeO newColumn newRow splitColumn).O = G.O.splitPoint newColumn newRow splitColumn

The O state of an O-stabilization is obtained by splitting the chosen O-marking.

@[simp]

theorem TauCeti.GridDiagram.stabilizeO_X {n : ℕ} (G : GridDiagram n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) : (G.stabilizeO newColumn newRow splitColumn).X = G.X.insertPoint newColumn newRow

The X state of an O-stabilization is obtained by inserting the new X-marking.

@[simp]

theorem TauCeti.GridDiagram.stabilizeX_O {n : ℕ} (G : GridDiagram n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) : (G.stabilizeX newColumn newRow splitColumn).O = G.O.insertPoint newColumn newRow

The O state of an X-stabilization is obtained by inserting the new O-marking.

@[simp]

theorem TauCeti.GridDiagram.stabilizeX_X {n : ℕ} (G : GridDiagram n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) : (G.stabilizeX newColumn newRow splitColumn).X = G.X.splitPoint newColumn newRow splitColumn

The X state of an X-stabilization is obtained by splitting the chosen X-marking.

theorem TauCeti.GridDiagram.stabilizeX_O_eq_castSucc_iff {n : ℕ} (G : GridDiagram n) (s : Fin n) (c : Fin (n + 1)) : (G.O.insertPoint s.castSucc (G.X.toPerm s).castSucc).toPerm c = (G.X.toPerm s).castSucc ↔ c = s.castSucc

In the stabilization splitting the X-marking of column s, the row (G.X s).castSucc carries its O-marking only in the new column s.castSucc.

theorem TauCeti.GridDiagram.stabilizeX_X_eq_castSucc_iff {n : ℕ} (G : GridDiagram n) (s : Fin n) (c : Fin (n + 1)) : (G.X.splitPoint s.castSucc (G.X.toPerm s).castSucc s).toPerm c = (G.X.toPerm s).castSucc ↔ c = s.succ

In the stabilization splitting the X-marking of column s, the row (G.X s).castSucc carries its X-marking only in the column s.succ.

theorem TauCeti.GridDiagram.predAbove_X_stabilizeX {n : ℕ} (G : GridDiagram n) (s : Fin n) (c : Fin (n + 1)) : (G.X.toPerm s).predAbove ((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).X.toPerm c) = G.X.toPerm (s.predAbove c)

In the stabilization splitting the X-marking of column s, the X-marking of each column collapses under Fin.predAbove onto the X-marking of G in the collapsed column: both X-markings of the new block collapse onto the split marking.

theorem TauCeti.GridDiagram.rotate_stabilizeO {n : ℕ} (G : GridDiagram n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) : (G.stabilizeO newColumn newRow splitColumn).rotate = G.rotate.stabilizeO newColumn.rev newRow.rev splitColumn.rev

Reversing both coordinates of an O-stabilization reverses the inserted row and column and the split column.

theorem TauCeti.GridDiagram.rotate_stabilizeX {n : ℕ} (G : GridDiagram n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) : (G.stabilizeX newColumn newRow splitColumn).rotate = G.rotate.stabilizeX newColumn.rev newRow.rev splitColumn.rev

Reversing both coordinates of an X-stabilization reverses the inserted row and column and the split column.

theorem TauCeti.GridDiagram.rotate_stabilizeX_succ {n : ℕ} (G : GridDiagram n) (s : Fin n) : (G.stabilizeX s.succ (G.X.toPerm s).succ s).rotate = G.rotate.stabilizeX s.rev.castSucc (G.rotate.X.toPerm s.rev).castSucc s.rev

The half-turn exchanges the two corner types of X-stabilization: the stabilization of G whose new O-marking is the north-east corner of the new block is carried to the stabilization of G.rotate whose new O-marking is the south-west corner.

@[simp]

theorem TauCeti.GridDiagram.stabilizeO_swapMarkings {n : ℕ} (G : GridDiagram n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) : (G.stabilizeO newColumn newRow splitColumn).swapMarkings = G.swapMarkings.stabilizeX newColumn newRow splitColumn

Exchanging the marking types turns an O-stabilization into an X-stabilization.

@[simp]

theorem TauCeti.GridDiagram.stabilizeX_swapMarkings {n : ℕ} (G : GridDiagram n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) : (G.stabilizeX newColumn newRow splitColumn).swapMarkings = G.swapMarkings.stabilizeO newColumn newRow splitColumn

Exchanging the marking types turns an X-stabilization into an O-stabilization.

theorem TauCeti.GridDiagram.stabilizeX_castSucc_X {n : ℕ} (G : GridDiagram n) (s : Fin n) (newRow : Fin (n + 1)) : (G.stabilizeX s.castSucc newRow s).X = G.X.insertPoint s.succ newRow

With the new column inserted just before the split column, the X state of an X-stabilization inserts its point in the column s.succ of the split marking.

theorem TauCeti.GridDiagram.stabilizeX_succ_X {n : ℕ} (G : GridDiagram n) (s : Fin n) (newRow : Fin (n + 1)) : (G.stabilizeX s.succ newRow s).X = G.X.insertPoint s.castSucc newRow

With the new column inserted just after the split column, the X state of an X-stabilization inserts its point in the column s.castSucc of the split marking.

theorem TauCeti.GridDiagram.stabilizeX_X_castSucc {n : ℕ} (G : GridDiagram n) (s : Fin n) : (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).X.toPerm s.castSucc = (G.X.toPerm s).succ

In the stabilization splitting the X-marking of column s with a new column just before it, the X-marking state has its point (G.X s).succ in the new column s.castSucc.

theorem TauCeti.GridDiagram.stabilizeX_X_swapColumns {n : ℕ} (G : GridDiagram n) (s : Fin n) : GridState.swapColumns s.succ s.castSucc (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).X = G.X.insertPoint s.succ (G.X.toPerm s).succ

In the stabilization splitting the X-marking of column s with a new column just before it, exchanging the two points of the X-marking state in the new block gives the X-marking state of G with the center (s.succ, (G.X s).succ) of the block inserted.

theorem TauCeti.GridDiagram.stabilizeX_X_succ_ne {n : ℕ} (G : GridDiagram n) (s : Fin n) : (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).X.toPerm s.succ ≠ (G.X.toPerm s).succ

In the stabilization splitting the X-marking of column s with a new column just before it, the X-marking state does not contain the center (s.succ, (G.X s).succ) of the new block.

theorem TauCeti.GridDiagram.stabilizeO_castSucc_eq_stabilizeX_succ {n : ℕ} (G : GridDiagram n) (s : Fin n) (newRow : Fin (n + 1)) : G.stabilizeO s.castSucc newRow s = G.stabilizeX s.succ newRow s

Splitting the O-marking of column s with a new column just before it gives the same diagram as splitting its X-marking with a new column just after it: both put an O at (s.succ, newRow) and an X at (s.castSucc, newRow).

theorem TauCeti.GridDiagram.stabilizeO_succ_eq_stabilizeX_castSucc {n : ℕ} (G : GridDiagram n) (s : Fin n) (newRow : Fin (n + 1)) : G.stabilizeO s.succ newRow s = G.stabilizeX s.castSucc newRow s

Splitting the O-marking of column s with a new column just after it gives the same diagram as splitting its X-marking with a new column just before it.

theorem TauCeti.GridDiagram.stabilizeX_castSucc_swapColumns {n : ℕ} (G : GridDiagram n) (s : Fin n) (newRow : Fin (n + 1)) : swapColumns s.castSucc s.succ (G.stabilizeX s.castSucc newRow s) = G.stabilizeX s.succ newRow s

Swapping the two columns of the new block exchanges the X-stabilizations with the new column on either side of the split column.

theorem TauCeti.GridDiagram.stabilizeX_swapRows {n : ℕ} (G : GridDiagram n) (newColumn : Fin (n + 1)) (k s : Fin n) : swapRows k.castSucc k.succ (G.stabilizeX newColumn k.castSucc s) = G.stabilizeX newColumn k.succ s

Swapping the new row k.castSucc of an X-stabilization with the old row k just above it moves the new row to k.succ.

theorem TauCeti.GridDiagram.stabilizeX_last_relabelRows {n : ℕ} (G : GridDiagram n) (newColumn : Fin (n + 1)) (s : Fin n) : relabelRows (finRotate (n + 1)) (G.stabilizeX newColumn (Fin.last n) s) = G.stabilizeX newColumn 0 s

Cyclically permuting the rows moves the new top row of an X-stabilization to the bottom.

theorem TauCeti.GridDiagram.stabilizeX_last_relabelColumns {n : ℕ} (G : GridDiagram n) (newRow : Fin (n + 1)) (s : Fin n) : relabelColumns (finRotate (n + 1)) (G.stabilizeX (Fin.last n) newRow s) = G.stabilizeX 0 newRow s

Cyclically permuting the columns moves the new last column of an X-stabilization to the front.

theorem TauCeti.GridDiagram.stabilizeO_last_relabelColumns {n : ℕ} (G : GridDiagram n) (newRow : Fin (n + 1)) (s : Fin n) : relabelColumns (finRotate (n + 1)) (G.stabilizeO (Fin.last n) newRow s) = G.stabilizeO 0 newRow s

Cyclically permuting the columns moves the new last column of an O-stabilization to the front.

def TauCeti.GridDiagram.IsOStabilization {n : ℕ} (G : GridDiagram n) (G' : GridDiagram (n + 1)) : Prop

Two grid diagrams differ by an elementary stabilization that splits an O-marking.

The new column is cyclically adjacent to the embedded split column, and the new row is cyclically adjacent to the embedded row of its O-marking. The two disjunctions independently choose the cyclic orientation, giving the four O-stabilization corner types.

theorem TauCeti.GridDiagram.isOStabilization_iff {n : ℕ} (G : GridDiagram n) (G' : GridDiagram (n + 1)) : G.IsOStabilization G' ↔ ∃ (newColumn : Fin (n + 1)) (newRow : Fin (n + 1)) (splitColumn : Fin n), ((finRotate (n + 1)) newColumn = newColumn.succAbove splitColumn ∨ (finRotate (n + 1)) (newColumn.succAbove splitColumn) = newColumn) ∧ ((finRotate (n + 1)) newRow = newRow.succAbove (G.O.toPerm splitColumn) ∨ (finRotate (n + 1)) (newRow.succAbove (G.O.toPerm splitColumn)) = newRow) ∧ G' = G.stabilizeO newColumn newRow splitColumn

An elementary O-stabilization is the O-stabilization construction at a new row and column cyclically adjacent to the split marking.

theorem TauCeti.GridDiagram.isOStabilization_stabilizeO {n : ℕ} (G : GridDiagram n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) (hColumn : (finRotate (n + 1)) newColumn = newColumn.succAbove splitColumn ∨ (finRotate (n + 1)) (newColumn.succAbove splitColumn) = newColumn) (hRow : (finRotate (n + 1)) newRow = newRow.succAbove (G.O.toPerm splitColumn) ∨ (finRotate (n + 1)) (newRow.succAbove (G.O.toPerm splitColumn)) = newRow) : G.IsOStabilization (G.stabilizeO newColumn newRow splitColumn)

A local O-stabilization construction is an elementary O-stabilization.

theorem TauCeti.GridDiagram.isOStabilization_stabilizeO_castSucc {n : ℕ} (G : GridDiagram n) (splitColumn : Fin n) : G.IsOStabilization (G.stabilizeO splitColumn.castSucc (G.O.toPerm splitColumn).castSucc splitColumn)

Inserting a column immediately before splitColumn and a row immediately before its O-marking gives an elementary O-stabilization.

def TauCeti.GridDiagram.IsXStabilization {n : ℕ} (G : GridDiagram n) (G' : GridDiagram (n + 1)) : Prop

Two grid diagrams differ by an elementary stabilization that splits an X-marking.

The new column is cyclically adjacent to the embedded split column, and the new row is cyclically adjacent to the embedded row of its X-marking. The two disjunctions independently choose the cyclic orientation, giving the four X-stabilization corner types.

theorem TauCeti.GridDiagram.isXStabilization_iff {n : ℕ} (G : GridDiagram n) (G' : GridDiagram (n + 1)) : G.IsXStabilization G' ↔ ∃ (newColumn : Fin (n + 1)) (newRow : Fin (n + 1)) (splitColumn : Fin n), ((finRotate (n + 1)) newColumn = newColumn.succAbove splitColumn ∨ (finRotate (n + 1)) (newColumn.succAbove splitColumn) = newColumn) ∧ ((finRotate (n + 1)) newRow = newRow.succAbove (G.X.toPerm splitColumn) ∨ (finRotate (n + 1)) (newRow.succAbove (G.X.toPerm splitColumn)) = newRow) ∧ G' = G.stabilizeX newColumn newRow splitColumn

An elementary X-stabilization is the X-stabilization construction at a new row and column cyclically adjacent to the split marking.

theorem TauCeti.GridDiagram.isXStabilization_stabilizeX {n : ℕ} (G : GridDiagram n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) (hColumn : (finRotate (n + 1)) newColumn = newColumn.succAbove splitColumn ∨ (finRotate (n + 1)) (newColumn.succAbove splitColumn) = newColumn) (hRow : (finRotate (n + 1)) newRow = newRow.succAbove (G.X.toPerm splitColumn) ∨ (finRotate (n + 1)) (newRow.succAbove (G.X.toPerm splitColumn)) = newRow) : G.IsXStabilization (G.stabilizeX newColumn newRow splitColumn)

A local X-stabilization construction is an elementary X-stabilization.

theorem TauCeti.GridDiagram.isXStabilization_stabilizeX_castSucc {n : ℕ} (G : GridDiagram n) (splitColumn : Fin n) : G.IsXStabilization (G.stabilizeX splitColumn.castSucc (G.X.toPerm splitColumn).castSucc splitColumn)

Inserting a column immediately before splitColumn and a row immediately before its X-marking gives an elementary X-stabilization.

@[simp]

theorem TauCeti.GridDiagram.isOStabilization_swapMarkings {n : ℕ} (G : GridDiagram n) (G' : GridDiagram (n + 1)) : G.swapMarkings.IsOStabilization G'.swapMarkings ↔ G.IsXStabilization G'

Exchanging the marking types turns an O-stabilization relation into an X-stabilization relation.

@[simp]

theorem TauCeti.GridDiagram.isXStabilization_swapMarkings {n : ℕ} (G : GridDiagram n) (G' : GridDiagram (n + 1)) : G.swapMarkings.IsXStabilization G'.swapMarkings ↔ G.IsOStabilization G'

Exchanging the marking types turns an X-stabilization relation into an O-stabilization relation.

def TauCeti.GridDiagram.IsStabilization {n : ℕ} (G : GridDiagram n) (G' : GridDiagram (n + 1)) : Prop

One elementary grid stabilization, splitting either an O- or an X-marking.

theorem TauCeti.GridDiagram.isStabilization_iff {n : ℕ} (G : GridDiagram n) (G' : GridDiagram (n + 1)) : G.IsStabilization G' ↔ G.IsOStabilization G' ∨ G.IsXStabilization G'

An elementary stabilization splits either an O-marking or an X-marking.

@[simp]

theorem TauCeti.GridDiagram.isStabilization_swapMarkings {n : ℕ} (G : GridDiagram n) (G' : GridDiagram (n + 1)) : G.swapMarkings.IsStabilization G'.swapMarkings ↔ G.IsStabilization G'

Exchanging the marking types preserves the elementary stabilization relation.

def TauCeti.GridDiagram.IsDestabilization {n : ℕ} (G' : GridDiagram (n + 1)) (G : GridDiagram n) : Prop

One elementary grid destabilization, oriented from the larger diagram to the smaller one.

theorem TauCeti.GridDiagram.isDestabilization_iff_isStabilization {n : ℕ} (G' : GridDiagram (n + 1)) (G : GridDiagram n) : G'.IsDestabilization G ↔ G.IsStabilization G'

A destabilization from the larger diagram to the smaller one is the reverse orientation of the corresponding stabilization.

@[simp]

theorem TauCeti.GridDiagram.isDestabilization_swapMarkings {n : ℕ} (G' : GridDiagram (n + 1)) (G : GridDiagram n) : G'.swapMarkings.IsDestabilization G.swapMarkings ↔ G'.IsDestabilization G

Exchanging the marking types preserves the elementary destabilization relation.