The squares a toroidal rectangle covers

A toroidal grid rectangle has two different finite domains, and the grid gradings need both. Its corners are grid points, that is, intersections of grid lines, and the grid points strictly inside it are GridRectangle.interior, the product of the two open cyclic intervals: this is the domain against which a grid state is tested for emptiness. The O- and X-markings, however, sit at the centres of squares, so a marked square lies inside the rectangle exactly when its index lies in the half-open cyclic interval in each direction. That domain is GridRectangle.coveredSquares, the product of the two half-open arcs Grid.cIco left right and Grid.cIco bottom top.

When the vertical sides differ, coveredSquares includes the initial column in addition to the open column interval; when they coincide, both column sets are empty. The analogous statement holds for rows. GridRectangle.interior_subset_coveredSquares records the resulting inclusion without a nondegeneracy hypothesis.

The convention that markings sit at the centres of their squares is the one the Maslov and Alexander gradings already use (JFunction/Center.lean). GridRectangle.coveredColumns, GridRectangle.coveredRows and GridRectangle.coveredSquares are defined with the rectangles in Rectangle/Basic.lean, where the marking-avoidance predicate of the grid differential, GridRectangle.AvoidsMarkings, tests the covered squares; this file develops them for the gradings, and Grading/MarkingCount.lean uses them to turn the Maslov and Alexander grading changes across a rectangle move into marking counts.

Main results

• TauCeti.GridRectangle.interior_subset_coveredSquares: every grid point strictly inside a rectangle names a square the rectangle covers.
• TauCeti.GridRectangle.disjoint_coveredSquares_iff: two covered-square domains are disjoint exactly when their covered columns or their covered rows are disjoint.
• TauCeti.GridRectangle.card_coveredSquares: the number of covered squares is the product of the two arc lengths.
• TauCeti.GridDiagram.disjoint_coveredSquares_XSet_swapColumns_of_subinterval: X-avoidance transfers across a column swap to a rectangle whose covered columns are contained in an X-avoiding rectangle's covered columns and whose rows are contained in its rows, provided the swapped-out column is covered by the original rectangle but not by the new one.
• TauCeti.GridDiagram.X_not_mem_coveredRows_of_disjoint: the X-marking of a covered column avoids an X-avoiding rectangle's covered rows.

References

The placement of the markings at the centres of their squares, and hence the half-open shape of the domain they are counted in, follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapters 3.1--3.2 and 4.1.

theorem TauCeti.GridRectangle.columnInterior_subset_coveredColumns {n : ℕ} (R : GridRectangle n) : R.columnInterior ⊆ R.coveredColumns

Every interior column is a covered column. For distinct vertical sides the covered columns also contain the initial column; for coincident sides both sets are empty.

theorem TauCeti.GridRectangle.rowInterior_subset_coveredRows {n : ℕ} (R : GridRectangle n) : R.rowInterior ⊆ R.coveredRows

Every interior row is a covered row. For distinct horizontal sides the covered rows also contain the initial row; for coincident sides both sets are empty.

@[simp]

theorem TauCeti.GridRectangle.card_coveredColumns {n : ℕ} (R : GridRectangle n) : R.coveredColumns.card = if R.left = R.right then 0 else if ↑R.left < ↑R.right then ↑R.right - ↑R.left else n - ↑R.left + ↑R.right

The number of covered columns, expressed in the standard representatives of the sides.

@[simp]

theorem TauCeti.GridRectangle.card_coveredRows {n : ℕ} (R : GridRectangle n) : R.coveredRows.card = if R.bottom = R.top then 0 else if ↑R.bottom < ↑R.top then ↑R.top - ↑R.bottom else n - ↑R.bottom + ↑R.top

The number of covered rows, expressed in the standard representatives of the sides.

theorem TauCeti.GridRectangle.mem_coveredSquares_swap_iff_of_coveredColumns {n : ℕ} (R : GridRectangle n) {a b : Fin n} (h : a ∈ R.coveredColumns ↔ b ∈ R.coveredColumns) (p : Fin n × Fin n) : ((Equiv.swap a b) p.1, p.2) ∈ R.coveredSquares ↔ p ∈ R.coveredSquares

Swapping two columns preserves a rectangle's covered squares when the rectangle either covers both columns or covers neither.

theorem TauCeti.GridRectangle.disjoint_coveredSquares_iff {n : ℕ} (R S : GridRectangle n) : Disjoint R.coveredSquares S.coveredSquares ↔ Disjoint R.coveredColumns S.coveredColumns ∨ Disjoint R.coveredRows S.coveredRows

Two rectangles have disjoint covered-square domains exactly when their covered columns or their covered rows are disjoint.

theorem TauCeti.GridRectangle.interior_subset_coveredSquares {n : ℕ} (R : GridRectangle n) : R.interior ⊆ R.coveredSquares

Every grid point strictly inside a rectangle names a square that the rectangle covers.

@[simp]

theorem TauCeti.GridRectangle.card_coveredSquares {n : ℕ} (R : GridRectangle n) : R.coveredSquares.card = R.coveredColumns.card * R.coveredRows.card

The number of covered squares is the product of the numbers of covered columns and covered rows.

theorem TauCeti.GridDiagram.disjoint_coveredSquares_XSet_swapColumns_iff_of_coveredColumns {n : ℕ} (G : GridDiagram n) (R : GridRectangle n) {a b : Fin n} (h : a ∈ R.coveredColumns ↔ b ∈ R.coveredColumns) : Disjoint R.coveredSquares (swapColumns a b G).XSet ↔ Disjoint R.coveredSquares G.XSet

Avoidance of the X-markings is unchanged by swapping two columns of the diagram when the rectangle either covers both columns or covers neither.

theorem TauCeti.GridDiagram.disjoint_coveredSquares_XSet_swapColumns_of_subinterval {n : ℕ} (G : GridDiagram n) (R R' : GridRectangle n) {a b : Fin n} (hR'row : R'.coveredRows ⊆ R.coveredRows) (hX : Disjoint R.coveredSquares G.XSet) (ha : a ∈ R.coveredColumns) (ha_not : a ∉ R'.coveredColumns) (hsub : R'.coveredColumns ⊆ R.coveredColumns) : Disjoint R'.coveredSquares (swapColumns a b G).XSet

X-avoidance transfers across a column swap to a rectangle whose covered columns are contained in an X-avoiding rectangle's covered columns (with rows contained in the original's), provided the swapped-out column is covered by the original rectangle but not by the new one.

theorem TauCeti.GridDiagram.X_not_mem_coveredRows_of_disjoint {n : ℕ} (G : GridDiagram n) (R : GridRectangle n) {b : Fin n} (hX : Disjoint R.coveredSquares G.XSet) (hb : b ∈ R.coveredColumns) : G.X.toPerm b ∉ R.coveredRows

The X-marking of a covered column avoids an X-avoiding rectangle's covered rows: if G.X b were in the row interval, (b, G.X b) would be a covered square carrying an X-marking.

theorem TauCeti.GridRectangleBetween.pointSet_inter_coveredSquares_eq_insert {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : x.pointSet ∩ R.toGridRectangle.coveredSquares = insert (R.left, R.bottom) (x.pointSet ∩ R.toGridRectangle.interior)

The source-state points in the covered squares are its interior points together with the lower-left corner. This distinguishes occupied grid points from marking-square centers.