The grading changes across a rectangle are marking counts

Grading/Change.lean localizes the grading changes across a rectangle move to the four corners of the rectangle: each change is an alternating combination of the pairings of the two source corners and the two target corners against the marking sets, plus, for the Maslov gradings, the pairings of those corners against each other and against the squares the two states share. This file evaluates all of those combinations and so puts the grading changes in the closed form the rest of the theory uses,

A(x) - A(y) = #(𝕏 ∩ r) - #(𝕆 ∩ r) for every rectangle, and M_O(x) - M_O(y) = 2 #(x ∩ r) - 1 - 2 #(𝕆 ∩ r) for every rectangle. For an empty rectangle the latter specializes to M_O(x) - M_O(y) = 1 - 2 #(𝕆 ∩ r),

where r is the set of squares the rectangle covers (GridRectangle.coveredSquares).

The evaluation is pointwise in the marking. Writing u, v, s, t for the indicators of the four comparisons left ≤ c, right ≤ c, bottom ≤ r, top ≤ r of a marked square (c, r), the four corner terms contribute 2 (u - v) (s - t) to twice the alternating combination, an identity of polynomials in four variables. The factor u - v is the indicator of the covered columns when the rectangle does not wrap around the torus horizontally, and that indicator minus one when it does; likewise for s - t and the covered rows. Summing over a marking set therefore produces the count of markings inside the rectangle, corrected by terms proportional to the number of covered columns, the number of covered rows and the grid size. Those corrections are the same for 𝕆 and for 𝕏, because each marking set meets every column and every row exactly once, so they cancel in the Alexander grading and the wrapping of the rectangle leaves no trace.

The same evaluation, applied to the two J-terms that the Maslov grading change carries in addition, gives the general Maslov formula above. For an empty rectangle, the rectangle covers only one occupied square of its source state, its own lower-left corner, yielding the familiar constant 1. Here the wrapping corrections do not cancel between two marking sets; instead they cancel against the corner pairings and the shared squares.

Together the two formulas give bidegree (-1, 0) when an empty rectangle's GridRectangle.coveredSquares are disjoint from the markings, which is the marking-avoidance predicate GridRectangle.AvoidsMarkings of the grid differential. Two further consequences are recorded: the Alexander grading changes by an integer across any rectangle move, even though the grading itself is a priori only rational, and a square-disjoint rectangle preserves it outright.

Main results

• TauCeti.GridDiagram.alexander_sub_alexander_eq_card_sub_card: the Alexander grading change across a rectangle move is the number of X-markings in the squares the rectangle covers minus the number of O-markings there.
• TauCeti.GridDiagram.maslovO_sub_maslovO_eq_two_mul_card_sub_one_sub_two_mul_card, TauCeti.GridDiagram.maslovX_sub_maslovX_eq_two_mul_card_sub_one_sub_two_mul_card: the Maslov grading changes across any rectangle move in terms of the covered source-state squares and corresponding marking count.
• TauCeti.GridDiagram.maslovO_sub_maslovO_eq_one_sub_two_mul_card, TauCeti.GridDiagram.maslovX_sub_maslovX_eq_one_sub_two_mul_card: the Maslov grading changes across an empty rectangle move are one minus twice the corresponding marking count.
• TauCeti.GridDiagram.alexander_eq_alexander_of_disjoint_coveredSquares, TauCeti.GridDiagram.maslovO_sub_maslovO_eq_one_of_disjoint_coveredSquares, TauCeti.GridDiagram.maslovX_sub_maslovX_eq_one_of_disjoint_coveredSquares: a square-disjoint empty rectangle move preserves the Alexander grading and drops either Maslov grading by one.
• TauCeti.GridDiagram.exists_int_alexander_sub_alexander: the Alexander gradings of two grid states joined by a rectangle differ by an integer.
• TauCeti.GridRectangleBetween.JWeight_sub_JWeight_eq_sum: the pairing GridState.JWeight against an integer weight on the squares whose rows and columns sum to zero changes across a rectangle by the total weight of the covered squares.

References

This supplies TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.2, "Gradings. The J-function, M_O, M_X, A; integer-valuedness of A; grading-change formulas across a rectangle", in the closed form Lanes G.3 and G.4 consume. The formulas are Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.3, where the grading changes across a rectangle r from x to y are A(x) - A(y) = #(r ∩ 𝕏) - #(r ∩ 𝕆) and, for an empty rectangle, M_O(x) - M_O(y) = 1 - 2 #(r ∩ 𝕆).

theorem TauCeti.GridDiagram.alexander_sub_alexander_eq_card_sub_card {n : ℕ} (G : GridDiagram n) {x y : GridState n} (R : GridRectangleBetween x y) : G.alexander x - G.alexander y = ↑(G.XSet ∩ R.toGridRectangle.coveredSquares).card - ↑(G.OSet ∩ R.toGridRectangle.coveredSquares).card

The Alexander grading change across a rectangle move is the number of X-markings in the squares the rectangle covers minus the number of O-markings there.

This is the closed form of GridDiagram.alexander_change_rectangle: the corner pairings evaluate to marking counts, and the corrections recording how the rectangle wraps around the torus are the same for the two marking sets, so they cancel.

theorem TauCeti.GridDiagram.maslovO_sub_maslovO_eq_two_mul_card_sub_one_sub_two_mul_card {n : ℕ} (G : GridDiagram n) {x y : GridState n} (R : GridRectangleBetween x y) : G.maslovO x - G.maslovO y = 2 * ↑(x.pointSet ∩ R.toGridRectangle.coveredSquares).card - 1 - 2 * ↑(G.OSet ∩ R.toGridRectangle.coveredSquares).card

The O-Maslov grading change across any rectangle move is twice the number of covered source-state squares, minus one, minus twice the number of covered O-markings.

theorem TauCeti.GridDiagram.maslovX_sub_maslovX_eq_two_mul_card_sub_one_sub_two_mul_card {n : ℕ} (G : GridDiagram n) {x y : GridState n} (R : GridRectangleBetween x y) : G.maslovX x - G.maslovX y = 2 * ↑(x.pointSet ∩ R.toGridRectangle.coveredSquares).card - 1 - 2 * ↑(G.XSet ∩ R.toGridRectangle.coveredSquares).card

The X-Maslov grading change across any rectangle move is twice the number of covered source-state squares, minus one, minus twice the number of covered X-markings.

theorem TauCeti.GridDiagram.maslovO_sub_maslovO_eq_one_sub_two_mul_card {n : ℕ} (G : GridDiagram n) {x y : GridState n} (R : GridRectangleBetween x y) (hR : R.IsEmpty) : G.maslovO x - G.maslovO y = 1 - 2 * ↑(G.OSet ∩ R.toGridRectangle.coveredSquares).card

The O-Maslov grading change across an empty rectangle move is one minus twice the number of O-markings in the squares the rectangle covers.

Unlike the Alexander formula, this one needs the rectangle to be empty: the source state's occupied squares inside the rectangle would otherwise contribute.

theorem TauCeti.GridDiagram.maslovX_sub_maslovX_eq_one_sub_two_mul_card {n : ℕ} (G : GridDiagram n) {x y : GridState n} (R : GridRectangleBetween x y) (hR : R.IsEmpty) : G.maslovX x - G.maslovX y = 1 - 2 * ↑(G.XSet ∩ R.toGridRectangle.coveredSquares).card

The X-Maslov grading change across an empty rectangle move is one minus twice the number of X-markings in the squares the rectangle covers.

theorem TauCeti.GridDiagram.maslovO_sub_maslovO_eq_one_of_disjoint_coveredSquares {n : ℕ} (G : GridDiagram n) {x y : GridState n} (R : GridRectangleBetween x y) (hR : R.IsEmpty) (h : Disjoint R.toGridRectangle.coveredSquares G.OSet) : G.maslovO x - G.maslovO y = 1

An empty rectangle move whose squares carry no O-marking drops the O-Maslov grading by exactly one. A rectangle satisfying GridRectangle.AvoidsMarkings meets the hypothesis (GridRectangle.disjoint_coveredSquares_OSet_of_avoidsMarkings). Together with GridDiagram.alexander_eq_alexander_of_disjoint_coveredSquares, this gives the Maslov part of bidegree (-1, 0).

theorem TauCeti.GridDiagram.maslovX_sub_maslovX_eq_one_of_disjoint_coveredSquares {n : ℕ} (G : GridDiagram n) {x y : GridState n} (R : GridRectangleBetween x y) (hR : R.IsEmpty) (h : Disjoint R.toGridRectangle.coveredSquares G.XSet) : G.maslovX x - G.maslovX y = 1

An empty rectangle move whose covered squares carry no X-marking drops the X-Maslov grading by exactly one. A rectangle satisfying GridRectangle.AvoidsMarkings meets the hypothesis (GridRectangle.disjoint_coveredSquares_XSet_of_avoidsMarkings).

theorem TauCeti.GridDiagram.alexander_eq_alexander_of_disjoint_coveredSquares {n : ℕ} (G : GridDiagram n) {x y : GridState n} (R : GridRectangleBetween x y) (h : Disjoint R.toGridRectangle.coveredSquares (G.OSet ∪ G.XSet)) : G.alexander x = G.alexander y

A rectangle move whose covered squares carry no marking preserves the Alexander grading. The hypothesis is GridRectangle.AvoidsMarkings for the underlying toroidal rectangle.

theorem TauCeti.GridDiagram.exists_int_alexander_sub_alexander {n : ℕ} (G : GridDiagram n) {x y : GridState n} (R : GridRectangleBetween x y) : ∃ (m : ℤ), G.alexander x - G.alexander y = ↑m

The Alexander gradings of two grid states joined by a rectangle differ by an integer, even though the Alexander grading is a priori only rational.

Pairing against a weight on the squares

noncomputable def TauCeti.GridState.JWeight {n : ℕ} (w : Fin n × Fin n → ℤ) (x : GridState n) : ℚ

The pairing of a grid state against an integer weight w on the squares of the grid: the sum, over the squares q, of w q times the pairing GridPoint.JCenter of the state with the single square q. It extends the pairing against a set of marked squares to integer weights.

theorem TauCeti.GridState.JWeight_def {n : ℕ} (w : Fin n × Fin n → ℤ) (x : GridState n) : JWeight w x = ∑ q : Fin n × Fin n, ↑(w q) * GridPoint.JCenter x.pointSet {q}

The weighted pairing as a sum over squares.

theorem TauCeti.GridRectangleBetween.JWeight_sub_JWeight_eq_sum {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) {w : Fin n × Fin n → ℤ} (hcol : ∀ (c : Fin n), ∑ r : Fin n, w (c, r) = 0) (hrow : ∀ (r : Fin n), ∑ c : Fin n, w (c, r) = 0) : GridState.JWeight w x - GridState.JWeight w y = ∑ q ∈ R.toGridRectangle.coveredSquares, ↑(w q)

The pairing against a balanced weight changes by the covered weight. If an integer weight on the squares sums to zero along every column and every row, its pairing with the source of a rectangle minus its pairing with the target is the total weight of the squares the rectangle covers. The wrapping corrections of the four-corner evaluation are proportional to the column and row sums of the weight, so they vanish.