Integer-valuedness of the Maslov gradings

The Maslov gradings M_O and M_X of a grid state are defined in TauCeti.KnotTheory.Grid.Gradings as rational-valued formulas through the J-function, which is itself a half-integer (the symmetrization of a point-pair count divided by two). This file proves that the two Maslov gradings are in fact integers, by exhibiting explicit integer formulas and the corresponding rational casts. As an immediate consequence the Alexander grading is a half-integer: its double is an integer.

The key elementary fact is that the J-function on a point set with itself is already an integer, J(s, s) = I(s, s), because the symmetrized numerator JNum(s, s) = 2 · I(s, s) is even. Feeding this into the formula M_O(x) = J(x, x) - 2 · J_O(x) + J(O, O) + 1 cancels every remaining half: 2 · J_O(x) = JNumCenter(x, O) is an integer, and the two self-pairings are integers, so M_O(x) is an integer. The same computation handles M_X.

Main definitions

• TauCeti.GridDiagram.maslovOℤ, TauCeti.GridDiagram.maslovXℤ: the integer-valued Maslov gradings.
• TauCeti.GridDiagram.alexanderTwoℤ: the integer numerator of twice the Alexander grading.

Main results

• TauCeti.GridDiagram.maslovO_eq_intCast, TauCeti.GridDiagram.maslovX_eq_intCast: the rational Maslov gradings are the casts of their integer counterparts.
• TauCeti.GridDiagram.maslovO_exists_int, TauCeti.GridDiagram.maslovX_exists_int: the Maslov gradings are integers.
• TauCeti.GridDiagram.two_mul_alexander_eq_intCast, TauCeti.GridDiagram.two_mul_alexander_exists_int: twice the Alexander grading is an integer.
• TauCeti.GridDiagram.maslovOℤ_transpose, TauCeti.GridDiagram.maslovXℤ_transpose, TauCeti.GridDiagram.alexanderTwoℤ_transpose: the integer-valued gradings are invariant under the diagonal reflection of a grid state and diagram.
• TauCeti.GridDiagram.maslovOℤ_swapMarkings, TauCeti.GridDiagram.maslovXℤ_swapMarkings, TauCeti.GridDiagram.alexanderTwoℤ_swapMarkings: the integer-valued gradings transform under the marking swap.
• TauCeti.GridDiagram.maslovOℤ_eq_card, TauCeti.GridDiagram.maslovXℤ_eq_card: the integer Maslov gradings written entirely as counts over column indices, so they evaluate on an explicit grid without unfolding any point-pair product.
• TauCeti.GridDiagram.maslovOℤ_O, TauCeti.GridDiagram.maslovXℤ_X: the integer Maslov grading of a marking state against its own markings is always 1 - n.

References

This advances TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G item 2, "Gradings. The J-function, M_O, M_X, A; integer-valuedness of A; grading-change formulas across a rectangle." The integrality of the Maslov gradings is the prerequisite that the (parity-sensitive) integrality of the Alexander grading itself builds on; see Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.

def TauCeti.GridDiagram.maslovOℤ {n : ℕ} (G : GridDiagram n) (x : GridState n) : ℤ

The integer-valued O-Maslov grading of a grid state.

This is the integer formula M_O(x) = I(x, x) - JNumCenter(x, O) + I(O, O) + 1 obtained from the rational definition once the two halves coming from the J-function cancel.

@[simp]

theorem TauCeti.GridDiagram.maslovOℤ_def {n : ℕ} (G : GridDiagram n) (x : GridState n) : G.maslovOℤ x = ↑(GridPoint.I x.pointSet x.pointSet) - ↑(GridPoint.JNumCenter x.pointSet G.OSet) + ↑(GridPoint.I G.OSet G.OSet) + 1

The integer O-Maslov grading restated as its defining formula.

def TauCeti.GridDiagram.maslovXℤ {n : ℕ} (G : GridDiagram n) (x : GridState n) : ℤ

The integer-valued X-Maslov grading of a grid state.

@[simp]

theorem TauCeti.GridDiagram.maslovXℤ_def {n : ℕ} (G : GridDiagram n) (x : GridState n) : G.maslovXℤ x = ↑(GridPoint.I x.pointSet x.pointSet) - ↑(GridPoint.JNumCenter x.pointSet G.XSet) + ↑(GridPoint.I G.XSet G.XSet) + 1

The integer X-Maslov grading restated as its defining formula.

theorem TauCeti.GridDiagram.maslovOℤ_eq_card {n : ℕ} (G : GridDiagram n) (x : GridState n) : G.maslovOℤ x = ↑{p : Fin n × Fin n | p.1 < p.2 ∧ x.toPerm p.1 < x.toPerm p.2}.card - (↑{p : Fin n × Fin n | p.1 ≤ p.2 ∧ x.toPerm p.1 ≤ G.O.toPerm p.2}.card + ↑{p : Fin n × Fin n | p.1 < p.2 ∧ G.O.toPerm p.1 < x.toPerm p.2}.card) + ↑{p : Fin n × Fin n | p.1 < p.2 ∧ G.O.toPerm p.1 < G.O.toPerm p.2}.card + 1

The integer O-Maslov grading of a grid state written entirely as counts over column indices. The state and marking self-counts are strict southwest counts, while the first directed state-to-marking count is the weak southwest-of-centre comparison. All collapse to column-pair counts, so the grading evaluates without unfolding any point-pair product.

theorem TauCeti.GridDiagram.maslovXℤ_eq_card {n : ℕ} (G : GridDiagram n) (x : GridState n) : G.maslovXℤ x = ↑{p : Fin n × Fin n | p.1 < p.2 ∧ x.toPerm p.1 < x.toPerm p.2}.card - (↑{p : Fin n × Fin n | p.1 ≤ p.2 ∧ x.toPerm p.1 ≤ G.X.toPerm p.2}.card + ↑{p : Fin n × Fin n | p.1 < p.2 ∧ G.X.toPerm p.1 < x.toPerm p.2}.card) + ↑{p : Fin n × Fin n | p.1 < p.2 ∧ G.X.toPerm p.1 < G.X.toPerm p.2}.card + 1

The integer X-Maslov grading of a grid state written entirely as counts over column indices, with the state-to-marking term using the weak southwest-of-centre comparison.

theorem TauCeti.GridDiagram.maslovOℤ_O {n : ℕ} (G : GridDiagram n) : G.maslovOℤ G.O = 1 - ↑n

The integer O-Maslov grading of the O-marking state is always 1 - n: pairing the O-marking state against the squares that hold the O markings adds the n diagonal pairs that the strict southwest count misses.

theorem TauCeti.GridDiagram.maslovXℤ_X {n : ℕ} (G : GridDiagram n) : G.maslovXℤ G.X = 1 - ↑n

The integer X-Maslov grading of the X-marking state is always 1 - n.

theorem TauCeti.GridDiagram.maslovO_eq_intCast {n : ℕ} (G : GridDiagram n) (x : GridState n) : G.maslovO x = ↑(G.maslovOℤ x)

The rational O-Maslov grading equals the cast of its integer counterpart. In particular, the doubled asymmetric marking pairing has the integer numerator JNumCenter(x, 𝕆).

theorem TauCeti.GridDiagram.maslovX_eq_intCast {n : ℕ} (G : GridDiagram n) (x : GridState n) : G.maslovX x = ↑(G.maslovXℤ x)

The rational X-Maslov grading equals the cast of its integer counterpart. In particular, the doubled asymmetric marking pairing has the integer numerator JNumCenter(x, 𝕏).

theorem TauCeti.GridDiagram.maslovO_exists_int {n : ℕ} (G : GridDiagram n) (x : GridState n) : ∃ (m : ℤ), G.maslovO x = ↑m

The O-Maslov grading is an integer.

theorem TauCeti.GridDiagram.maslovX_exists_int {n : ℕ} (G : GridDiagram n) (x : GridState n) : ∃ (m : ℤ), G.maslovX x = ↑m

The X-Maslov grading is an integer.

def TauCeti.GridDiagram.alexanderTwoℤ {n : ℕ} (G : GridDiagram n) (x : GridState n) : ℤ

The integer numerator of twice the Alexander grading, 2 · A(x) = M_O(x) - M_X(x) - (n - 1). The normalization shift (n - 1) is taken over ℤ, so the formula is literal at every n.

@[simp]

theorem TauCeti.GridDiagram.alexanderTwoℤ_def {n : ℕ} (G : GridDiagram n) (x : GridState n) : G.alexanderTwoℤ x = G.maslovOℤ x - G.maslovXℤ x - (↑n - 1)

The integer numerator of twice the Alexander grading restated as its defining formula.

theorem TauCeti.GridDiagram.two_mul_alexander_eq_intCast {n : ℕ} (G : GridDiagram n) (x : GridState n) : 2 * G.alexander x = ↑(G.alexanderTwoℤ x)

Twice the Alexander grading is an integer: it is the difference of the integer Maslov gradings, corrected by the normalization shift. This stops short of integrality of A itself, which is the genuinely parity-sensitive statement.

theorem TauCeti.GridDiagram.two_mul_alexander_exists_int {n : ℕ} (G : GridDiagram n) (x : GridState n) : ∃ (m : ℤ), 2 * G.alexander x = ↑m

Twice the Alexander grading is an integer; equivalently, the Alexander grading is a half-integer.

theorem TauCeti.GridDiagram.maslovOℤ_transpose {n : ℕ} (G : GridDiagram n) (x : GridState n) : G.transpose.maslovOℤ x.transpose = G.maslovOℤ x

The integer-valued O-Maslov grading is invariant under the diagonal reflection.

theorem TauCeti.GridDiagram.maslovXℤ_transpose {n : ℕ} (G : GridDiagram n) (x : GridState n) : G.transpose.maslovXℤ x.transpose = G.maslovXℤ x

The integer-valued X-Maslov grading is invariant under the diagonal reflection.

theorem TauCeti.GridDiagram.alexanderTwoℤ_transpose {n : ℕ} (G : GridDiagram n) (x : GridState n) : G.transpose.alexanderTwoℤ x.transpose = G.alexanderTwoℤ x

The integer numerator of twice the Alexander grading is invariant under the diagonal reflection.

@[simp]

theorem TauCeti.GridDiagram.maslovOℤ_swapMarkings {n : ℕ} (G : GridDiagram n) (x : GridState n) : G.swapMarkings.maslovOℤ x = G.maslovXℤ x

The marking swap exchanges the integer-valued Maslov gradings.

@[simp]

theorem TauCeti.GridDiagram.maslovXℤ_swapMarkings {n : ℕ} (G : GridDiagram n) (x : GridState n) : G.swapMarkings.maslovXℤ x = G.maslovOℤ x

The marking swap exchanges the integer-valued Maslov gradings.

theorem TauCeti.GridDiagram.alexanderTwoℤ_swapMarkings {n : ℕ} (G : GridDiagram n) (x : GridState n) : G.swapMarkings.alexanderTwoℤ x = -G.alexanderTwoℤ x - 2 * (↑n - 1)

The marking swap negates the integer numerator of twice the Alexander grading, up to twice the normalization shift: 2·A_swap(x) = −2·A(x) − 2(n − 1).