Backtracking in the two-step grid differential support

The support of the square of the fully blocked grid differential is already bounded by GridState.twoStepColumnSwapNeighbors: states reached from x by two nontrivial column transpositions. This file records the first exact feature of that two-step support. A path that swaps the same pair of columns twice returns to the starting state, so the source state appears in its own two-step neighbour set exactly when the grid has at least two columns.

This is small but useful bookkeeping for the ∂² = 0 rectangle-pairing argument: diagonal targets lie in the two-step search space exactly through such backtracking when 2 ≤ n. Grids of size 0 and 1 have no two-step targets at all, so any coefficient-level vanishing there follows from the small-grid differential support API rather than from a cancellation argument in this file.

Main results

• TauCeti.GridState.self_mem_twoStepColumnSwapNeighbors_of_ne: swapping a pair of distinct columns and then swapping it back puts x in its own two-step neighbour set.
• TauCeti.GridState.sym2_mk_eq_of_swapColumns_swapColumns_eq_self: any diagonal two-step witness swaps the same unordered pair of columns twice.
• TauCeti.GridState.self_mem_twoStepColumnSwapNeighbors_iff_exists_pair_ne: this is possible exactly when there is a distinct pair of columns.
• TauCeti.GridState.self_mem_twoStepColumnSwapNeighbors_iff_two_le: equivalently, exactly when 2 ≤ n.

References

The column-transposition model of rectangle targets follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapters 3 and 4.

theorem TauCeti.GridState.self_mem_twoStepColumnSwapNeighbors_of_ne {n : ℕ} (x : GridState n) {a b : Fin n} (hab : a ≠ b) : x ∈ x.twoStepColumnSwapNeighbors

Swapping a distinct pair of columns and then swapping the same pair back puts the source state in its own two-step column-swap neighbour set.

theorem TauCeti.GridState.sym2_mk_eq_of_swapColumns_swapColumns_eq_self {n : ℕ} (x : GridState n) {a b c d : Fin n} (hab : a ≠ b) (h : swapColumns c d (swapColumns a b x) = x) : s(a, b) = s(c, d)

A diagonal two-step column-swap witness whose first swap is nontrivial swaps the same unordered pair of columns twice.

theorem TauCeti.GridState.swapColumns_swapColumns_eq_self_iff_sym2_mk_eq {n : ℕ} (x : GridState n) {a b c d : Fin n} (hab : a ≠ b) : swapColumns c d (swapColumns a b x) = x ↔ s(a, b) = s(c, d)

A nontrivial column swap followed by a second column swap is a diagonal two-step witness exactly when the two use the same unordered pair of columns.

theorem TauCeti.GridState.self_mem_twoStepColumnSwapNeighbors_iff_exists_pair_ne {n : ℕ} (x : GridState n) : x ∈ x.twoStepColumnSwapNeighbors ↔ ∃ (a : Fin n) (b : Fin n), a ≠ b

The source state appears in its own two-step neighbour set exactly when there is a distinct pair of grid columns.

theorem TauCeti.GridState.self_mem_twoStepColumnSwapNeighbors_of_two_le {n : ℕ} (x : GridState n) (hn : 2 ≤ n) : x ∈ x.twoStepColumnSwapNeighbors

If the grid has at least two columns, the source state is a two-step neighbour of itself.

@[simp]

theorem TauCeti.GridState.self_mem_twoStepColumnSwapNeighbors_iff_two_le {n : ℕ} (x : GridState n) : x ∈ x.twoStepColumnSwapNeighbors ↔ 2 ≤ n

The source state is a two-step neighbour of itself exactly in grid size at least two.