Hexagon shapes in a mixed-side recut

Consider two rectangles whose common grid line is terminal for the first and initial for the second, or initial for the first and terminal for the second, as for a pentagon turning on one side of the replaced grid line followed by a pentagon turning on the other side. Off the diagonal this line is their only common side. When both rectangles are empty, the recut from the proof of ∂² = 0 cuts their union the other way. If the turn rows are placed as for such a pentagon pair, no hexagon composite has this recut as its underlying rectangle decomposition: one recut rectangle has no side on the replaced grid line, and the other misses one of the two turn rows. This is the mixed-side counterpart of SameSideRecut.lean, and it serves the homotopy equations of a column commutation and of a crossing change alike.

Main results

• toRectangleDecomposition_ne_recut_of_right_eq_left and toRectangleDecomposition_ne_recut_of_left_eq_right, in the namespace TauCeti.GridHexagonCompositeDecomposition: the recut of two empty rectangles sharing the replaced grid line with opposite orientations, with the two turn rows placed as for a mixed-side pentagon pair, underlies no hexagon composite.

References

This is the mixed-side case of the hexagon--rectangle juxtaposition argument of Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.1, and Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Section 3.1, Proposition 3.2 (arXiv:math/0610559).

theorem TauCeti.GridHexagonCompositeDecomposition.toRectangleDecomposition_ne_recut_of_right_eq_left {n : ℕ} {a s s' : Fin n} {x z : GridState n} {D : GridRectangleDecomposition x z} (hright : D.first.right = (finRotate n) a) (hleft : D.second.left = (finRotate n) a) (hone : D.HasOneCommonSide) (hfirst : D.first.IsEmpty) (hsecond : D.second.IsEmpty) (hs : s ∈ Grid.cIco D.first.bottom D.first.top) (hs' : s' ∈ Grid.cIco D.first.bottom D.second.top) (F : GridHexagonCompositeDecomposition a s s' x z) : F.toRectangleDecomposition ≠ D.recut hone hfirst hsecond

Let the empty rectangles of an off-diagonal decomposition D share the grid line finRotate n a, terminal for the first and initial for the second, as the rectangles of a terminal-side pentagon followed by an initial-side one do. If the first rectangle contains the row s and the rows from its bottom up to the top of the second contain s', then the recut of D underlies no hexagon composite with turn rows s and s': one recut rectangle has no side on the grid line, and the other misses one of the two rows.

theorem TauCeti.GridHexagonCompositeDecomposition.toRectangleDecomposition_ne_recut_of_left_eq_right {n : ℕ} {a s s' : Fin n} {x z : GridState n} {D : GridRectangleDecomposition x z} (hleft : D.first.left = (finRotate n) a) (hright : D.second.right = (finRotate n) a) (hone : D.HasOneCommonSide) (hfirst : D.first.IsEmpty) (hsecond : D.second.IsEmpty) (hs : s ∈ Grid.cIco D.first.bottom D.first.top) (hs' : s' ∈ Grid.cIco D.second.bottom D.first.top) (F : GridHexagonCompositeDecomposition a s s' x z) : F.toRectangleDecomposition ≠ D.recut hone hfirst hsecond

Let the empty rectangles of an off-diagonal decomposition D share the grid line finRotate n a, initial for the first and terminal for the second, as the rectangles of an initial-side pentagon followed by a terminal-side one do. If the first rectangle contains the row s and the rows from the bottom of the second up to the top of the first contain s', then the recut of D underlies no hexagon composite with turn rows s and s': one recut rectangle has no side on the grid line, and the other misses one of the two rows.