Coefficients of the square of the fully blocked grid differential

This file expands the coefficient of ∂ (∂ x) for the fully blocked grid differential as the finite sum over intermediate grid states. It is the algebraic handoff from the matrix coefficient definition of the differential to the rectangle-pairing argument: proving ∂² = 0 on a generator is exactly proving that this sum of length-two rectangle counts vanishes.

The statements here do not assert square-zero. They isolate the coefficient formula and combine it with the two-step support bound, so that a square-zero argument can work coefficient-by-coefficient inside the finite set of states reached by two column swaps.

Main results

• TauCeti.GridDiagram.fullyBlockedDifferential_sq_single_apply: the coefficient of ∂ (∂ x) at z is ∑ y, count(x, y) * count(y, z).
• TauCeti.GridDiagram.sum_fullyBlockedRectangleCount_mul_eq_zero_of_notMem_twoStep: the same finite sum vanishes off the two-step column-swap neighbour set.
• TauCeti.GridDiagram.fullyBlockedDifferential_sq_single_eq_zero_iff: square-zero on a generator is equivalent to vanishing of all of those coefficient sums.
• TauCeti.GridDiagram.fullyBlockedDifferential_comp_self_eq_zero_iff: the global square-zero statement is equivalent to the same coefficient vanishing for every pair of states.

References

The coefficient interpretation follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedDifferential_sq_single_apply {n : ℕ} (G : GridDiagram n) (x z : GridState n) : (Finsupp.sum (G.fullyBlockedDifferentialOnGenerator x) fun (y : GridState n) (a : ZMod 2) => a * G.fullyBlockedRectangleCount y z) = ∑ y : GridState n, G.fullyBlockedRectangleCount x y * G.fullyBlockedRectangleCount y z

The coefficient of ∂ (∂ x) at z is the finite sum over all intermediate grid states y of the product of the two rectangle-count coefficients. This is the matrix multiplication formula for the fully blocked differential.

theorem TauCeti.GridDiagram.sum_fullyBlockedRectangleCount_mul_eq_zero_of_notMem_twoStep {n : ℕ} (G : GridDiagram n) (x : GridState n) {z : GridState n} (hz : z ∉ x.twoStepColumnSwapNeighbors) : ∑ y : GridState n, G.fullyBlockedRectangleCount x y * G.fullyBlockedRectangleCount y z = 0

If z is not reachable from x by two column swaps, the length-two rectangle-count sum from x to z vanishes.

theorem TauCeti.GridDiagram.fullyBlockedDifferential_sq_single_eq_zero_iff {n : ℕ} (G : GridDiagram n) (x : GridState n) : G.fullyBlockedDifferential (G.fullyBlockedDifferential (Finsupp.single x 1)) = 0 ↔ ∀ (z : GridState n), ∑ y : GridState n, G.fullyBlockedRectangleCount x y * G.fullyBlockedRectangleCount y z = 0

The square of the fully blocked differential vanishes on a generator exactly when every length-two rectangle-count coefficient sum out of that generator vanishes.

theorem TauCeti.GridDiagram.fullyBlockedDifferential_comp_self_eq_zero_iff {n : ℕ} (G : GridDiagram n) : G.fullyBlockedDifferential ∘ₗ G.fullyBlockedDifferential = 0 ↔ ∀ (x z : GridState n), ∑ y : GridState n, G.fullyBlockedRectangleCount x y * G.fullyBlockedRectangleCount y z = 0

The global square-zero statement for the fully blocked differential is equivalent to vanishing of every length-two rectangle-count coefficient sum.