Grading changes across a rectangle move

This file records how the Maslov and Alexander gradings of two grid states differ, first as a pure identity between the grading formulas of any two states, then localized to the four corners of a rectangle move.

Two grading functions with the same changes across rectangles agree everywhere once they agree at one grid state, by rectangle connectivity.

The two Maslov gradings split the same way: their difference is the change in the state's J-self-pairing minus twice the change in the marking pairing, M_O(x) - M_O(y) = (J(x, x) - J(y, y)) - 2 (J_O(x) - J_O(y)), and similarly for M_X. The state-self-pairing term is identical in both Maslov gradings, so it cancels in the Alexander grading, leaving the clean marking-only identity A(x) - A(y) = (J_X(x) - J_X(y)) - (J_O(x) - J_O(y)). None of these three reductions needs any relationship between x and y.

When y is obtained from x by a rectangle move R : GridRectangleBetween x y, the two states share all but two of their occupied squares (RectangleSwap.lean), so each marking pairing J_O(x) - J_O(y) collapses to a difference of four corner JCenter-singletons: the source corners (left, bottom), (right, top) against the target corners (left, top), (right, bottom). For Maslov gradings the state self-pairing does not cancel, so this file also localizes its change to the moving corners and their pairings with the shared part of the two states. Feeding these localized formulas back into the grading reductions removes the opaque whole-state self-pairing term from the rectangle Maslov formulas, while the Alexander formula remains purely marking-local because the state self-pairing cancels there.

Main results

• TauCeti.GridDiagram.maslovO_sub_maslovO_eq, TauCeti.GridDiagram.maslovX_sub_maslovX_eq: the difference of a Maslov grading at two states splits into the state self-pairing change and twice the marking pairing change.
• TauCeti.GridDiagram.alexander_sub_alexander_eq: the Alexander grading change is the difference of the two marking pairing changes; the state self-pairing cancels.
• TauCeti.GridRectangleBetween.JCenter_pointSet_sub_eq: across a rectangle move, the change in the marking pairing of a state's points against an arbitrary fixed point set collapses to the four moving corners.
• TauCeti.GridDiagram.JO_sub_JO_eq, TauCeti.GridDiagram.JX_sub_JX_eq: across a rectangle move the marking pairing change is a difference of four corner JCenter-singletons.
• TauCeti.GridRectangleBetween.J_self_sub_J_self_eq: across a rectangle move, the state self-pairing change is localized to the moving corners and the shared state points.
• TauCeti.GridDiagram.alexander_change_rectangle, TauCeti.GridDiagram.maslovO_change_rectangle, TauCeti.GridDiagram.maslovX_change_rectangle: the grading changes across a rectangle move, localized to the four corners.

References

This supplies the rectangle grading-change part of 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." The formulas follow the J-function bookkeeping in Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapters 3 and 4.

theorem TauCeti.GridRectangleBetween.J_self_sub_J_self_eq {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) : x.J x - y.J y = 2 * (GridPoint.J {(R.left, R.bottom)} {(R.right, R.top)} + GridPoint.J {(R.left, R.bottom)} (x.pointSet ∩ y.pointSet) + GridPoint.J {(R.right, R.top)} (x.pointSet ∩ y.pointSet) - (GridPoint.J {(R.left, R.top)} {(R.right, R.bottom)} + GridPoint.J {(R.left, R.top)} (x.pointSet ∩ y.pointSet) + GridPoint.J {(R.right, R.bottom)} (x.pointSet ∩ y.pointSet)))

Across a rectangle move, the change in the state self-pairing is localized to the four moving corners and their pairings with the shared part of the two states. This removes the opaque GridState.J x x - GridState.J y y term from the Maslov grading-change formulas.

theorem TauCeti.GridRectangleBetween.JCenter_pointSet_sub_eq {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (P : Finset (Fin n × Fin n)) : GridPoint.JCenter x.pointSet P - GridPoint.JCenter y.pointSet P = GridPoint.JCenter {(R.left, R.bottom)} P + GridPoint.JCenter {(R.right, R.top)} P - (GridPoint.JCenter {(R.left, R.top)} P + GridPoint.JCenter {(R.right, R.bottom)} P)

Across a rectangle move, the change in the pairing of a state's points against an arbitrary fixed point set P collapses to the four moving corners: the source corners (left, bottom), (right, top) against the target corners (left, top), (right, bottom). The shared part of the two states cancels. The marking-pairing localizations specialize this at the O- and X-marking sets.

theorem TauCeti.GridState.eq_of_forall_sub_eq {n : ℕ} {A : Type u_1} [AddGroup A] {f g : GridState n → A} (x₀ : GridState n) (h₀ : f x₀ = g x₀) (h : ∀ (x y : GridState n) (a : GridRectangleBetween x y), f x - f y = g x - g y) (x : GridState n) : f x = g x

Two grading functions that change in the same way across every rectangle, and agree at one grid state, agree everywhere.

theorem TauCeti.GridDiagram.maslovO_sub_maslovO_eq {n : ℕ} (G : GridDiagram n) (x y : GridState n) : G.maslovO x - G.maslovO y = x.J x - y.J y - 2 * (G.JO x - G.JO y)

The difference of the O-Maslov grading at two grid states splits into the change in the state self-pairing and twice the change in the O-marking pairing. The two states need not be related: this is the algebraic shape of the grading formula.

theorem TauCeti.GridDiagram.maslovX_sub_maslovX_eq {n : ℕ} (G : GridDiagram n) (x y : GridState n) : G.maslovX x - G.maslovX y = x.J x - y.J y - 2 * (G.JX x - G.JX y)

The difference of the X-Maslov grading at two grid states splits into the change in the state self-pairing and twice the change in the X-marking pairing.

theorem TauCeti.GridDiagram.alexander_sub_alexander_eq {n : ℕ} (G : GridDiagram n) (x y : GridState n) : G.alexander x - G.alexander y = G.JX x - G.JX y - (G.JO x - G.JO y)

The Alexander grading change at two grid states is the difference of the two marking pairing changes. The state self-pairing term is common to both Maslov gradings and the normalization shift depends only on the grid size, so both cancel, leaving a marking-only identity that needs no relationship between x and y.

theorem TauCeti.GridDiagram.JO_sub_JO_eq {n : ℕ} (G : GridDiagram n) {x y : GridState n} (R : GridRectangleBetween x y) : G.JO x - G.JO y = GridPoint.JCenter {(R.left, R.bottom)} G.OSet + GridPoint.JCenter {(R.right, R.top)} G.OSet - (GridPoint.JCenter {(R.left, R.top)} G.OSet + GridPoint.JCenter {(R.right, R.bottom)} G.OSet)

Across a rectangle move the O-marking pairing change collapses to the four corners: the source corners (left, bottom), (right, top) against the target corners (left, top), (right, bottom). The two states share all but their corners, and the shared part cancels.

theorem TauCeti.GridDiagram.JX_sub_JX_eq {n : ℕ} (G : GridDiagram n) {x y : GridState n} (R : GridRectangleBetween x y) : G.JX x - G.JX y = GridPoint.JCenter {(R.left, R.bottom)} G.XSet + GridPoint.JCenter {(R.right, R.top)} G.XSet - (GridPoint.JCenter {(R.left, R.top)} G.XSet + GridPoint.JCenter {(R.right, R.bottom)} G.XSet)

Across a rectangle move the X-marking pairing change collapses to the four corners.

theorem TauCeti.GridDiagram.alexander_change_rectangle {n : ℕ} (G : GridDiagram n) {x y : GridState n} (R : GridRectangleBetween x y) : G.alexander x - G.alexander y = GridPoint.JCenter {(R.left, R.bottom)} G.XSet + GridPoint.JCenter {(R.right, R.top)} G.XSet - (GridPoint.JCenter {(R.left, R.top)} G.XSet + GridPoint.JCenter {(R.right, R.bottom)} G.XSet) - (GridPoint.JCenter {(R.left, R.bottom)} G.OSet + GridPoint.JCenter {(R.right, R.top)} G.OSet - (GridPoint.JCenter {(R.left, R.top)} G.OSet + GridPoint.JCenter {(R.right, R.bottom)} G.OSet))

The Alexander grading change across a rectangle move, localized to the four corners: it is the four X-corner pairings minus the four O-corner pairings, in each case the two source corners against the two target corners. The state self-pairing cancels (alexander_sub_alexander_eq) and the shared squares cancel (JX_sub_JX_eq, JO_sub_JO_eq).

theorem TauCeti.GridDiagram.maslovO_change_rectangle {n : ℕ} (G : GridDiagram n) {x y : GridState n} (R : GridRectangleBetween x y) : G.maslovO x - G.maslovO y = 2 * (GridPoint.J {(R.left, R.bottom)} {(R.right, R.top)} + GridPoint.J {(R.left, R.bottom)} (x.pointSet ∩ y.pointSet) + GridPoint.J {(R.right, R.top)} (x.pointSet ∩ y.pointSet) - (GridPoint.J {(R.left, R.top)} {(R.right, R.bottom)} + GridPoint.J {(R.left, R.top)} (x.pointSet ∩ y.pointSet) + GridPoint.J {(R.right, R.bottom)} (x.pointSet ∩ y.pointSet))) - 2 * (GridPoint.JCenter {(R.left, R.bottom)} G.OSet + GridPoint.JCenter {(R.right, R.top)} G.OSet - (GridPoint.JCenter {(R.left, R.top)} G.OSet + GridPoint.JCenter {(R.right, R.bottom)} G.OSet))

The O-Maslov grading change across a rectangle move, with both the state self-pairing change and the O-marking pairing change localized to the rectangle corners.

theorem TauCeti.GridDiagram.maslovX_change_rectangle {n : ℕ} (G : GridDiagram n) {x y : GridState n} (R : GridRectangleBetween x y) : G.maslovX x - G.maslovX y = 2 * (GridPoint.J {(R.left, R.bottom)} {(R.right, R.top)} + GridPoint.J {(R.left, R.bottom)} (x.pointSet ∩ y.pointSet) + GridPoint.J {(R.right, R.top)} (x.pointSet ∩ y.pointSet) - (GridPoint.J {(R.left, R.top)} {(R.right, R.bottom)} + GridPoint.J {(R.left, R.top)} (x.pointSet ∩ y.pointSet) + GridPoint.J {(R.right, R.bottom)} (x.pointSet ∩ y.pointSet))) - 2 * (GridPoint.JCenter {(R.left, R.bottom)} G.XSet + GridPoint.JCenter {(R.right, R.top)} G.XSet - (GridPoint.JCenter {(R.left, R.top)} G.XSet + GridPoint.JCenter {(R.right, R.bottom)} G.XSet))

The X-Maslov grading change across a rectangle move, with both the state self-pairing change and the X-marking pairing change localized to the rectangle corners.