Recutting a two-step grid rectangle decomposition sharing its terminal side column

A nondiagonal term in the square of the unblocked grid differential ∂⁻ is a pair of composable empty rectangles whose two pairs of side columns are either disjoint or share exactly one column. In the second case the two rectangles meet at a corner and their union is an L-shaped hexagon, which can be cut into two rectangles in exactly one other way. This file builds that alternate cut in the orientation where the two rectangles share their terminal side column, the mirror of the initial-side orientation built in TauCeti.KnotTheory.Grid.Differential.Square.Recut.Initial.

The two orientations are genuinely different configurations rather than one another's image under a symmetry of the situation. Reversing a rectangle (to the one from y to x) does exchange its two side columns, but it spans the complementary arc of columns and hence does not preserve emptiness; and the diagonal reflection GridRectangleDecomposition.transpose exchanges side columns with corner rows, so it carries a common terminal side column to a coincidence of corner rows rather than to a common initial side column. Both cuts are therefore proved directly, from the same geometric inputs: the cyclic order forced by emptiness (cyclicOrder_of_isEmpty_of_right_eq_right) and the finite-domain repartition identities for the covered squares (GridRectangle.coveredSquares_union_eq_of_mem_cIoo_common_right and its complementary form). Emptiness of the new rectangles is not part of those identities: it is proved here, and it is where emptiness of both old rectangles is used, one for the columns below the cut and one for the columns above it.

The relation between the two cuts is packaged as GridRectangleDecomposition.IsRepartition: the rectangles of each cut cover disjoint sets of squares, and the two unions agree. The geometric construction separately proves that the two cuts have different intermediate states, and records the intermediate state and the side columns of the new cut.

Main results

• TauCeti.GridRectangleDecomposition.exists_isRepartition_of_isEmpty_of_right_eq_right: two composable empty rectangles sharing their terminal side column admit a recut by two empty rectangles, whose intermediate state and side columns are computed.

References

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

The two old rectangles read in the source state

Building the recut

The recut of a decomposition sharing its terminal side column

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

Two composable empty rectangles that share their terminal side column and no other side admit a recut: the L-shaped union of their domains has a second decomposition into two empty rectangles, through a different intermediate grid state.

The two cyclic orders of the three side columns give the two shapes of the new cut, and in each of them the intermediate state and the four side columns of the recut are computed, which by GridRectangleDecomposition.ext determine it.

Emptiness of both rectangles enters twice. It fixes the cyclic order of the three side columns and of the three corner rows, and it then transfers to the two new rectangles: the part of a new rectangle below the cut is controlled by the second old rectangle and the part above it by the first.