Fully blocked empty rectangles in grid diagrams

This file packages the finite rectangle counts used by the fully blocked grid differential. For grid states x and y, the already-defined GridRectangleBetween x y records an oriented toroidal rectangle from x to y. Here we filter the generic empty-rectangle enumeration to rectangles none of whose covered squares carries an O or X marking of a grid diagram.

The final count is valued in ZMod 2, matching the first coefficient system used in the grid homology roadmap.

Main definitions

• TauCeti.GridDiagram.fullyBlockedRectangles: empty rectangles avoiding all markings.
• TauCeti.GridDiagram.fullyBlockedRectangleCount: the corresponding count in ZMod 2.
• TauCeti.GridDiagram.card_fullyBlockedRectangles_le_two: at most two fully blocked rectangles contribute to each matrix coefficient.

Main results

• TauCeti.GridDiagram.fullyBlockedRectangleCount_transpose: the count is invariant under the diagonal reflection of a grid diagram and its two states.
• TauCeti.GridDiagram.fullyBlockedRectangles_swapMarkings and TauCeti.GridDiagram.fullyBlockedRectangleCount_swapMarkings: the rectangle set and its count are unchanged by swapping the O and X markings.

References

This supplies a prerequisite for the Tau Ceti Heegaard Floer roadmap, CombinatorialHeegaardFloer/README.md in TauCetiRoadmap, Lane G.3, "The complexes and ∂² = 0", where the fully blocked grid complex over 𝔽₂ counts rectangles avoiding all markings. The objects and terminology follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3; the marking-avoidance condition defining the fully blocked complex is in Chapter 4, Section 4.4.

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

The finite set of fully blocked empty rectangles from x to y in a grid diagram.

"Fully blocked" means that the rectangle is empty for the source grid state and none of the squares it covers carries an O or X marking. This is the rectangle set whose parity gives the coefficient of y in the fully blocked grid differential applied to x.

@[simp]

theorem TauCeti.GridDiagram.mem_fullyBlockedRectangles {n : ℕ} (G : GridDiagram n) (x y : GridState n) (R : GridRectangleBetween x y) : R ∈ G.fullyBlockedRectangles x y ↔ R.IsEmpty ∧ R.AvoidsMarkings G

Membership in the fully blocked rectangle set is emptiness together with marking avoidance.

theorem TauCeti.GridDiagram.isEmpty_of_mem_fullyBlockedRectangles {n : ℕ} (G : GridDiagram n) (x y : GridState n) {R : GridRectangleBetween x y} (hR : R ∈ G.fullyBlockedRectangles x y) : R.IsEmpty

Every fully blocked rectangle is empty.

theorem TauCeti.GridDiagram.avoidsMarkings_of_mem_fullyBlockedRectangles {n : ℕ} (G : GridDiagram n) (x y : GridState n) {R : GridRectangleBetween x y} (hR : R ∈ G.fullyBlockedRectangles x y) : R.AvoidsMarkings G

Every fully blocked rectangle avoids the O and X markings.

theorem TauCeti.GridDiagram.fullyBlockedRectangles_subset_emptyRectangles {n : ℕ} (G : GridDiagram n) (x y : GridState n) : G.fullyBlockedRectangles x y ⊆ GridRectangleBetween.emptyRectangles x y

Fully blocked rectangles are a subset of the empty rectangles between the same states.

theorem TauCeti.GridDiagram.card_fullyBlockedRectangles_le_two {n : ℕ} (G : GridDiagram n) (x y : GridState n) : (G.fullyBlockedRectangles x y).card ≤ 2

There are at most two fully blocked rectangles in each matrix coefficient of the fully blocked differential.

noncomputable def TauCeti.GridDiagram.fullyBlockedRectangleCount {n : ℕ} (G : GridDiagram n) (x y : GridState n) : ZMod 2

The number of fully blocked empty rectangles from x to y, reduced modulo 2.

theorem TauCeti.GridDiagram.fullyBlockedRectangleCount_def {n : ℕ} (G : GridDiagram n) (x y : GridState n) : G.fullyBlockedRectangleCount x y = ↑(G.fullyBlockedRectangles x y).card

The fully blocked rectangle count is the cardinality of fullyBlockedRectangles, coerced to ZMod 2.

theorem TauCeti.GridDiagram.exists_swapColumns_of_fullyBlockedRectangleCount_ne_zero {n : ℕ} (G : GridDiagram n) (x y : GridState n) (h : G.fullyBlockedRectangleCount x y ≠ 0) : ∃ (a : Fin n) (b : Fin n), a ≠ b ∧ y = GridState.swapColumns a b x

A nonzero fully blocked rectangle count forces the target state to be a column transposition of the source state: a nonzero count means there is a fully blocked rectangle, hence an oriented rectangle, between the two states.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedRectangles_self {n : ℕ} (G : GridDiagram n) (x : GridState n) : G.fullyBlockedRectangles x x = ∅

The set of fully blocked rectangles from a grid state to itself is empty.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedRectangleCount_self {n : ℕ} (G : GridDiagram n) (x : GridState n) : G.fullyBlockedRectangleCount x x = 0

The fully blocked rectangle count from a grid state to itself is zero.

theorem TauCeti.GridDiagram.mem_fullyBlockedRectangles_transpose {n : ℕ} (G : GridDiagram n) (x y : GridState n) (R : GridRectangleBetween x y) : R.transpose ∈ G.transpose.fullyBlockedRectangles x.transpose y.transpose ↔ R ∈ G.fullyBlockedRectangles x y

The diagonal reflection of a fully blocked rectangle is a fully blocked rectangle for the reflected diagram.

theorem TauCeti.GridDiagram.fullyBlockedRectangleCount_transpose {n : ℕ} (G : GridDiagram n) (x y : GridState n) : G.transpose.fullyBlockedRectangleCount x.transpose y.transpose = G.fullyBlockedRectangleCount x y

The fully blocked rectangle count is invariant under the diagonal reflection of a grid diagram and its two states. This is the matrix-coefficient form of the statement that the diagonal reflection is a chain symmetry of the fully blocked grid complex.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedRectangles_swapMarkings {n : ℕ} (G : GridDiagram n) (x y : GridState n) : G.swapMarkings.fullyBlockedRectangles x y = G.fullyBlockedRectangles x y

The fully blocked rectangles are unchanged by swapping the O and X markings, since marking avoidance only refers to the union of the two marking sets.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedRectangleCount_swapMarkings {n : ℕ} (G : GridDiagram n) (x y : GridState n) : G.swapMarkings.fullyBlockedRectangleCount x y = G.fullyBlockedRectangleCount x y

The fully blocked rectangle count is invariant under swapping the O and X markings.