Geometry of mixed-side rectangle recuts

Two composable empty grid rectangles with exactly one common side admit a canonical recut. When the common side is terminal for one rectangle and initial for the other, the generic recut API records its rows but not its side columns. This file reconstructs those columns from the source and intermediate grid states, giving a complete geometric description in both mixed orientations.

The two alternatives in each result are the two possible cyclic orders of the three corner rows. In either branch, the displayed side and row equalities determine which recut rectangle can be promoted to a polygon with prescribed turn data. This is the interface used by juxtaposition arguments for grid differentials and commutation maps.

Main results

• TauCeti.GridRectangleDecomposition.IsRecutOfLeftEqRight.recut_geometry: the two geometric branches of any recut when the first rectangle's initial side is the second rectangle's terminal side.
• TauCeti.GridRectangleDecomposition.IsRecutOfRightEqLeft.recut_geometry: the two geometric branches of any recut for the opposite mixed orientation.
• TauCeti.GridRectangleDecomposition.recut_geometry_of_left_eq_right and TauCeti.GridRectangleDecomposition.recut_geometry_of_right_eq_left: the same descriptions specialized to the canonical recut.

References

The mixed recuts are the overlapping-domain decompositions in Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.6. Their use for commutation domains follows Section 5.1 and Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Section 3.1 (arXiv:math/0610559).

theorem TauCeti.GridRectangleDecomposition.IsRecutOfLeftEqRight.recut_geometry {n : ℕ} {x z : GridState n} {D E : GridRectangleDecomposition x z} (hdata : D.IsRecutOfLeftEqRight E) (hone : D.HasOneCommonSide) : D.first.bottom ∈ Grid.cIoo D.second.bottom D.first.top ∧ E.first.left = D.second.left ∧ E.first.right = D.first.left ∧ E.second.left = D.second.left ∧ E.second.right = D.first.right ∧ E.first.bottom = D.second.bottom ∧ E.first.top = D.first.bottom ∧ E.second.bottom = D.first.bottom ∧ E.second.top = D.first.top ∨ D.second.bottom ∈ Grid.cIoo D.first.bottom D.first.top ∧ E.first.left = D.second.left ∧ E.first.right = D.first.right ∧ E.second.left = D.first.left ∧ E.second.right = D.first.right ∧ E.first.bottom = D.second.bottom ∧ E.first.top = D.first.top ∧ E.second.bottom = D.first.bottom ∧ E.second.top = D.second.bottom

The complete geometry of a recut when the first rectangle's initial side is the second rectangle's terminal side. The row containing the remaining corner selects whether the recut rectangles share their initial or terminal side.

theorem TauCeti.GridRectangleDecomposition.IsRecutOfRightEqLeft.recut_geometry {n : ℕ} {x z : GridState n} {D E : GridRectangleDecomposition x z} (hdata : D.IsRecutOfRightEqLeft E) (hone : D.HasOneCommonSide) : D.first.top ∈ Grid.cIoo D.first.bottom D.second.top ∧ E.first.left = D.first.right ∧ E.first.right = D.second.right ∧ E.second.left = D.first.left ∧ E.second.right = D.second.right ∧ E.first.bottom = D.first.top ∧ E.first.top = D.second.top ∧ E.second.bottom = D.first.bottom ∧ E.second.top = D.first.top ∨ D.second.top ∈ Grid.cIoo D.first.bottom D.first.top ∧ E.first.left = D.first.left ∧ E.first.right = D.second.right ∧ E.second.left = D.first.left ∧ E.second.right = D.first.right ∧ E.first.bottom = D.first.bottom ∧ E.first.top = D.second.top ∧ E.second.bottom = D.second.top ∧ E.second.top = D.first.top

The complete geometry of a recut when the first rectangle's terminal side is the second rectangle's initial side. The row containing the remaining corner selects whether the recut rectangles share their terminal or initial side.

theorem TauCeti.GridRectangleDecomposition.recut_geometry_of_left_eq_right {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (hcommon : D.first.left = D.second.right) (hone : D.HasOneCommonSide) (hfirst : D.first.IsEmpty) (hsecond : D.second.IsEmpty) : have E := D.recut hone hfirst hsecond; D.first.bottom ∈ Grid.cIoo D.second.bottom D.first.top ∧ E.first.left = D.second.left ∧ E.first.right = D.first.left ∧ E.second.left = D.second.left ∧ E.second.right = D.first.right ∧ E.first.bottom = D.second.bottom ∧ E.first.top = D.first.bottom ∧ E.second.bottom = D.first.bottom ∧ E.second.top = D.first.top ∨ D.second.bottom ∈ Grid.cIoo D.first.bottom D.first.top ∧ E.first.left = D.second.left ∧ E.first.right = D.first.right ∧ E.second.left = D.first.left ∧ E.second.right = D.first.right ∧ E.first.bottom = D.second.bottom ∧ E.first.top = D.first.top ∧ E.second.bottom = D.first.bottom ∧ E.second.top = D.second.bottom

The complete geometry of the canonical recut when the first rectangle's initial side is the second rectangle's terminal side. The row containing the remaining corner selects whether the recut rectangles share their initial or terminal side.

theorem TauCeti.GridRectangleDecomposition.recut_geometry_of_right_eq_left {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (hcommon : D.first.right = D.second.left) (hone : D.HasOneCommonSide) (hfirst : D.first.IsEmpty) (hsecond : D.second.IsEmpty) : have E := D.recut hone hfirst hsecond; D.first.top ∈ Grid.cIoo D.first.bottom D.second.top ∧ E.first.left = D.first.right ∧ E.first.right = D.second.right ∧ E.second.left = D.first.left ∧ E.second.right = D.second.right ∧ E.first.bottom = D.first.top ∧ E.first.top = D.second.top ∧ E.second.bottom = D.first.bottom ∧ E.second.top = D.first.top ∨ D.second.top ∈ Grid.cIoo D.first.bottom D.first.top ∧ E.first.left = D.first.left ∧ E.first.right = D.second.right ∧ E.second.left = D.first.left ∧ E.second.right = D.first.right ∧ E.first.bottom = D.first.bottom ∧ E.first.top = D.second.top ∧ E.second.bottom = D.second.top ∧ E.second.top = D.first.top

The complete geometry of the canonical recut when the first rectangle's terminal side is the second rectangle's initial side. The row containing the remaining corner selects whether the recut rectangles share their terminal or initial side.