Recutting two-step grid rectangle decompositions with a mixed common side

Two composable empty rectangles sharing exactly one side column form an L-shaped domain with a second cut uniquely characterized by its computed side rows and row configuration. The cases where the common column is initial for both rectangles or terminal for both are handled in Recut.Initial and Recut.Terminal. This file treats the two remaining orientations: the common column is initial for one rectangle and terminal for the other.

Diagonal reflection turns either mixed column orientation into one of the same-side orientations. Reflecting its recut back gives the required second decomposition. Accordingly, its side rows rather than its side columns are computed explicitly. The reflected domain is still a repartition, so the new rectangles cover the same squares as the old ones.

Main results

• TauCeti.GridRectangleDecomposition.exists_isRepartition_of_isEmpty_of_left_eq_right and exists_isRepartition_of_isEmpty_of_right_eq_left: the two mixed common-side configurations admit recuts through different intermediate states, uniquely characterized by their computed side rows and row configurations, with both new rectangles empty.

References

The recut is the overlapping-rectangle case of Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.6.

Initial side of the first rectangle equals terminal side of the second

theorem TauCeti.GridRectangleDecomposition.exists_isRepartition_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) : ∃! E : GridRectangleDecomposition x z, D.IsRepartition E ∧ E.middle ≠ D.middle ∧ E.first.IsEmpty ∧ E.second.IsEmpty ∧ E.first.bottom = D.second.bottom ∧ E.second.bottom = D.first.bottom ∧ (D.first.bottom ∈ Grid.cIoo D.second.bottom D.first.top ∧ E.middle = GridState.swapRows D.second.bottom D.first.bottom x ∧ E.first.top = D.first.bottom ∧ E.second.top = D.first.top ∨ D.second.bottom ∈ Grid.cIoo D.first.bottom D.first.top ∧ E.middle = GridState.swapRows D.second.bottom D.first.top x ∧ E.first.top = D.first.top ∧ E.second.top = D.second.bottom)

Two composable empty rectangles whose common column is the initial side of the first and the terminal side of the second admit a recut through a different intermediate state, unique among decompositions with the stated side rows and row configuration.

The two alternatives record which of the two noncommon corner rows lies inside the other row span. They compute all four side rows of the recut and hence determine it uniquely after diagonal reflection.

Terminal side of the first rectangle equals initial side of the second

theorem TauCeti.GridRectangleDecomposition.exists_isRepartition_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) : ∃! E : GridRectangleDecomposition x z, D.IsRepartition E ∧ E.middle ≠ D.middle ∧ E.first.IsEmpty ∧ E.second.IsEmpty ∧ E.first.top = D.second.top ∧ E.second.top = D.first.top ∧ (D.first.top ∈ Grid.cIoo D.first.bottom D.second.top ∧ E.middle = GridState.swapRows D.first.top D.second.top x ∧ E.first.bottom = D.first.top ∧ E.second.bottom = D.first.bottom ∨ D.second.top ∈ Grid.cIoo D.first.bottom D.first.top ∧ E.middle = GridState.swapRows D.first.bottom D.second.top x ∧ E.first.bottom = D.first.bottom ∧ E.second.bottom = D.second.top)

Two composable empty rectangles whose common column is the terminal side of the first and the initial side of the second admit a recut through a different intermediate state, unique among decompositions with the stated side rows and row configuration.

The two alternatives record which of the two noncommon corner rows lies inside the other row span. They compute all four side rows of the recut and hence determine it uniquely after diagonal reflection.