The recut pairing on two-step grid rectangle decompositions #
A nondiagonal term in the square of the unblocked grid differential ∂⁻ is a pair of composable
empty rectangles whose two pairs of side columns are disjoint or share exactly one column. In the
second case the two rectangles meet at a corner, their union is an L-shaped hexagon, and cutting
that hexagon the other way gives a second such pair through a different intermediate grid state.
The four orientations of the common column are constructed in Recut/Initial.lean,
Recut/Terminal.lean and Recut/Mixed.lean, each as the unique decomposition carrying the side
data computed there. This file assembles those four constructions into a single involution, the
pairing that cancels the one-common-side terms of ∂⁻ ∘ ∂⁻ in characteristic two.
GridRectangleDecomposition.IsRecut collects the four side-data alternatives into one relation.
A decomposition has at most one orientation of its common column, so exactly one alternative can
hold and the relation has a unique solution. Recutting twice returns the original decomposition:
a common initial or terminal column recuts to a mixed common column and conversely, and in each of
the eight resulting configurations the original decomposition satisfies precisely the side data
that describes the recut of the recut. On the decompositions by two empty rectangles sharing
exactly one side column -- the only ones for which a recut is constructed -- the relation is
therefore symmetric, and uniqueness turns it into an involution GridRectangleDecomposition.recut
of that set. It has no fixed point, since the intermediate state changes, and it preserves the
covered-square domain, hence every weight computed from the squares a two-step term covers: the
monomial V^{O(r₁)} · V^{O(r₂)} that the square of the differential attaches to it, and which
markings the domain carries.
The pairing is stated for empty rectangles, with no condition on the markings they cover: any
condition on the markings in the covered domain, such as the avoidance of X-markings that
∂⁻ ∘ ∂⁻ requires, is transported separately along GridRectangleDecomposition.IsRepartition.
The geometric input is the cyclic order forced by emptiness of both rectangles: for a common initial or terminal column the corner row of the common side lies strictly between the other two corner rows, and for a mixed common column the terminal side of the first rectangle lies strictly between the other two side columns. That one order fact decides which of the two alternatives of the recut's own side data holds.
Main definitions #
TauCeti.GridRectangleDecomposition.IsRecutOfLeftEqLeft,TauCeti.GridRectangleDecomposition.IsRecutOfRightEqRight,TauCeti.GridRectangleDecomposition.IsRecutOfLeftEqRightandTauCeti.GridRectangleDecomposition.IsRecutOfRightEqLeft: the side data computed for the recut in each of the four orientations of the common side column.TauCeti.GridRectangleDecomposition.IsRecut: a second two-step decomposition repartitioning the same domain into empty rectangles, through a different intermediate state, with the side data of the matching orientation.TauCeti.GridRectangleDecomposition.recut: the recut of a decomposition sharing exactly one side column.
Main results #
TauCeti.GridRectangleDecomposition.existsUnique_isRecut: a decomposition by two empty rectangles sharing exactly one side column has exactly one recut.TauCeti.GridRectangleDecomposition.IsRecut.symm: such a decomposition is a recut of its own recut.TauCeti.GridRectangleDecomposition.recut_recut: recutting is an involution.TauCeti.GridRectangleDecomposition.recut_ne: it has no fixed point.TauCeti.GridRectangleDecomposition.hasOneCommonSide_recut: the recut again shares exactly one side column, so the involution stays inside the one-common-side terms.TauCeti.GridRectangleDecomposition.sideColumns_union_recut: recutting preserves the three columns used by the composite domain.TauCeti.GridRectangleDecomposition.IsRecutOfLeftEqLeft.first_left_notMem_commonSideColumnsandTauCeti.GridRectangleDecomposition.IsRecutOfRightEqRight.first_right_notMem_commonSideColumns: the recut of a decomposition with a common initial or terminal column does not keep that column as a common side.TauCeti.GridRectangleDecomposition.isRecutOfLeftEqLeft_recutand its three siblings: the recut is classified by the orientation of the original decomposition's common side.TauCeti.GridRectangleDecomposition.recut_sides_of_left_eq_left_of_mem_cIooandrecut_first_bottom_top_of_left_eq_left_of_mem_cIoo: the sides and the first recut rectangle's rows of a common-initial-side recut whose second rectangle ends inside the first's column interval.TauCeti.GridRectangleDecomposition.recut_geometry_of_right_eq_right_of_mem_cIooandrecut_geometry_of_right_eq_right_of_second_left_mem_cIoo: the sides and rows of a common-terminal-side recut, in the two orders of the initial sides.- The
side_eq,recut_sidesandrecut_branchtheorems on each orientation predicate, together withTauCeti.GridRectangleDecomposition.IsRecut.orientation, expose the recut data without unfolding these predicates.
References #
The recut of an L-shaped juxtaposition follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.6.
The side data of the recut of a decomposition whose two rectangles share their initial side column.
Instances For
The side data of the recut of a decomposition whose two rectangles share their terminal side column.
Instances For
The side data of the recut of a decomposition whose common column is the initial side of its first rectangle and the terminal side of its second.
Instances For
The side data of the recut of a decomposition whose common column is the terminal side of its first rectangle and the initial side of its second.
Instances For
E is the recut of the two-step decomposition D: it repartitions the same domain into two
empty rectangles, passes through a different intermediate state, and carries the side data
computed for the orientation of the common side column of D.
Instances For
The common initial side in the left = left recut orientation.
The column and branch data of a left = left recut.
The common initial side of D is not a common side column of its left = left recut.
The common terminal side in the right = right recut orientation.
The column and branch data of a right = right recut.
The common terminal side of D is not a common side column of its right = right
recut.
The mixed common side in the left = right recut orientation.
The row and branch data of a left = right recut.
The mixed common side in the right = left recut orientation.
The row and branch data of a right = left recut.
The side-data orientation of a recut.
A decomposition admitting a recut is nondiagonal: each of the four orientations of the recut data places the two rectangles on distinct side pairs.
A decomposition admitting a recut has exactly one common side column: the side data of that recut records which of the four orientations the decomposition's own common column has.
A recut of a decomposition whose rectangles share their initial side column has the
left = left side data.
A recut of a decomposition whose rectangles share their terminal side column has the
right = right side data.
Existence and uniqueness of the recut #
A two-step decomposition by two empty rectangles sharing exactly one side column has exactly one recut.
The recut of the recut #
If E is a recut of a two-step decomposition D by two empty rectangles sharing exactly one
side column, then D is a recut of E: in each of the four orientations of the common column of
D, the recut carries precisely the side data that describes D as its recut.
The recut as an involution #
The two decompositions of a recut pair repartition the same domain.
A recut passes through a different intermediate grid state.
The first rectangle of a recut is empty.
The second rectangle of a recut is empty.
Two decompositions by empty rectangles with exactly one common side column that admit the same recut are equal.
The recut of a two-step decomposition by two empty rectangles sharing exactly one side column.
Instances For
The recut of a decomposition is a recut of it.
A decomposition whose rectangles share their initial side has a recut classified by the
left = left side data of the original decomposition.
When two empty rectangles share their initial side and the second ends strictly inside the first's column interval, the recut runs from the common side to the second rectangle's terminal side, then on to the first rectangle's terminal side.
When two empty rectangles share their initial side and the first ends strictly inside the second's column interval, the recut runs between the two terminal sides, then from the common initial side to the first rectangle's terminal side.
When two empty rectangles share their initial side and the second ends strictly inside the first's column interval, the first rectangle of the recut has the first rectangle's bottom row and the second rectangle's top row.
When two empty rectangles share their initial side and the second ends strictly inside the first's column interval, the second rectangle of the recut has the first rectangle's rows.
When two empty rectangles share their initial side and the first ends strictly inside the second's column interval, the first rectangle of the recut runs from the first rectangle's top row to the second rectangle's top row.
When two empty rectangles share their initial side and the first ends strictly inside the second's column interval, the second rectangle of the recut spans the two original row intervals.
A decomposition whose rectangles share their terminal side has a recut classified by the
right = right side data of the original decomposition.
When two empty rectangles share their terminal side and the first starts strictly inside the second's column interval, the recut first ends where the original first starts. Its first rectangle has the second's rows; its second spans both row intervals.
When two empty rectangles share their terminal side and the second starts strictly inside the first's column interval, the recut first runs from the second's initial side to the common terminal side, then from the first's initial side to the second's. Its first rectangle spans both row intervals; its second has the first's rows.
A decomposition whose first initial side is the second terminal side has a recut classified
by the left = right side data of the original decomposition.
A decomposition whose first terminal side is the second initial side has a recut classified
by the right = left side data of the original decomposition.
The recut of a decomposition again shares exactly one side column.
Recutting a decomposition with one common side preserves the union of its three side columns.
The recut of a decomposition is different from it: the two pass through different intermediate grid states.
Recutting is an involution on the two-step decompositions by two empty rectangles sharing exactly one side column.