Cyclic order for overlapping empty grid rectangles

Two composable rectangles in a nondiagonal term of the grid differential square either have disjoint side columns or share exactly one side column. In the latter case, constructing the alternate two-rectangle decomposition requires knowing the cyclic order of the three side columns and of the three rows at their corners.

This file proves the order constraint in all four orientations of the common column. When the common column is the initial side of both rectangles, the two remaining side columns lie on opposite choices of the cyclic arc from the common column, while emptiness forces the common corner row to lie strictly between the other two rows. The terminal--terminal orientation is the reversed counterpart. The mixed orientations follow by diagonally reflecting a decomposition, which exchanges column and row order. Thus every one-common-side pair forms one of the L-shaped configurations that can be recut along the other internal edge.

The proof uses emptiness for both the source and target state of a rectangle. If the third column lies in the first rectangle's column interior, its state point must miss that rectangle's row interior; if it lies in the second rectangle's column interior, the corresponding point must miss the second row interior. Circular-order trichotomy turns either exclusion into the same cyclic row order.

Main results

• TauCeti.GridRectangleDecomposition.side_eq_cases_of_hasOneCommonSide: the four possible orientations of the unique common side, with the two other sides distinct.
• TauCeti.GridRectangleDecomposition.cyclicOrder_of_isEmpty_of_left_eq_left: when the common side is the initial side of both empty rectangles, their other side columns determine one of two cyclic orders and the shared corner row lies between the other two rows.
• TauCeti.GridRectangleDecomposition.cyclicOrder_of_isEmpty_of_right_eq_right: the corresponding order constraint when the common side is terminal for both rectangles.
• TauCeti.GridRectangleDecomposition.cyclicOrder_of_isEmpty_of_left_eq_right and cyclicOrder_of_isEmpty_of_right_eq_left: the two mixed-orientation constraints.
• TauCeti.GridRectangleBetween.bottom_mem_cIoo_and_top_eq_of_right_eq_right and top_mem_cIoo_and_bottom_eq_of_left_eq_left: two composable empty rectangles with one common side of the same orientation are stacked along it.

References

The cyclic-order argument follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.6.

theorem TauCeti.GridRectangleDecomposition.second_bottom_eq_first_top_of_left_eq_left {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (hleft : D.first.left = D.second.left) : D.second.bottom = D.first.top

When two rectangles share their initial side, the second rectangle's bottom row is the first rectangle's top row.

theorem TauCeti.GridRectangleDecomposition.second_bottom_eq_first_bottom_of_right_eq_left {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (hcommon : D.first.right = D.second.left) : D.second.bottom = D.first.bottom

When the terminal side of the first rectangle is the initial side of the second, the two rectangles have the same bottom row.

theorem TauCeti.GridRectangleDecomposition.second_top_eq_first_top_of_left_eq_right {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (hcommon : D.first.left = D.second.right) : D.second.top = D.first.top

When the initial side of the first rectangle is the terminal side of the second, the two rectangles have the same top row.

theorem TauCeti.GridRectangleDecomposition.cyclicOrder_of_isEmpty_of_left_eq_left {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (hleft : D.first.left = D.second.left) (hright : D.first.right ≠ D.second.right) (hfirst : D.first.IsEmpty) (hsecond : D.second.IsEmpty) : (D.first.right ∈ Grid.cIoo D.first.left D.second.right ∨ D.second.right ∈ Grid.cIoo D.first.left D.first.right) ∧ D.first.top ∈ Grid.cIoo D.first.bottom D.second.top

Suppose the two empty rectangles in a decomposition share their initial side column and no other side. Then their two terminal sides occur in one of the two possible cyclic orders around the common side, while the row of the common corner lies strictly between the other two corner rows.

The disjunction records which L-shaped repartition applies. The row order is independent of that choice: emptiness of the rectangle whose column interval contains the third side forces the corresponding third corner outside its row interior.

theorem TauCeti.GridRectangleDecomposition.cyclicOrder_of_isEmpty_of_right_eq_right {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (hright : D.first.right = D.second.right) (hleft : D.first.left ≠ D.second.left) (hfirst : D.first.IsEmpty) (hsecond : D.second.IsEmpty) : (D.first.left ∈ Grid.cIoo D.second.left D.first.right ∨ D.second.left ∈ Grid.cIoo D.first.left D.first.right) ∧ D.first.bottom ∈ Grid.cIoo D.second.bottom D.first.top

Suppose the two empty rectangles share their terminal side column and no other side. Then their two initial sides occur in one of the two possible cyclic orders around the common side, while the row of the common corner lies strictly between the other two corner rows.

theorem TauCeti.GridRectangleDecomposition.cyclicOrder_of_isEmpty_of_left_eq_right {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (hcommon : D.first.left = D.second.right) (hother : D.first.right ≠ D.second.left) (hfirst : D.first.IsEmpty) (hsecond : D.second.IsEmpty) : D.first.right ∈ Grid.cIoo D.first.left D.second.left ∧ (D.first.bottom ∈ Grid.cIoo D.second.bottom D.first.top ∨ D.second.bottom ∈ Grid.cIoo D.first.bottom D.first.top)

Suppose the first empty rectangle's initial side is the second one's terminal side, with no other common side. The other side columns have a fixed cyclic order, while the three corner rows occur in one of the two orders obtained by reflecting the terminal--terminal case.

theorem TauCeti.GridRectangleDecomposition.cyclicOrder_of_isEmpty_of_right_eq_left {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (hcommon : D.first.right = D.second.left) (hother : D.first.left ≠ D.second.right) (hfirst : D.first.IsEmpty) (hsecond : D.second.IsEmpty) : D.first.right ∈ Grid.cIoo D.first.left D.second.right ∧ (D.first.top ∈ Grid.cIoo D.first.bottom D.second.top ∨ D.second.top ∈ Grid.cIoo D.first.bottom D.first.top)

Suppose the first empty rectangle's terminal side is the second one's initial side, with no other common side. The other side columns have a fixed cyclic order, while the three corner rows occur in one of the two orders obtained by reflecting the initial--initial case.

theorem TauCeti.GridRectangleBetween.bottom_mem_cIoo_and_top_eq_of_right_eq_right {n : ℕ} {x y z : GridState n} (P : GridRectangleBetween x y) (Q : GridRectangleBetween y z) (hright : P.right = Q.right) (hleft : P.left ≠ Q.left) (hP : P.IsEmpty) (hQ : Q.IsEmpty) : P.bottom ∈ Grid.cIoo Q.bottom P.top ∧ Q.top = P.bottom

Two composable empty rectangles sharing their terminal side column but not their initial one are stacked along it: the second ends at the row where the first starts, and this row lies strictly between the bottom of the second and the top of the first.

theorem TauCeti.GridRectangleBetween.top_mem_cIoo_and_bottom_eq_of_left_eq_left {n : ℕ} {x y z : GridState n} (P : GridRectangleBetween x y) (Q : GridRectangleBetween y z) (hleft : P.left = Q.left) (hright : P.right ≠ Q.right) (hP : P.IsEmpty) (hQ : Q.IsEmpty) : P.top ∈ Grid.cIoo P.bottom Q.top ∧ Q.bottom = P.top

Two composable empty rectangles sharing their initial side column but not their terminal one are stacked along it: the second starts at the row where the first ends, and this row lies strictly between the bottom of the first and the top of the second.