Rectangles in grid diagrams

The grid lives on a torus, so the basic one-dimensional ingredient of a rectangle is the circular interval in Fin n. A grid rectangle carries two finite coordinate sets built from such intervals: its interior, the product of two open intervals, records the grid points strictly inside and is what a grid state must avoid for the rectangle to be empty; its coveredSquares, the product of two half-open intervals, records the region the rectangle covers and is what must avoid the O and X markings.

The final section packages an oriented rectangle from one grid state to another: two columns where the states exchange rows, and agreement everywhere else. This is the shape counted by the grid differential; the IsEmptyFor and AvoidsMarkings predicates record the two finite-set disjointness conditions used for empty rectangles and marking-avoiding rectangles.

AvoidsMarkings tests coveredSquares, so a marking counts as covered exactly when its square lies under the rectangle: marking indices are the southwest corners of square-centred markings, the convention the Maslov and Alexander gradings use. Rectangle/Squares.lean develops the covered squares further for the gradings.

Main definitions

• TauCeti.GridRectangle: a toroidal rectangle, represented by its four cyclic sides.
• TauCeti.GridRectangle.transpose: the diagonal reflection of a toroidal rectangle, exchanging the column and row sides.
• TauCeti.GridRectangle.interior: the finite set of grid points strictly inside the rectangle.
• TauCeti.GridRectangle.coveredSquares: the finite set of squares the rectangle covers, each named by its lower-left grid point.
• TauCeti.GridRectangle.IsEmptyFor: a toroidal rectangle is empty for a grid state when no point of the state lies in its interior.
• TauCeti.GridRectangle.AvoidsMarkings: a toroidal rectangle avoids a grid diagram's markings when no O or X marking lies in a square it covers.
• TauCeti.GridRectangleBetween: an oriented rectangle from one grid state to another.
• TauCeti.GridRectangleBetween.toGridRectangle: the toroidal rectangle of an oriented rectangle, with the same side columns and with the source-state rows in those columns as its horizontal sides.
• TauCeti.GridRectangleBetween.IsEmpty: an oriented rectangle is empty when its toroidal rectangle is empty for the source state.
• TauCeti.GridRectangleBetween.swapSides: the other oriented rectangle from x to y on the same two side columns, which runs along the complementary column arc and the complementary row arc.
• TauCeti.GridRectangleBetween.transpose: the diagonal reflection of an oriented rectangle, from x.transpose to y.transpose.
• TauCeti.GridRectangleBetween.transposeEquiv: the diagonal reflection packaged as an involutive equivalence with oriented rectangles from x.transpose to y.transpose.
• TauCeti.GridRectangleBetween.emptyRectangles: the empty rectangles from x to y.

Main results

• TauCeti.GridRectangle.isEmptyFor_iff_forall_notMem_cIoo: emptiness of a toroidal rectangle for a grid state, quantified over the columns strictly inside it, and TauCeti.GridRectangleBetween.isEmpty_iff_forall_notMem_cIoo, its form for an oriented rectangle and its source state, with TauCeti.GridRectangleBetween.isEmpty_iff_forall_notMem_cIoo_target the same test read through the target state.
• TauCeti.GridRectangleBetween.isEmpty_of_right_eq_finRotate: a rectangle one column wide is empty.
• TauCeti.GridRectangle.avoidsMarkings_iff_forall: marking avoidance tested column by column.

References

The encoding follows the toroidal grid-diagram convention from Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3. Rectangles connecting two grid states, Rect(x, y), and the empty ones among them, Rect°(x, y) (Definition 4.2.1), are in Chapter 4, Section 4.2; the marking-avoidance condition defining the fully blocked complex is in Section 4.4.

structure TauCeti.GridRectangle (n : ℕ) : Type

A toroidal grid rectangle, represented by its oriented column and row sides.

The interior is the product of the clockwise open interval from left to right with the clockwise open interval from bottom to top. Degenerate side choices are allowed at this level; their interiors are empty in the degenerate direction.

• left : Fin n

  The initial vertical side of the rectangle.

• right : Fin n

  The terminal vertical side of the rectangle.

• bottom : Fin n

  The initial horizontal side of the rectangle.

• top : Fin n

  The terminal horizontal side of the rectangle.

theorem TauCeti.GridRectangle.ext_iff {n : ℕ} {x y : GridRectangle n} : x = y ↔ x.left = y.left ∧ x.right = y.right ∧ x.bottom = y.bottom ∧ x.top = y.top

theorem TauCeti.GridRectangle.ext {n : ℕ} {x y : GridRectangle n} (left : x.left = y.left) (right : x.right = y.right) (bottom : x.bottom = y.bottom) (top : x.top = y.top) : x = y

noncomputable def TauCeti.GridRectangle.columnInterior {n : ℕ} (R : GridRectangle n) : Finset (Fin n)

The columns strictly inside a toroidal grid rectangle.

noncomputable def TauCeti.GridRectangle.rowInterior {n : ℕ} (R : GridRectangle n) : Finset (Fin n)

The rows strictly inside a toroidal grid rectangle.

@[simp]

theorem TauCeti.GridRectangle.mem_columnInterior {n : ℕ} (R : GridRectangle n) (c : Fin n) : c ∈ R.columnInterior ↔ c ∈ Grid.cIoo R.left R.right

Membership in the interior columns is membership in the corresponding open-open circular interval.

@[simp]

theorem TauCeti.GridRectangle.mem_rowInterior {n : ℕ} (R : GridRectangle n) (r : Fin n) : r ∈ R.rowInterior ↔ r ∈ Grid.cIoo R.bottom R.top

Membership in the interior rows is membership in the corresponding open-open circular interval.

theorem TauCeti.GridRectangle.left_notMem_columnInterior {n : ℕ} (R : GridRectangle n) : R.left ∉ R.columnInterior

The left side is not an interior column.

theorem TauCeti.GridRectangle.right_notMem_columnInterior {n : ℕ} (R : GridRectangle n) : R.right ∉ R.columnInterior

The right side is not an interior column.

theorem TauCeti.GridRectangle.bottom_notMem_rowInterior {n : ℕ} (R : GridRectangle n) : R.bottom ∉ R.rowInterior

The bottom side is not an interior row.

theorem TauCeti.GridRectangle.top_notMem_rowInterior {n : ℕ} (R : GridRectangle n) : R.top ∉ R.rowInterior

The top side is not an interior row.

noncomputable def TauCeti.GridRectangle.interior {n : ℕ} (R : GridRectangle n) : Finset (Fin n × Fin n)

The finite set of grid points strictly inside a toroidal grid rectangle.

@[simp]

theorem TauCeti.GridRectangle.mem_interior {n : ℕ} (R : GridRectangle n) (p : Fin n × Fin n) : p ∈ R.interior ↔ p.1 ∈ R.columnInterior ∧ p.2 ∈ R.rowInterior

Membership in a rectangle interior is membership in both one-dimensional open intervals.

theorem TauCeti.GridRectangle.notMem_interior_of_fst_eq_left {n : ℕ} (R : GridRectangle n) {p : Fin n × Fin n} (hp : p.1 = R.left) : p ∉ R.interior

A point on the initial side column is not in the interior.

theorem TauCeti.GridRectangle.notMem_interior_of_fst_eq_right {n : ℕ} (R : GridRectangle n) {p : Fin n × Fin n} (hp : p.1 = R.right) : p ∉ R.interior

A point on the terminal side column is not in the interior.

@[simp]

theorem TauCeti.GridRectangle.interior_eq_empty_of_left_eq_right {n : ℕ} (R : GridRectangle n) (h : R.left = R.right) : R.interior = ∅

A rectangle has empty interior if its two column sides coincide.

@[simp]

theorem TauCeti.GridRectangle.interior_eq_empty_of_bottom_eq_top {n : ℕ} (R : GridRectangle n) (h : R.bottom = R.top) : R.interior = ∅

A rectangle has empty interior if its two row sides coincide.

@[simp]

theorem TauCeti.GridRectangle.card_interior {n : ℕ} (R : GridRectangle n) : R.interior.card = R.columnInterior.card * R.rowInterior.card

The number of interior grid points is the product of the numbers of interior columns and interior rows.

theorem TauCeti.GridRectangle.interior_eq_empty_of_le_two {n : ℕ} (hn : n ≤ 2) (R : GridRectangle n) : R.interior = ∅

In a grid of size at most two, every toroidal rectangle has empty interior.

noncomputable def TauCeti.GridRectangle.coveredColumns {n : ℕ} (R : GridRectangle n) : Finset (Fin n)

The columns of squares a toroidal grid rectangle covers: the clockwise half-open arc from the initial vertical side to the terminal one. For distinct sides this is the initial side together with the strictly interior columns, each column of squares named by its initial grid line; for coincident sides it is empty.

theorem TauCeti.GridRectangle.coveredColumns_def {n : ℕ} (R : GridRectangle n) : R.coveredColumns = Grid.cIco R.left R.right

The covered columns are the half-open cyclic interval between the vertical sides.

noncomputable def TauCeti.GridRectangle.coveredRows {n : ℕ} (R : GridRectangle n) : Finset (Fin n)

The rows of squares a toroidal grid rectangle covers: the clockwise half-open arc from the initial horizontal side to the terminal one. For distinct sides this is the initial side together with the strictly interior rows, each row of squares named by its initial grid line; for coincident sides it is empty.

theorem TauCeti.GridRectangle.coveredRows_def {n : ℕ} (R : GridRectangle n) : R.coveredRows = Grid.cIco R.bottom R.top

The covered rows are the half-open cyclic interval between the horizontal sides.

@[simp]

theorem TauCeti.GridRectangle.mem_coveredColumns {n : ℕ} (R : GridRectangle n) (c : Fin n) : c ∈ R.coveredColumns ↔ c ∈ Grid.cIco R.left R.right

Membership in the covered columns is membership in the corresponding half-open circular interval.

@[simp]

theorem TauCeti.GridRectangle.mem_coveredRows {n : ℕ} (R : GridRectangle n) (r : Fin n) : r ∈ R.coveredRows ↔ r ∈ Grid.cIco R.bottom R.top

Membership in the covered rows is membership in the corresponding half-open circular interval.

noncomputable def TauCeti.GridRectangle.coveredSquares {n : ℕ} (R : GridRectangle n) : Finset (Fin n × Fin n)

The finite set of squares a toroidal grid rectangle covers, each square named by its lower-left grid point, following the marking-coordinate convention documented with GridDiagram.OSet and GridDiagram.XSet.

Where interior records the grid points strictly inside the rectangle — what a grid state must avoid for the rectangle to be empty — coveredSquares records the region the rectangle covers, which is what contains or avoids the O and X markings placed in the squares of a grid diagram: a marking sits at the centre of its square, so it lies inside the rectangle exactly when its column and row indices lie in the two half-open arcs. If either pair of sides coincides, the covered set is empty.

theorem TauCeti.GridRectangle.coveredSquares_def {n : ℕ} (R : GridRectangle n) : R.coveredSquares = R.coveredColumns ×ˢ R.coveredRows

The covered squares are the product of the covered columns and rows.

@[simp]

theorem TauCeti.GridRectangle.mem_coveredSquares {n : ℕ} (R : GridRectangle n) (p : Fin n × Fin n) : p ∈ R.coveredSquares ↔ p.1 ∈ R.coveredColumns ∧ p.2 ∈ R.coveredRows

Membership in the covered squares is membership in both one-dimensional half-open arcs.

def TauCeti.GridRectangle.IsEmptyFor {n : ℕ} (R : GridRectangle n) (x : GridState n) : Prop

A rectangle is empty for a grid state when the state has no point in its interior.

theorem TauCeti.GridRectangle.isEmptyFor_iff {n : ℕ} (R : GridRectangle n) (x : GridState n) : R.IsEmptyFor x ↔ ∀ p ∈ x.pointSet, p ∉ R.interior

A rectangle is empty for a grid state exactly when no point of the state lies in its interior.

theorem TauCeti.GridRectangle.isEmptyFor_iff_forall_notMem_cIoo {n : ℕ} (R : GridRectangle n) (x : GridState n) : R.IsEmptyFor x ↔ ∀ c ∈ Grid.cIoo R.left R.right, x.toPerm c ∉ Grid.cIoo R.bottom R.top

A rectangle is empty for a grid state exactly when the state sends every column strictly between its two side columns to a row outside the open arc between its two side rows.

This is the one-dimensional form of emptiness that the rectangle-pairing arguments for the grid differential use: it quantifies over columns rather than over grid points.

theorem TauCeti.GridRectangle.isEmptyFor_of_right_eq_finRotate {n : ℕ} (R : GridRectangle n) (x : GridState n) (h : R.right = (finRotate n) R.left) : R.IsEmptyFor x

A rectangle whose terminal side is the cyclic successor of its initial side is empty for every grid state: no column lies strictly between two cyclically consecutive ones.

theorem TauCeti.GridRectangle.isEmptyFor_of_le_two {n : ℕ} (hn : n ≤ 2) (R : GridRectangle n) (x : GridState n) : R.IsEmptyFor x

In a grid of size at most two, every toroidal rectangle is empty for every grid state.

theorem TauCeti.GridRectangle.isEmptyFor_of_eq_away {n : ℕ} (R : GridRectangle n) {u v : GridState n} (a b : Fin n) (ha : (a, u.toPerm a) ∉ R.interior) (hb : (b, u.toPerm b) ∉ R.interior) (haway : ∀ (p : Fin n × Fin n), p.1 ≠ a → p.1 ≠ b → p ∈ u.pointSet → p ∈ v.pointSet) (hv : R.IsEmptyFor v) : R.IsEmptyFor u

Emptiness transfers between two grid states that agree away from two columns, once the two points of the first state on those columns are known to lie outside the interior: every other point of the first state is a point of the second.

def TauCeti.GridRectangle.AvoidsMarkings {n : ℕ} (R : GridRectangle n) (G : GridDiagram n) : Prop

A rectangle avoids the markings of a grid diagram when none of the squares it covers carries an O or X marking.

theorem TauCeti.GridRectangle.disjoint_coveredSquares_OSet_of_avoidsMarkings {n : ℕ} (R : GridRectangle n) {G : GridDiagram n} (h : R.AvoidsMarkings G) : Disjoint R.coveredSquares G.OSet

A marking-avoiding rectangle covers no square carrying an O marking.

theorem TauCeti.GridRectangle.disjoint_coveredSquares_XSet_of_avoidsMarkings {n : ℕ} (R : GridRectangle n) {G : GridDiagram n} (h : R.AvoidsMarkings G) : Disjoint R.coveredSquares G.XSet

A marking-avoiding rectangle covers no square carrying an X marking.

theorem TauCeti.GridRectangle.avoidsMarkings_iff {n : ℕ} (R : GridRectangle n) (G : GridDiagram n) : R.AvoidsMarkings G ↔ Disjoint R.coveredSquares G.OSet ∧ Disjoint R.coveredSquares G.XSet

A rectangle avoids markings exactly when neither the O nor the X marking set meets the squares it covers.

theorem TauCeti.GridRectangle.avoidsMarkings_iff_forall {n : ℕ} (R : GridRectangle n) (G : GridDiagram n) : R.AvoidsMarkings G ↔ ∀ c ∈ R.coveredColumns, G.O.toPerm c ∉ R.coveredRows ∧ G.X.toPerm c ∉ R.coveredRows

A rectangle avoids markings exactly when, in each column of squares it covers, neither the O marking nor the X marking of that column lies in a covered row.

@[simp]

theorem TauCeti.GridRectangle.avoidsMarkings_swapMarkings {n : ℕ} (R : GridRectangle n) (G : GridDiagram n) : R.AvoidsMarkings G.swapMarkings ↔ R.AvoidsMarkings G

Marking avoidance is unchanged by swapping the O and X markings, since it only refers to the union of the two marking sets.

def TauCeti.GridRectangle.transpose {n : ℕ} (R : GridRectangle n) : GridRectangle n

The diagonal reflection of a toroidal rectangle, exchanging the two vertical sides with the two horizontal sides.

Reflecting across the main diagonal turns columns into rows and rows into columns, so the interior is reflected by Prod.swap.

@[simp]

theorem TauCeti.GridRectangle.transpose_left {n : ℕ} (R : GridRectangle n) : R.transpose.left = R.bottom

@[simp]

theorem TauCeti.GridRectangle.transpose_bottom {n : ℕ} (R : GridRectangle n) : R.transpose.bottom = R.left

@[simp]

theorem TauCeti.GridRectangle.transpose_top {n : ℕ} (R : GridRectangle n) : R.transpose.top = R.right

@[simp]

theorem TauCeti.GridRectangle.transpose_right {n : ℕ} (R : GridRectangle n) : R.transpose.right = R.top

@[simp]

theorem TauCeti.GridRectangle.transpose_transpose {n : ℕ} (R : GridRectangle n) : R.transpose.transpose = R

Reflecting a toroidal rectangle twice gives the original rectangle.

theorem TauCeti.GridRectangle.interior_transpose {n : ℕ} (R : GridRectangle n) : R.transpose.interior = Finset.image Prod.swap R.interior

The interior of the reflected rectangle is the diagonal reflection of the original interior.

theorem TauCeti.GridRectangle.coveredSquares_transpose {n : ℕ} (R : GridRectangle n) : R.transpose.coveredSquares = Finset.image Prod.swap R.coveredSquares

The squares covered by the reflected rectangle are the diagonal reflections of the squares covered by the original rectangle.

@[simp]

theorem TauCeti.GridRectangle.isEmptyFor_transpose {n : ℕ} (R : GridRectangle n) (x : GridState n) : R.transpose.IsEmptyFor x.transpose ↔ R.IsEmptyFor x

The diagonal reflection preserves emptiness: the reflected rectangle is empty for the reflected state exactly when the rectangle is empty for the state.

@[simp]

theorem TauCeti.GridRectangle.avoidsMarkings_transpose {n : ℕ} (R : GridRectangle n) (G : GridDiagram n) : R.transpose.AvoidsMarkings G.transpose ↔ R.AvoidsMarkings G

The diagonal reflection preserves marking avoidance: the reflected rectangle avoids the markings of the reflected diagram exactly when the rectangle avoids those of the diagram.

structure TauCeti.GridRectangleBetween {n : ℕ} (x y : GridState n) : Type

An oriented toroidal rectangle from one grid state to another.

The two states agree outside the two side columns, and in those side columns they exchange the two rows. Swapping left and right gives the other oriented rectangle from x to y on the same side columns (GridRectangleBetween.swapSides). The two side columns determine the rectangle (GridRectangleBetween.ext).

• left : Fin n

  The initial vertical side.

• right : Fin n

  The terminal vertical side.

• left_ne_right : self.left ≠ self.right

  The two side columns are distinct.

• map_left : y.toPerm self.left = x.toPerm self.right

  At the initial side, y uses the row that x uses at the terminal side.

• map_right : y.toPerm self.right = x.toPerm self.left

  At the terminal side, y uses the row that x uses at the initial side.

• map_of_ne (c : Fin n) : c ≠ self.left → c ≠ self.right → y.toPerm c = x.toPerm c

  Away from the side columns, the two states agree.

theorem TauCeti.GridRectangleBetween.ext_iff {n : ℕ} {x y : GridState n} {x✝ y✝ : GridRectangleBetween x y} : x✝ = y✝ ↔ x✝.left = y✝.left ∧ x✝.right = y✝.right

theorem TauCeti.GridRectangleBetween.ext {n : ℕ} {x y : GridState n} {x✝ y✝ : GridRectangleBetween x y} (left : x✝.left = y✝.left) (right : x✝.right = y✝.right) : x✝ = y✝

def TauCeti.GridRectangleBetween.sideColumns {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : Finset (Fin n)

The unordered finite set of side columns of an oriented grid rectangle.

@[simp]

theorem TauCeti.GridRectangleBetween.mem_sideColumns {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (c : Fin n) : c ∈ R.sideColumns ↔ c = R.left ∨ c = R.right

Membership in the side-column set of an oriented grid rectangle.

@[simp]

theorem TauCeti.GridRectangleBetween.card_sideColumns {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.sideColumns.card = 2

An oriented grid rectangle has exactly two side columns.

theorem TauCeti.GridRectangleBetween.sidePair_injective {n : ℕ} {x y : GridState n} : Function.Injective fun (R : GridRectangleBetween x y) => (R.left, R.right)

A rectangle between two grid states is determined by its two side columns.

theorem TauCeti.GridRectangleBetween.left_injective {n : ℕ} {x y : GridState n} : Function.Injective fun (R : GridRectangleBetween x y) => R.left

A rectangle between two fixed grid states is determined by its initial side column alone: the exchange condition y R.left = x R.right fixes the terminal one.

@[instance_reducible]

instance TauCeti.GridRectangleBetween.instDecidableEq {n : ℕ} {x y : GridState n} : DecidableEq (GridRectangleBetween x y)

An oriented rectangle between two grid states has decidable equality: it is determined by its ordered pair of side columns, which has decidable equality.

@[instance_reducible]

instance TauCeti.GridRectangleBetween.instFintype {n : ℕ} {x y : GridState n} : Fintype (GridRectangleBetween x y)

For fixed source and target grid states, the oriented rectangles between them form a finite type: a rectangle is its ordered pair of side columns, and the pairs that occur form a decidable subset of Fin n × Fin n. The instance is computable, so decide can count rectangles on a concrete grid.

def TauCeti.GridRectangleBetween.bottom {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : Fin n

The row of x on the initial side.

def TauCeti.GridRectangleBetween.top {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : Fin n

The row of x on the terminal side.

theorem TauCeti.GridRectangleBetween.bottom_def {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.bottom = x.toPerm R.left

The initial horizontal side is the row occupied by the source state in the initial column.

theorem TauCeti.GridRectangleBetween.top_def {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.top = x.toPerm R.right

The terminal horizontal side is the row occupied by the source state in the terminal column.

def TauCeti.GridRectangleBetween.toGridRectangle {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : GridRectangle n

The toroidal rectangle of an oriented rectangle: it has the same two side columns, and its bottom and top sides are the rows the source state occupies in the initial and terminal side columns.

@[simp]

theorem TauCeti.GridRectangleBetween.toGridRectangle_bottom {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.toGridRectangle.bottom = R.bottom

@[simp]

theorem TauCeti.GridRectangleBetween.toGridRectangle_top {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.toGridRectangle.top = R.top

@[simp]

theorem TauCeti.GridRectangleBetween.toGridRectangle_left {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.toGridRectangle.left = R.left

@[simp]

theorem TauCeti.GridRectangleBetween.toGridRectangle_right {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.toGridRectangle.right = R.right

theorem TauCeti.GridRectangleBetween.toGridRectangle_eq {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.toGridRectangle = { left := R.left, right := R.right, bottom := x.toPerm R.left, top := x.toPerm R.right }

The associated toroidal rectangle in terms of the two side columns: its two horizontal sides are the rows the source state assigns to them.

theorem TauCeti.GridRectangleBetween.mem_coveredColumns {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (c : Fin n) : c ∈ R.toGridRectangle.coveredColumns ↔ c ∈ Grid.cIco R.left R.right

Membership in the covered columns of the rectangle underlying a rectangle between states is membership in the half-open cyclic interval between its side columns.

theorem TauCeti.GridRectangleBetween.coveredColumns_subset_and_notMem_of_right_mem_cIoo {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) {a : Fin n} (hcol : R.right ∈ Grid.cIoo R.left ((finRotate n) a)) : R.toGridRectangle.coveredColumns ⊆ Grid.cIco R.left ((finRotate n) a) ∧ a ∉ R.toGridRectangle.coveredColumns ∧ (finRotate n) a ∉ R.toGridRectangle.coveredColumns

A rectangle between states whose terminal column lies strictly inside the cyclic interval from its initial column to the rotation of a covers only columns of that interval, and misses both a and its rotation.

theorem TauCeti.GridRectangleBetween.mem_toGridRectangle_interior {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) {p : Fin n × Fin n} : p ∈ R.toGridRectangle.interior ↔ p.1 ∈ Grid.cIoo R.left R.right ∧ p.2 ∈ Grid.cIoo (x.toPerm R.left) (x.toPerm R.right)

Membership in the interior of an oriented rectangle is membership in the open cyclic intervals between its side columns and the corresponding source-state rows.

theorem TauCeti.GridRectangleBetween.mem_toGridRectangle_coveredSquares {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) {p : Fin n × Fin n} : p ∈ R.toGridRectangle.coveredSquares ↔ p.1 ∈ Grid.cIco R.left R.right ∧ p.2 ∈ Grid.cIco (x.toPerm R.left) (x.toPerm R.right)

Membership in the covered squares of an oriented rectangle is membership in the half-open cyclic intervals between its side columns and the corresponding source-state rows.

theorem TauCeti.GridRectangleBetween.mem_toGridRectangle_coveredSquares_target {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) {p : Fin n × Fin n} : p ∈ R.toGridRectangle.coveredSquares ↔ p.1 ∈ Grid.cIco R.left R.right ∧ p.2 ∈ Grid.cIco (y.toPerm R.right) (y.toPerm R.left)

The covered squares of an oriented rectangle, read through its target state: the rows it covers run from the target-state row at its terminal side to the target-state row at its initial side.

theorem TauCeti.GridRectangleBetween.bottom_ne_top {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.bottom ≠ R.top

The two side rows of a rectangle between states are distinct.

theorem TauCeti.GridRectangleBetween.source_ne_target {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : x ≠ y

A rectangle between grid states has distinct source and target states. A self-rectangle would force the source state's permutation to take the same value on the two distinct side columns.

instance TauCeti.GridRectangleBetween.instIsEmpty {n : ℕ} (x : GridState n) : IsEmpty (GridRectangleBetween x x)

There are no rectangles from a grid state to itself.

theorem TauCeti.GridRectangleBetween.left_bottom_mem_source {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : (R.left, R.bottom) ∈ x.pointSet

The initial lower corner is a point of the source state.

theorem TauCeti.GridRectangleBetween.left_bottom_mem_coveredSquares {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : (R.left, R.bottom) ∈ R.toGridRectangle.coveredSquares

The associated rectangle covers its initial lower square.

theorem TauCeti.GridRectangleBetween.right_top_mem_source {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : (R.right, R.top) ∈ x.pointSet

The terminal upper corner is a point of the source state.

theorem TauCeti.GridRectangleBetween.left_top_mem_target {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : (R.left, R.top) ∈ y.pointSet

The initial upper corner is a point of the target state.

theorem TauCeti.GridRectangleBetween.right_bottom_mem_target {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : (R.right, R.bottom) ∈ y.pointSet

The terminal lower corner is a point of the target state.

theorem TauCeti.GridRectangleBetween.mem_target_pointSet_iff_of_ne {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) {p : Fin n × Fin n} (hleft : p.1 ≠ R.left) (hright : p.1 ≠ R.right) : p ∈ y.pointSet ↔ p ∈ x.pointSet

Away from the two side columns, membership in the source and target states is identical.

def TauCeti.GridRectangleBetween.IsEmpty {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : Prop

The associated rectangle is empty for the source state when no source-state point lies in its interior.

theorem TauCeti.GridRectangleBetween.isEmpty_iff_toGridRectangle_isEmptyFor {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.IsEmpty ↔ R.toGridRectangle.IsEmptyFor x

Emptiness of an oriented rectangle is emptiness of its underlying toroidal rectangle for the source state.

noncomputable def TauCeti.GridRectangleBetween.emptyRectangles {n : ℕ} (x y : GridState n) : Finset (GridRectangleBetween x y)

The finite set of empty oriented rectangles from x to y.

@[simp]

theorem TauCeti.GridRectangleBetween.mem_emptyRectangles {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R ∈ emptyRectangles x y ↔ R.IsEmpty

Membership in the finite set of empty rectangles is exactly the emptiness predicate.

theorem TauCeti.GridRectangleBetween.isEmpty_of_le_two {n : ℕ} {x y : GridState n} (hn : n ≤ 2) (R : GridRectangleBetween x y) : R.IsEmpty

In grid size at most two, every oriented rectangle between grid states is empty.

theorem TauCeti.GridRectangleBetween.emptyRectangles_eq_univ_of_le_two {n : ℕ} (hn : n ≤ 2) (x y : GridState n) : emptyRectangles x y = Finset.univ

In grid size at most two, the empty rectangles are all oriented rectangles.

@[simp]

theorem TauCeti.GridRectangleBetween.emptyRectangles_self {n : ℕ} (x : GridState n) : emptyRectangles x x = ∅

There are no empty rectangles from a grid state to itself.

theorem TauCeti.GridRectangleBetween.notMem_interior_of_isEmpty {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (h : R.IsEmpty) {p : Fin n × Fin n} (hp : p ∈ x.pointSet) : p ∉ R.toGridRectangle.interior

The source state has no point in the interior of an empty rectangle between states.

theorem TauCeti.GridRectangleBetween.isEmpty_iff {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.IsEmpty ↔ ∀ p ∈ x.pointSet, p ∉ R.toGridRectangle.interior

A rectangle between states is empty exactly when no source-state point lies in its interior.

theorem TauCeti.GridRectangleBetween.isEmpty_iff_forall_notMem_cIoo {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.IsEmpty ↔ ∀ c ∈ Grid.cIoo R.left R.right, x.toPerm c ∉ Grid.cIoo R.bottom R.top

A rectangle between states is empty exactly when the source state sends every column strictly between its two side columns to a row outside the open arc between its two side rows.

This is the one-dimensional form of emptiness that the rectangle-pairing arguments for the grid differential use: it quantifies over columns rather than over grid points.

theorem TauCeti.GridRectangleBetween.isEmpty_of_right_eq_finRotate {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (h : R.right = (finRotate n) R.left) : R.IsEmpty

A rectangle between states whose terminal side is the cyclic successor of its initial side is empty: no column lies strictly between two cyclically consecutive ones.

theorem TauCeti.GridRectangleBetween.isEmpty_iff_target {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.IsEmpty ↔ ∀ p ∈ y.pointSet, p ∉ R.toGridRectangle.interior

A rectangle between states is empty exactly when no target-state point lies in its interior.

theorem TauCeti.GridRectangleBetween.notMem_interior_target_of_isEmpty {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (h : R.IsEmpty) {p : Fin n × Fin n} (hp : p ∈ y.pointSet) : p ∉ R.toGridRectangle.interior

The target state has no point in the interior of an empty rectangle between states.

theorem TauCeti.GridRectangleBetween.isEmpty_iff_forall_notMem_cIoo_target {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.IsEmpty ↔ ∀ c ∈ Grid.cIoo R.left R.right, y.toPerm c ∉ Grid.cIoo (y.toPerm R.right) (y.toPerm R.left)

A rectangle between states is empty exactly when the target state sends every column strictly between its two side columns to a row outside the open arc between its two side rows, read through the target state: from its row at the terminal side to its row at the initial side.

This is isEmpty_iff_forall_notMem_cIoo for rectangles into a distinguished target state.

def TauCeti.GridRectangleBetween.AvoidsMarkings {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (G : GridDiagram n) : Prop

The associated rectangle avoids a grid diagram's markings when none of the squares it covers carries a marking.

theorem TauCeti.GridRectangleBetween.avoidsMarkings_iff {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (G : GridDiagram n) : R.AvoidsMarkings G ↔ Disjoint R.toGridRectangle.coveredSquares G.OSet ∧ Disjoint R.toGridRectangle.coveredSquares G.XSet

A rectangle between states avoids markings exactly when neither marking set meets the squares it covers.

theorem TauCeti.GridRectangleBetween.disjoint_coveredSquares_OSet_of_avoidsMarkings {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) {G : GridDiagram n} (h : R.AvoidsMarkings G) : Disjoint R.toGridRectangle.coveredSquares G.OSet

A marking-avoiding rectangle between states covers no square carrying an O marking.

theorem TauCeti.GridRectangleBetween.disjoint_coveredSquares_XSet_of_avoidsMarkings {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) {G : GridDiagram n} (h : R.AvoidsMarkings G) : Disjoint R.toGridRectangle.coveredSquares G.XSet

A marking-avoiding rectangle between states covers no square carrying an X marking.

def TauCeti.GridRectangleBetween.transpose {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : GridRectangleBetween x.transpose y.transpose

The diagonal reflection of an oriented rectangle from x to y, an oriented rectangle from x.transpose to y.transpose.

Reflecting across the main diagonal exchanges the side columns with the side rows: the new side columns are the two rows x R.left and x R.right that R connects.

@[simp]

theorem TauCeti.GridRectangleBetween.transpose_left {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.transpose.left = R.bottom

@[simp]

theorem TauCeti.GridRectangleBetween.transpose_right {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.transpose.right = R.top

@[simp]

theorem TauCeti.GridRectangleBetween.transpose_bottom {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.transpose.bottom = R.left

The reflected rectangle's initial side row is the original initial side column.

@[simp]

theorem TauCeti.GridRectangleBetween.transpose_top {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.transpose.top = R.right

The reflected rectangle's terminal side row is the original terminal side column.

@[simp]

theorem TauCeti.GridRectangleBetween.transpose_toGridRectangle {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.transpose.toGridRectangle = R.toGridRectangle.transpose

The associated toroidal rectangle of the reflected oriented rectangle is the reflection of the associated toroidal rectangle.

def TauCeti.GridRectangleBetween.swapSides {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : GridRectangleBetween x y

The oriented rectangle from x to y obtained by exchanging the two side columns.

It connects the same two states x and y -- the two states still exchange rows at the two side columns and agree elsewhere -- but runs along the complementary column arc and the complementary row arc. Cutting the torus along the two side columns and the two side rows, R and R.swapSides are diagonally opposite pieces; the other two pieces lie in neither. This is not the opposite rectangle symm, which runs from y back to x.

@[simp]

theorem TauCeti.GridRectangleBetween.swapSides_left {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.swapSides.left = R.right

The side-swapped rectangle's initial side column is the original terminal side column.

@[simp]

theorem TauCeti.GridRectangleBetween.swapSides_right {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.swapSides.right = R.left

The side-swapped rectangle's terminal side column is the original initial side column.

@[simp]

theorem TauCeti.GridRectangleBetween.swapSides_bottom {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.swapSides.bottom = R.top

The side-swapped rectangle's bottom row is the original top row.

@[simp]

theorem TauCeti.GridRectangleBetween.swapSides_top {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.swapSides.top = R.bottom

The side-swapped rectangle's top row is the original bottom row.

@[simp]

theorem TauCeti.GridRectangleBetween.swapSides_toGridRectangle {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.swapSides.toGridRectangle = { left := R.right, right := R.left, bottom := R.top, top := R.bottom }

The toroidal rectangle of the side-swapped oriented rectangle, written out by its four sides.

@[simp]

theorem TauCeti.GridRectangleBetween.swapSides_swapSides {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.swapSides.swapSides = R

Exchanging the two side columns twice gives the original rectangle.

theorem TauCeti.GridRectangleBetween.swapSides_ne_self {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.swapSides ≠ R

Exchanging the two side columns gives a genuinely different rectangle, since the two side columns are distinct.

@[simp]

theorem TauCeti.GridRectangleBetween.transpose_transpose {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.transpose.transpose = R

Reflecting an oriented rectangle twice gives the original rectangle.

def TauCeti.GridRectangleBetween.transposeEquiv {n : ℕ} (x y : GridState n) : GridRectangleBetween x y ≃ GridRectangleBetween x.transpose y.transpose

The diagonal reflection as an equivalence between oriented rectangles from x to y and oriented rectangles from x.transpose to y.transpose. Since reflecting twice is the identity, transpose is its own inverse.

@[simp]

theorem TauCeti.GridRectangleBetween.transposeEquiv_apply {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : (transposeEquiv x y) R = R.transpose

The transpose equivalence applies a rectangle by reflecting it.

@[simp]

theorem TauCeti.GridRectangleBetween.transposeEquiv_symm_apply {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x.transpose y.transpose) : (transposeEquiv x y).symm R = R.transpose

The inverse of the transpose equivalence is again reflection.

theorem TauCeti.GridRectangleBetween.transpose_injective {n : ℕ} {x y : GridState n} : Function.Injective transpose

The diagonal reflection is injective on oriented rectangles.

@[simp]

theorem TauCeti.GridRectangleBetween.transpose_inj {n : ℕ} {x y : GridState n} {R S : GridRectangleBetween x y} : R.transpose = S.transpose ↔ R = S

Two oriented rectangles have equal diagonal reflections exactly when they are equal.

@[simp]

theorem TauCeti.GridRectangleBetween.isEmpty_transpose {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : R.transpose.IsEmpty ↔ R.IsEmpty

The diagonal reflection preserves emptiness of a rectangle between grid states.

@[simp]

theorem TauCeti.GridRectangleBetween.avoidsMarkings_transpose {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (G : GridDiagram n) : R.transpose.AvoidsMarkings G.transpose ↔ R.AvoidsMarkings G

The diagonal reflection preserves marking avoidance of a rectangle between grid states: the reflected rectangle avoids the markings of the reflected diagram exactly when the rectangle avoids those of the diagram.

@[simp]

theorem TauCeti.GridRectangleBetween.avoidsMarkings_swapMarkings {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (G : GridDiagram n) : R.AvoidsMarkings G.swapMarkings ↔ R.AvoidsMarkings G

Swapping the O and X markings preserves marking avoidance of a rectangle between grid states.