Cardinality bounds for the fully blocked grid differential support

The fully blocked grid differential is already known to be supported on the column-swap neighbours of a grid state. This file makes that computability statement quantitative: those neighbours are the image of Mathlib's off-diagonal finite set of ordered distinct column pairs. The two orders of the same column swap give the same target state, so Mathlib's Sym2.card_image_offDiag turns this into the n.choose 2 bound for possible targets.

The same estimate extends to arbitrary finitely supported chains by taking the finite union of the neighbour sets attached to the input support. These bounds are the finite-row bookkeeping needed before the ∂² = 0 rectangle-pairing proof and before evaluating the fully blocked complex on small explicit grids.

Main results

• TauCeti.GridDiagram.fullyBlockedDifferentialOnGenerator_support_card_le_choose: the same bound for the support of a differential row.
• TauCeti.GridDiagram.fullyBlockedDifferential_support_subset_biUnion and TauCeti.GridDiagram.fullyBlockedDifferential_support_card_le: support and cardinality bounds for the differential of an arbitrary chain.

References

This supplies a prerequisite for TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.3, "The complexes and ∂² = 0", and for the roadmap's standing requirement that the grid differential compute on explicit small grids. The column-transposition support condition follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapters 3 and 4.

theorem TauCeti.GridDiagram.fullyBlockedDifferentialOnGenerator_support_card_le_choose {n : ℕ} (G : GridDiagram n) (x : GridState n) : (G.fullyBlockedDifferentialOnGenerator x).support.card ≤ n.choose 2

The support of the fully blocked differential of one generator has at most n.choose 2 states. This is the quantitative form of the column-transposition support theorem.

theorem TauCeti.GridDiagram.fullyBlockedDifferentialOnGenerator_support_eq_empty_of_le_one {n : ℕ} (G : GridDiagram n) (hn : n ≤ 1) (x : GridState n) : (G.fullyBlockedDifferentialOnGenerator x).support = ∅

The support of the fully blocked differential of one generator is empty in grid size at most 1.

theorem TauCeti.GridDiagram.fullyBlockedDifferentialOnGenerator_support_eq_empty_of_zero (G : GridDiagram 0) (x : GridState 0) : (G.fullyBlockedDifferentialOnGenerator x).support = ∅

The support of the fully blocked differential of one generator is empty in grid size 0.

theorem TauCeti.GridDiagram.fullyBlockedDifferentialOnGenerator_eq_zero_of_le_one {n : ℕ} (G : GridDiagram n) (hn : n ≤ 1) (x : GridState n) : G.fullyBlockedDifferentialOnGenerator x = 0

The fully blocked differential of a generator is zero in grid size at most 1.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedDifferentialOnGenerator_eq_zero_of_zero (G : GridDiagram 0) (x : GridState 0) : G.fullyBlockedDifferentialOnGenerator x = 0

The fully blocked differential of a generator is zero in grid size 0.

theorem TauCeti.GridDiagram.fullyBlockedDifferential_support_subset_biUnion {n : ℕ} (G : GridDiagram n) (c : GridChain (ZMod 2) n) : (G.fullyBlockedDifferential c).support ⊆ c.support.biUnion fun (x : GridState n) => x.columnSwapNeighbors

The support of the fully blocked differential of a chain is contained in the union of the column-swap neighbour sets of the states appearing in the input chain.

theorem TauCeti.GridDiagram.fullyBlockedDifferential_apply_eq_zero_of_notMem_support_biUnion {n : ℕ} (G : GridDiagram n) (c : GridChain (ZMod 2) n) {y : GridState n} (h : y ∉ c.support.biUnion fun (x : GridState n) => x.columnSwapNeighbors) : (G.fullyBlockedDifferential c) y = 0

A coefficient of the fully blocked differential vanishes if its target is not in the union of column-swap neighbours of the input support.

theorem TauCeti.GridDiagram.fullyBlockedDifferential_support_card_le {n : ℕ} (G : GridDiagram n) (c : GridChain (ZMod 2) n) : (G.fullyBlockedDifferential c).support.card ≤ c.support.card * n.choose 2

The support of the fully blocked differential of an arbitrary chain has cardinality at most the size of the input support times n.choose 2.

theorem TauCeti.GridDiagram.fullyBlockedDifferential_eq_zero_of_le_one {n : ℕ} (G : GridDiagram n) (hn : n ≤ 1) : G.fullyBlockedDifferential = 0

The fully blocked differential is zero on every chain in grid size at most 1.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedDifferential_eq_zero_of_zero (G : GridDiagram 0) : G.fullyBlockedDifferential = 0

The fully blocked differential is zero on every chain in grid size 0.