Juxtaposing toroidal grid rectangles

Two rectangles in a nondiagonal term of the grid differential square can share one corner. Cutting their L-shaped union along its other internal edge gives the alternate two-rectangle decomposition. This file proves the finite-domain identities behind that cut.

The one-dimensional input is that an interior point b cuts the clockwise half-open interval from a to c into the disjoint intervals from a to b and from b to c. Applying this in both coordinates gives four forms of the L-shaped identity for GridRectangle.coveredSquares, two for each of the two ways the two rectangles being cut apart can share a vertical side: the shared side may be the initial side of both, or the terminal side of both. In each of those two configurations the third vertical side lies on one of the two arcs cut out by the other two, and the resulting column cut runs along a different line. The coordinate cuts and GridRectangle.disjoint_coveredSquares_iff ensure that all displayed unions are honest partitions, not merely equal unions with hidden overlap.

These identities use the square-centred, half-open domains counted by the unblocked grid differential. They are the geometric step needed to show that the alternate decomposition preserves X-avoidance and the product of the O-monomial weights in the one-common-side case.

Main results

The following results are in the TauCeti.GridRectangle namespace:

• coveredSquares_union_eq_of_mem_cIoo: the first L-shaped repartition identity, for two rectangles sharing their initial vertical side.
• coveredSquares_union_eq_of_mem_cIoo_complementary_col_cut: the complementary column-cut orientation of the same identity.
• coveredSquares_union_eq_of_mem_cIoo_common_right, coveredSquares_union_eq_of_mem_cIoo_common_right_complementary_col_cut: the two identities for rectangles sharing their terminal vertical side instead.
• disjoint_coveredSquares_of_row_cut, disjoint_coveredSquares_of_col_cut: the two rectangles on either side of a row or column cut cover disjoint sets of squares.

References

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

theorem TauCeti.GridRectangle.disjoint_coveredSquares_of_row_cut {n : ℕ} {a b c d u v w : Fin n} (hrow : v ∈ Grid.cIoo u w) : Disjoint { left := a, right := b, bottom := u, top := v }.coveredSquares { left := c, right := d, bottom := v, top := w }.coveredSquares

Rectangles on opposite sides of a row cut cover disjoint sets of squares, independently of their column spans.

theorem TauCeti.GridRectangle.disjoint_coveredSquares_of_col_cut {n : ℕ} {a b c u v w t : Fin n} (hcol : b ∈ Grid.cIoo a c) : Disjoint { left := a, right := b, bottom := u, top := v }.coveredSquares { left := b, right := c, bottom := w, top := t }.coveredSquares

Rectangles on opposite sides of a column cut cover disjoint sets of squares, independently of their row spans.

theorem TauCeti.GridRectangle.coveredSquares_union_eq_of_mem_cIoo {n : ℕ} {a b c u v w : Fin n} (hcol : b ∈ Grid.cIoo a c) (hrow : v ∈ Grid.cIoo u w) : { left := a, right := b, bottom := u, top := v }.coveredSquares ∪ { left := a, right := c, bottom := v, top := w }.coveredSquares = { left := b, right := c, bottom := v, top := w }.coveredSquares ∪ { left := a, right := b, bottom := u, top := w }.coveredSquares

If b and v lie between the corresponding outer sides, the two indicated pairs of rectangles are the two cuts of the same L-shaped set of squares.

theorem TauCeti.GridRectangle.coveredSquares_union_eq_of_mem_cIoo_complementary_col_cut {n : ℕ} {a b c u v w : Fin n} (hcol : c ∈ Grid.cIoo a b) (hrow : v ∈ Grid.cIoo u w) : { left := a, right := b, bottom := u, top := v }.coveredSquares ∪ { left := a, right := c, bottom := v, top := w }.coveredSquares = { left := a, right := c, bottom := u, top := w }.coveredSquares ∪ { left := c, right := b, bottom := u, top := v }.coveredSquares

The complementary L-shaped repartition uses the same row cut, with v between u and w, while in the column coordinate c lies between a and b.

theorem TauCeti.GridRectangle.coveredSquares_union_eq_of_mem_cIoo_common_right {n : ℕ} {a b c u v w : Fin n} (hcol : b ∈ Grid.cIoo a c) (hrow : v ∈ Grid.cIoo u w) : { left := b, right := c, bottom := v, top := w }.coveredSquares ∪ { left := a, right := c, bottom := u, top := v }.coveredSquares = { left := a, right := b, bottom := u, top := v }.coveredSquares ∪ { left := b, right := c, bottom := u, top := w }.coveredSquares

The mirror identity, for two rectangles sharing their terminal vertical side c rather than their initial one: the lower rectangle spans the columns from a to c and the upper one the columns from b to c, with b between a and c. Cutting along the column line b instead of the row line v gives the other pair.

theorem TauCeti.GridRectangle.coveredSquares_union_eq_of_mem_cIoo_common_right_complementary_col_cut {n : ℕ} {a b c u v w : Fin n} (hcol : b ∈ Grid.cIoo a c) (hrow : v ∈ Grid.cIoo u w) : { left := a, right := c, bottom := v, top := w }.coveredSquares ∪ { left := b, right := c, bottom := u, top := v }.coveredSquares = { left := b, right := c, bottom := u, top := w }.coveredSquares ∪ { left := a, right := b, bottom := v, top := w }.coveredSquares

The complementary column cut for two rectangles sharing their terminal vertical side c: here the upper rectangle is the wider one, spanning the columns from a to c, and the cut runs along the column line b of the narrower lower rectangle.