A two-rectangle bound for oriented rectangles between grid states

An oriented rectangle R : GridRectangleBetween x y is determined by its two side columns R.left, R.right: away from those columns the two states agree, and at those columns they exchange rows (RectangleSwap.lean). This file pins down the uniform two-rectangle upper bound between two fixed grid states, and the exact count once one such rectangle exists.

The key observation is purely about the side columns. A column c is a side column of R exactly when the two states differ there: if c is neither R.left nor R.right then y c = x c, and at a side column the states genuinely disagree because the source permutation is injective. So the unordered pair of side columns is forced — it is the set of columns where x and y differ — and a rectangle between x and y is determined up to the order of its two side columns. Reversing the two side columns gives the other oriented rectangle (swapSides), so there are at most two oriented rectangles, and exactly two whenever at least one exists. The separate RectangleSwap.lean file records the transposition/existence criterion.

This is the finiteness backbone of the grid differential: the coefficient of y in the fully blocked differential of x counts a sub-collection of these at-most-two rectangles, so the differential of a generator is supported on the column-transposition neighbours of that generator.

Main results

• TauCeti.GridRectangleBetween.apply_ne_iff: a column is a side column exactly when the two states differ there.
• TauCeti.GridRectangleBetween.eq_or_eq_swapSides: any two oriented rectangles between the same states are equal or differ by swapSides.
• TauCeti.GridRectangleBetween.univ_eq_pair, TauCeti.GridRectangleBetween.card_le_two, TauCeti.GridRectangleBetween.card_eq_two_of_nonempty: there are at most two oriented rectangles between two states, and exactly two when there is at least one.
• TauCeti.GridRectangleBetween.card_emptyRectangles_le_two: there are at most two empty rectangles between two states.

References

The count of rectangles between two states is the finiteness fact underlying the grid differential. The statement that exactly two rectangles connect two states differing by a transposition follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.

theorem TauCeti.GridRectangleBetween.apply_ne_iff {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (c : Fin n) : y.toPerm c ≠ x.toPerm c ↔ c = R.left ∨ c = R.right

A column is a side column of the rectangle exactly when the two states read different rows there. Away from the two side columns the states agree, and at a side column the source permutation is injective on the two distinct side columns, so the read rows differ.

theorem TauCeti.GridRectangleBetween.left_apply_ne {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : y.toPerm R.left ≠ x.toPerm R.left

The states differ at the initial side column.

theorem TauCeti.GridRectangleBetween.right_apply_ne {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : y.toPerm R.right ≠ x.toPerm R.right

The states differ at the terminal side column.

theorem TauCeti.GridRectangleBetween.eq_or_eq_swapSides {n : ℕ} {x y : GridState n} (R S : GridRectangleBetween x y) : S = R ∨ S = R.swapSides

Any oriented rectangle between the same two states is R or its side swap R.swapSides. Its two side columns are exactly the two columns where x and y differ, which are R.left and R.right, so its ordered side pair is one of the two orderings of that pair.

theorem TauCeti.GridRectangleBetween.univ_eq_pair {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : Finset.univ = {R, R.swapSides}

Given one oriented rectangle between two states, the oriented rectangles between them are exactly the pair {R, R.swapSides}.

theorem TauCeti.GridRectangleBetween.card_eq_two_of_nonempty {n : ℕ} {x y : GridState n} [Nonempty (GridRectangleBetween x y)] : Fintype.card (GridRectangleBetween x y) = 2

When there is at least one oriented rectangle between two states, there are exactly two: the chosen one and its side swap.

theorem TauCeti.GridRectangleBetween.card_le_two {n : ℕ} {x y : GridState n} (s : Finset (GridRectangleBetween x y)) : s.card ≤ 2

Any finite subcollection of oriented rectangles between two states has cardinality at most two.

theorem TauCeti.GridRectangleBetween.card_emptyRectangles_le_two {n : ℕ} (x y : GridState n) : (emptyRectangles x y).card ≤ 2

There are at most two empty oriented rectangles between two grid states.