Removing same-side pentagon pairs from the commutation homotopy equation

Off the diagonal, a counted pair of forward and reverse pentagons turning on the same side recuts to a unique unpaired hexagon composite of the same weight. Distinct pentagon pairs have distinct recuts. Consequently their total contribution equals that of their exact recut image, and both families can be removed from the homotopy coefficient equation.

The partner family below is precisely this image, not all unpaired composites. The remaining coefficient equation compares its complement with the mixed-side pentagon pairs. No converse classification of unpaired composites is assumed.

References

Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.1, and Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Section 3.1, Proposition 3.2 (arXiv:math/0610559). The geometric input is the weighted recut matching in Homotopy.TerminalPair and Homotopy.InitialPair.Weight.

noncomputable def TauCeti.GridDiagram.sameSidePentagonPairs {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (x z : GridState n) : Finset (GridPentagonPairDecomposition C.column C.turnRow C.reverse.column C.reverse.turnRow x z)

The counted forward--reverse pentagon pairs whose turns lie on the same side of the replaced grid line. This includes both terminal--terminal and initial--initial pairs.

@[simp]

theorem TauCeti.GridDiagram.mem_sameSidePentagonPairs {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} (D : GridPentagonPairDecomposition C.column C.turnRow C.reverse.column C.reverse.turnRow x z) : D ∈ G.sameSidePentagonPairs C x z ↔ D ∈ G.pentagonPairDecompositions C x z ∧ Sum.isLeft D.first = Sum.isLeft D.second

A same-side pair is counted and has equal turn-side indicators.

theorem TauCeti.GridDiagram.sameSidePentagonPairs_subset {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (x z : GridState n) : G.sameSidePentagonPairs C x z ⊆ G.pentagonPairDecompositions C x z

Every same-side pair is a term of the full round-trip coefficient sum.

noncomputable def TauCeti.GridDiagram.sameSidePentagonPartners {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (x z : GridState n) : Finset (GridHexagonCompositeDecomposition C.column C.turnRow C.oppositeTurnRow x z)

The unpaired hexagon composites obtained by recutting counted same-side pentagon pairs. This is their exact recut image, without a claim that it exhausts the unpaired composites.

@[simp]

theorem TauCeti.GridDiagram.mem_sameSidePentagonPartners {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} (F : GridHexagonCompositeDecomposition C.column C.turnRow C.oppositeTurnRow x z) : F ∈ G.sameSidePentagonPartners C x z ↔ F ∈ G.unpairedHexagonComposites C x z ∧ ∃ D ∈ G.sameSidePentagonPairs C x z, D.toRectangleDecomposition.IsRecut F.toRectangleDecomposition

Partners are exactly the unpaired composites recutting a counted same-side pair.

theorem TauCeti.GridDiagram.sameSidePentagonPartners_subset {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (x z : GridState n) : G.sameSidePentagonPartners C x z ⊆ G.unpairedHexagonComposites C x z

Every partner belongs to the unpaired-composite coefficient sum.

theorem TauCeti.GridDiagram.sum_pentagonPairWeight_sameSide_eq_sum_partners {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x z : GridState n} (hzx : z ≠ x) : ∑ D ∈ G.sameSidePentagonPairs C x z, G.pentagonPairWeight C R D = ∑ F ∈ G.sameSidePentagonPartners C x z, G.hexagonCompositeWeight C R F

Off the diagonal, the same-side pentagon pairs and their exact hexagon-composite recut image have equal total polynomial weight over every commutative semiring.

theorem TauCeti.GridDiagram.sum_unpaired_eq_sum_pentagonPairs_iff_sdiff_sameSide {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] [IsCancelAdd R] {x z : GridState n} (hzx : z ≠ x) : ∑ F ∈ G.unpairedHexagonComposites C x z, G.hexagonCompositeWeight C R F = ∑ D ∈ G.pentagonPairDecompositions C x z, G.pentagonPairWeight C R D ↔ ∑ F ∈ G.unpairedHexagonComposites C x z \ G.sameSidePentagonPartners C x z, G.hexagonCompositeWeight C R F = ∑ D ∈ G.pentagonPairDecompositions C x z \ G.sameSidePentagonPairs C x z, G.pentagonPairWeight C R D

The off-diagonal homotopy coefficient equation holds exactly when the remaining unpaired composites and mixed-side pentagon pairs have equal total weight.

theorem TauCeti.GridDiagram.unblockedDifferential_commutationHomotopy_add_eq_iff_sdiff_sameSide {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] [CharP R 2] : (∀ (c : GridChainMinus R n), (G.unblockedDifferential R) ((G.commutationHomotopy R C) c) + (G.commutationHomotopy R C) ((G.unblockedDifferential R) c) = c + ((swapColumns C.column ((finRotate n) C.column) G).commutationMap R C.reverse.toColumnTurn) ((G.commutationMap R C.toColumnTurn) c)) ↔ ∀ (x z : GridState n), z ≠ x → ∑ F ∈ G.unpairedHexagonComposites C x z \ G.sameSidePentagonPartners C x z, G.hexagonCompositeWeight C R F = ∑ D ∈ G.pentagonPairDecompositions C x z \ G.sameSidePentagonPairs C x z, G.pentagonPairWeight C R D

In characteristic two, the full commutation homotopy equation reduces to the complement of the same-side recut image off the diagonal. The diagonal returning annuli and the matched same-side pairs have already been discharged.