Complementary cyclic intervals in finite grids

This file records finite-set bookkeeping for the clockwise cyclic intervals used by toroidal grid rectangles. For distinct endpoints a and b, the two open arcs cIoo a b and cIoo b a are disjoint and together contain exactly the points other than a and b. The half-open arc cIco a b restores the initial endpoint, except in the degenerate case, and indexes the columns or rows of squares covered by a rectangle.

These lemmas are deliberately stated at the one-dimensional Fin n level. Rectangle-pair arguments for the grid differential can then apply them independently in the column and row directions before taking products.

Main definitions

• TauCeti.Grid.cIco: the clockwise half-open arc, the one-dimensional shape of the squares a toroidal rectangle covers.
• TauCeti.Grid.cyclicPosition: the position of a point on the cycle read clockwise from the successor of a basepoint.

Main results

• TauCeti.Grid.disjoint_cIoo_swap: opposite open arcs are disjoint.
• TauCeti.Grid.mem_cIoo_or_mem_cIoo_swap_iff: a point lies in one opposite arc exactly when it is not an endpoint.
• TauCeti.Grid.cIoo_union_swap: the two opposite arcs cover the endpoint complement.
• TauCeti.Grid.mem_cIoo_cyclic_left, TauCeti.Grid.mem_cIoo_cyclic_right: the two rotations of a cyclic order of three points.
• TauCeti.Grid.notMem_cIoo_of_mem_cIoo: if a lies on the arc from d to b, then d is not on the arc from a to b.
• TauCeti.Grid.mem_cIoo_swap_of_notMem: a point off both endpoints that misses one arc lies on the opposite arc.
• TauCeti.Grid.mem_cIoo_of_mem_cIoo_of_mem_cIoo_swap: if a and b lie on opposite arcs from c to d, then d lies on the clockwise arc from a to b.
• TauCeti.Grid.mem_cIoo_and_mem_cIoo_swap_of_notMem: cyclic separation is symmetric, so c and d then lie on the two opposite arcs between a and b.
• TauCeti.Grid.card_cIoo_add_card_cIoo_swap: the two arc lengths add to n - 2.
• TauCeti.Grid.cIoo_image_rev: reversing a clockwise open arc by Fin.rev gives the clockwise open arc with reversed, exchanged endpoints.
• TauCeti.Grid.mem_cIoo_finRotate_finRotate, TauCeti.Grid.mem_cIco_finRotate_finRotate: the cyclic permutation finRotate n preserves the open and half-open arcs, as do its powers (TauCeti.Grid.mem_cIoo_finRotate_pow_finRotate_pow, TauCeti.Grid.mem_cIco_finRotate_pow_finRotate_pow).
• TauCeti.Grid.mem_cIoo_finRotate_rev, TauCeti.Grid.rev_mem_cIco_finRotate_rev: the half-turn x ↦ finRotate n x.rev of the grid points reverses the open arcs of points, and acts on the half-open arcs of squares as Fin.rev.
• TauCeti.Grid.finRotate_ne_self: on a cycle of length at least two, the cyclic successor has no fixed point.
• TauCeti.Grid.cIoo_finRotate_eq_empty, TauCeti.Grid.cIco_eq_singleton_iff: the arcs from a point to its cyclic successor are empty and a single point, and these are the only one-point half-open arcs; TauCeti.Grid.cIoo_castSucc_succ is the case of r.castSucc and r.succ.
• TauCeti.Grid.mem_cIco: membership in the clockwise half-open arc.
• TauCeti.Grid.card_cIco: the length of a half-open arc in standard representatives.
• TauCeti.Grid.cIco_union_swap: opposite nondegenerate half-open arcs partition the grid.
• TauCeti.Grid.cIco_union_cIco_eq_cIco_of_mem_cIoo: an interior point cuts a half-open arc into two adjacent half-open arcs.
• TauCeti.Grid.disjoint_cIco_cIco_of_mem_cIoo: the two pieces of such a cut are disjoint.
• TauCeti.Grid.ite_eq_or_mem_cIoo_eq_add_add: a cut at two points partitions a closed-end cyclic-order test into three disjoint cases, counted in ℕ.
• TauCeti.Grid.cIoo_union_insert_cIoo_eq_cIoo_of_mem_cIoo: an interior point cuts an open arc into two open arcs and the cutting point itself.
• TauCeti.Grid.cIoo_subset_cIoo_right_of_mem_cIoo, TauCeti.Grid.cIoo_subset_cIoo_left_of_mem_cIoo: the two pieces of that cut are contained in the arc they cut.
• TauCeti.Grid.Noninterleaving: two endpoint pairs lie on the same cyclic side of each other.
• TauCeti.Grid.noninterleaving_rev: non-interleaving is preserved by reversing every endpoint with Fin.rev, exchanging the two endpoints within each pair.
• TauCeti.Grid.noninterleaving_of_eq_finRotate, TauCeti.Grid.noninterleaving_of_finRotate_eq: an endpoint pair of two cyclically adjacent points is non-interleaving with every endpoint pair that avoids its endpoints suitably, using TauCeti.Grid.finRotate_mem_cIoo_iff (stepping to the cyclic successor stays on the same side of an arc) and TauCeti.Grid.mem_cIoo_finRotate_left_iff (the arc from the successor of a back to a misses only these two points).
• TauCeti.Grid.mem_cIoo_succAbove_succAbove, TauCeti.Grid.mem_cIco_succAbove_succAbove: inserting a point into the cycle with Fin.succAbove preserves the arcs between old points, and TauCeti.Grid.mem_cIoo_succ_succAbove_succ_succAbove_iff locates the inserted point.
• TauCeti.Grid.mem_cIco_succ_succAbove_succ_succAbove_iff: after inserting a point immediately after i, a half-open arc between old points is the preimage of the old arc under the collapse Fin.predAbove i.
• TauCeti.Grid.cIco_subset_of_mem_cIoo: a half-open arc starting strictly inside another is contained in it.
• TauCeti.Grid.mem_cIco_of_mem_cIco_of_mem_cIoo: the membership form of that nesting.
• TauCeti.Grid.notMem_cIco_finRotate_left: a point is never in the half-open arc starting at its own cyclic successor.
• TauCeti.Grid.self_mem_cIco_finRotate: a point always lies in a nondegenerate half-open arc ending at its own cyclic successor.
• TauCeti.Grid.notMem_cIco_of_mem_cIoo_finRotate: a point and its cyclic successor both miss the half-open arc ending strictly before the successor.
• TauCeti.Grid.mem_cIco_finRotate_iff_mem_insert_cIoo: the half-open arc between cyclic successors is the open arc with its terminal endpoint restored.
• TauCeti.Grid.ite_mem_cIco_finRotate_sub_ite_mem_cIco_finRotate: moving from p to q enters the arc from finRotate n α to finRotate n β when passing α and leaves it when passing β.
• TauCeti.Grid.ite_mem_cIco_finRotate_eq: the arc from finRotate n α to finRotate n β is the complement of α and of the open arc from β to α.
• TauCeti.Grid.ite_mem_cIco_finRotate_sub_one_add_two_mul_eq: the crossing count for a shifted arc after cutting a half-open arc at an interior point.
• TauCeti.Grid.notMem_cIco_of_cIco_union: a point missing both halves of a half-open arc cut at an interior point misses the whole arc.
• TauCeti.Grid.notMem_cIoo_and_notMem_cIco_of_mem_insert_cIco_of_notMem_cIco, TauCeti.Grid.notMem_cIoo_and_notMem_cIco_of_mem_insert_cIco_of_mem_cIoo, TauCeti.Grid.notMem_cIco_of_mem_insert_cIco_of_notMem_cIco, TauCeti.Grid.notMem_cIoo_of_mem_insert_cIco_of_notMem_cIco: a point of the closed arc between two points of an arc misses the pieces of that arc outside them.
• TauCeti.Grid.mem_cIco_of_mem_insert_cIco, TauCeti.Grid.notMem_cIoo_of_mem_insert_cIco, TauCeti.Grid.notMem_cIco_of_mem_insert_cIco, TauCeti.Grid.notMem_cIco_of_noninterleaving: the cyclic order of points on the two closed arcs between a and b.
• TauCeti.Grid.cyclicPosition_lt_of_notMem_cIco: two distinct points whose half-open arc avoids the basepoint come in increasing order of cyclic position.

References

This supplies a prerequisite for TauCetiRoadmap/HeegaardFloer/README.md, Lane G.3, "The complexes and ∂² = 0", where the annular cases in the juxtaposition proof use the fact that the two complementary cyclic intervals partition the non-endpoint columns or rows. The terminology follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3.

noncomputable def TauCeti.Grid.cIoo {n : ℕ} (a b : Fin n) : Finset (Fin n)

The clockwise open cyclic interval from a to b in Fin n.

If a < b in the standard representatives, this is the ordinary open interval a < x < b. If b ≤ a and a ≠ b, it wraps around 0, so it is the union of a < x and x < b. The interval from a point to itself is empty.

@[simp]

theorem TauCeti.Grid.mem_cIoo {n : ℕ} (a b x : Fin n) : x ∈ cIoo a b ↔ a ≠ b ∧ if ↑a < ↑b then ↑a < ↑x ∧ ↑x < ↑b else ↑a < ↑x ∨ ↑x < ↑b

Membership in a clockwise open cyclic interval, unfolded as inequalities between the standard representatives.

@[simp]

theorem TauCeti.Grid.cIoo_self {n : ℕ} (a : Fin n) : cIoo a a = ∅

The open cyclic interval from a point to itself is empty.

theorem TauCeti.Grid.left_notMem_cIoo {n : ℕ} (a b : Fin n) : a ∉ cIoo a b

The initial endpoint is not in its open cyclic interval.

theorem TauCeti.Grid.right_notMem_cIoo {n : ℕ} (a b : Fin n) : b ∉ cIoo a b

The terminal endpoint is not in its open cyclic interval.

theorem TauCeti.Grid.ne_left_of_mem_cIoo {n : ℕ} {a b x : Fin n} (h : x ∈ cIoo a b) : x ≠ a

A point in an open cyclic interval differs from its initial endpoint.

theorem TauCeti.Grid.ne_right_of_mem_cIoo {n : ℕ} {a b x : Fin n} (h : x ∈ cIoo a b) : x ≠ b

A point in an open cyclic interval differs from its terminal endpoint.

noncomputable def TauCeti.Grid.cIco {n : ℕ} (a b : Fin n) : Finset (Fin n)

The clockwise half-open cyclic interval from a to b in Fin n.

This is the arc that starts at a and stops just before b, so it is the open arc cIoo a b with its initial endpoint restored, and it is empty when the two endpoints agree. It is the one-dimensional shape of the set of squares a toroidal rectangle covers, whereas cIoo is the shape of the set of grid points strictly inside it. Mathlib's circular-order intervals stop at Set.cIcc and Set.cIoo precisely because a half-open circular interval cannot be described without separating the degenerate case, which is why the definition below is by cases.

theorem TauCeti.Grid.cIco_of_ne {n : ℕ} {a b : Fin n} (h : a ≠ b) : cIco a b = insert a (cIoo a b)

Between distinct endpoints the half-open cyclic interval is the open one with its initial endpoint restored.

@[simp]

theorem TauCeti.Grid.cIco_self {n : ℕ} (a : Fin n) : cIco a a = ∅

The half-open cyclic interval from a point to itself is empty.

@[simp]

theorem TauCeti.Grid.mem_cIco {n : ℕ} (a b x : Fin n) : x ∈ cIco a b ↔ a ≠ b ∧ if ↑a < ↑b then ↑a ≤ ↑x ∧ ↑x < ↑b else ↑a ≤ ↑x ∨ ↑x < ↑b

Membership in a clockwise half-open cyclic interval, unfolded as inequalities between the standard representatives. Only the comparison against the initial endpoint is weakened relative to Grid.mem_cIoo.

theorem TauCeti.Grid.mem_cIco_iff_of_left_lt_right {n : ℕ} {a b : Fin n} (h : ↑a < ↑b) (x : Fin n) : x ∈ cIco a b ↔ ↑a ≤ ↑x ∧ ↑x < ↑b

The non-wrapping description of a half-open cyclic interval: when the initial endpoint precedes the terminal one, the arc is the ordinary half-open interval between them.

theorem TauCeti.Grid.mem_cIco_iff_of_right_lt_left {n : ℕ} {a b : Fin n} (h : ↑b < ↑a) (x : Fin n) : x ∈ cIco a b ↔ ↑a ≤ ↑x ∨ ↑x < ↑b

The wrapping description of a half-open cyclic interval: when the terminal endpoint precedes the initial one, the arc runs off the top and reappears at the bottom.

theorem TauCeti.Grid.left_mem_cIco {n : ℕ} {a b : Fin n} (h : a ≠ b) : a ∈ cIco a b

The initial endpoint of a nondegenerate half-open cyclic interval belongs to it.

theorem TauCeti.Grid.right_notMem_cIco {n : ℕ} (a b : Fin n) : b ∉ cIco a b

The terminal endpoint is not in its half-open cyclic interval.

theorem TauCeti.Grid.mem_cIoo_of_mem_cIco {n : ℕ} {a b x : Fin n} (h : x ∈ cIco a b) (hx : x ≠ a) : x ∈ cIoo a b

A point of a half-open cyclic interval other than its initial endpoint lies in the open interval with the same endpoints.

theorem TauCeti.Grid.cIoo_subset_cIco {n : ℕ} (a b : Fin n) : cIoo a b ⊆ cIco a b

The open cyclic interval is contained in the half-open one with the same endpoints.

theorem TauCeti.Grid.card_cIco_of_ne {n : ℕ} {a b : Fin n} (h : a ≠ b) : (cIco a b).card = (cIoo a b).card + 1

A nondegenerate half-open cyclic interval has one more point than the corresponding open interval.

theorem TauCeti.Grid.cIco_eq_Ico_of_lt {n : ℕ} {a b : Fin n} (h : ↑a < ↑b) : cIco a b = Finset.Ico a b

A non-wrapping half-open cyclic interval is the ordinary half-open interval in Fin n.

theorem TauCeti.Grid.cIco_eq_Ici_union_Iio_of_lt {n : ℕ} {a b : Fin n} (h : ↑b < ↑a) : cIco a b = Finset.Ici a ∪ Finset.Iio b

A wrapping half-open cyclic interval is the union of the final segment starting at its initial endpoint and the initial segment ending before its terminal endpoint.

@[simp]

theorem TauCeti.Grid.card_cIco {n : ℕ} (a b : Fin n) : (cIco a b).card = if a = b then 0 else if ↑a < ↑b then ↑b - ↑a else n - ↑a + ↑b

The cardinality of a clockwise half-open cyclic interval, including the degenerate case.

theorem TauCeti.Grid.disjoint_cIco_swap {n : ℕ} (a b : Fin n) : Disjoint (cIco a b) (cIco b a)

Opposite half-open cyclic intervals are disjoint.

@[simp]

theorem TauCeti.Grid.cIco_union_swap {n : ℕ} {a b : Fin n} (h : a ≠ b) : cIco a b ∪ cIco b a = Finset.univ

Opposite nondegenerate half-open cyclic intervals partition the grid.

theorem TauCeti.Grid.card_cIco_add_card_cIco_swap {n : ℕ} {a b : Fin n} (h : a ≠ b) : (cIco a b).card + (cIco b a).card = n

The cardinalities of opposite nondegenerate half-open cyclic intervals add to the grid size.

theorem TauCeti.Grid.notMem_cIco_iff_mem_cIco_swap {n : ℕ} {a b x : Fin n} (h : a ≠ b) : x ∉ cIco a b ↔ x ∈ cIco b a

A point lies outside a nondegenerate half-open cyclic interval exactly when it lies in the opposite one.

def TauCeti.Grid.Noninterleaving {n : ℕ} (a₀ a₁ b₀ b₁ : Fin n) : Prop

Two oriented cyclic intervals have non-interleaving endpoint pairs.

The endpoints a₀, a₁ lie on the same side of the pair b₀, b₁, and conversely. This two-sided formulation handles shared-endpoint cases uniformly.

theorem TauCeti.Grid.noninterleaving_iff {n : ℕ} (a₀ a₁ b₀ b₁ : Fin n) : Noninterleaving a₀ a₁ b₀ b₁ ↔ (a₀ ∈ cIoo b₀ b₁ ↔ a₁ ∈ cIoo b₀ b₁) ∧ (b₀ ∈ cIoo a₀ a₁ ↔ b₁ ∈ cIoo a₀ a₁)

The defining endpoint-side conditions for Grid.Noninterleaving.

@[simp]

theorem TauCeti.Grid.noninterleaving_self {n : ℕ} (a₀ a₁ : Fin n) : Noninterleaving a₀ a₁ a₀ a₁

An endpoint pair is non-interleaving with itself.

theorem TauCeti.Grid.noninterleaving_comm {n : ℕ} {a₀ a₁ b₀ b₁ : Fin n} : Noninterleaving a₀ a₁ b₀ b₁ ↔ Noninterleaving b₀ b₁ a₀ a₁

Non-interleaving is symmetric in the two endpoint pairs.

theorem TauCeti.Grid.disjoint_cIoo_swap {n : ℕ} (a b : Fin n) : Disjoint (cIoo a b) (cIoo b a)

Opposite open cyclic intervals with the same endpoints are disjoint.

theorem TauCeti.Grid.mem_cIoo_or_mem_cIoo_swap_iff {n : ℕ} {a b x : Fin n} (h : a ≠ b) : x ∈ cIoo a b ∨ x ∈ cIoo b a ↔ x ≠ a ∧ x ≠ b

Membership in one of the two opposite cyclic intervals is the same as being neither endpoint.

theorem TauCeti.Grid.cIco_union_cIco_eq_cIco_of_mem_cIoo {n : ℕ} {a b c : Fin n} (h : b ∈ cIoo a c) : cIco a b ∪ cIco b c = cIco a c

A point strictly between two endpoints cuts their half-open cyclic interval into two adjacent half-open intervals.

theorem TauCeti.Grid.disjoint_cIco_cIco_of_mem_cIoo {n : ℕ} {a b c : Fin n} (h : b ∈ cIoo a c) : Disjoint (cIco a b) (cIco b c)

The two pieces obtained by cutting a half-open cyclic interval at an interior point are disjoint.

theorem TauCeti.Grid.mem_cIco_and_mem_cIoo_or_mem_cIco_and_mem_cIoo_of_ne {n : ℕ} {a b c x y : Fin n} (hx : x ∈ cIco a b) (hy : y ∈ cIco a c) (hxy : x ≠ y) : x ∈ cIco a c ∧ y ∈ cIoo x c ∨ y ∈ cIco a b ∧ x ∈ cIoo y b

Of two distinct points of arcs with a common start, one lies in the arc of the other, and the other lies strictly between it and the end of that arc.

theorem TauCeti.Grid.mem_cIoo_or_mem_cIoo_of_ne {n : ℕ} {a b c x y : Fin n} (hx : x ∈ cIco a c) (hy : y ∈ cIco b c) (hxy : x ≠ y) : y ∈ cIoo x c ∨ x ∈ cIoo y c

Of two distinct points of arcs with a common end, one lies strictly between the other and that end.

theorem TauCeti.Grid.cIco_union_cIoo_eq_sdiff_of_mem_cIoo {n : ℕ} {B T s t : Fin n} (hs : s ∈ cIco B T) (ht : t ∈ cIoo s T) : cIco B s ∪ cIoo t T = cIco B T \ insert t (cIco s t)

Removing the closed arc from s to t inside the half-open arc from B to T leaves the arcs cIco B s and cIoo t T.

theorem TauCeti.Grid.disjoint_cIco_cIoo_of_mem_cIoo {n : ℕ} {B T s t : Fin n} (hs : s ∈ cIco B T) (ht : t ∈ cIoo s T) : Disjoint (cIco B s) (cIoo t T)

The arcs before and after a closed subarc of a half-open cyclic interval are disjoint.

theorem TauCeti.Grid.cIoo_union_cIco_eq_union_of_mem_cIoo {n : ℕ} {B T s t : Fin n} (ht : t ∈ cIco B T) (hst : t ∈ cIoo s T) : cIoo s T ∪ cIco B t = cIoo s t ∪ cIco B T

Recutting the overlapping arcs cIoo s T and cIco B t at t preserves their union.

theorem TauCeti.Grid.cIoo_inter_cIco_eq_inter_of_mem_cIoo {n : ℕ} {B T s t : Fin n} (ht : t ∈ cIco B T) (hst : t ∈ cIoo s T) : cIoo s T ∩ cIco B t = cIoo s t ∩ cIco B T

Recutting the overlapping arcs cIoo s T and cIco B t at t preserves their intersection.

theorem TauCeti.Grid.cIoo_union_insert_cIoo_eq_cIoo_of_mem_cIoo {n : ℕ} {a b c : Fin n} (h : b ∈ cIoo a c) : cIoo a b ∪ insert b (cIoo b c) = cIoo a c

An interior point cuts a clockwise open arc into two open arcs and the cutting point.

theorem TauCeti.Grid.cIoo_subset_cIoo_right_of_mem_cIoo {n : ℕ} {a b c : Fin n} (h : b ∈ cIoo a c) : cIoo a b ⊆ cIoo a c

The initial piece of a cut open arc is contained in the whole arc.

theorem TauCeti.Grid.cIoo_subset_cIoo_left_of_mem_cIoo {n : ℕ} {a b c : Fin n} (h : b ∈ cIoo a c) : cIoo b c ⊆ cIoo a c

The terminal piece of a cut open arc is contained in the whole arc.

theorem TauCeti.Grid.ite_mem_cIco_eq_add_of_mem_cIoo {n : ℕ} {u v w s : Fin n} (hv : v ∈ cIoo u w) (hs : s ∈ cIco v w) (t : Fin n) : (if t ∈ cIco u s then 1 else 0) = (if t ∈ cIco u v then 1 else 0) + if t ∈ cIco v s then 1 else 0

A point v strictly inside the arc from u to w cuts every arc from u to a point s of the arc from v to w, counted.

theorem TauCeti.Grid.ite_mem_cIoo_eq_add_of_mem_cIoo {n : ℕ} {u v w s : Fin n} (hv : v ∈ cIoo u w) (hs : s ∈ cIco u v) (t : Fin n) : (if t ∈ cIoo s w then 1 else 0) = (if t ∈ cIoo s v then 1 else 0) + if t ∈ cIco v w then 1 else 0

A point v strictly inside the arc from u to w cuts the open arc from a point s of the arc from u to v to w into the open arc from s to v and the arc from v to w, counted.

theorem TauCeti.Grid.ite_mem_cIco_eq_add_add {n : ℕ} {u w s : Fin n} (hs : s ∈ cIco u w) (t : Fin n) : (if t ∈ cIco u w then 1 else 0) = ((if t ∈ cIco u s then 1 else 0) + if t = s then 1 else 0) + if t ∈ cIoo s w then 1 else 0

A point s of the arc from u to w cuts it into the arc before s, the point s and the open arc after s, counted.

theorem TauCeti.Grid.ite_eq_or_mem_cIoo_eq_add_add {n : ℕ} {u v s t : Fin n} (huv : u ≠ v) (hst : s ≠ t) : (if v = t ∨ v ∈ cIoo s t then 1 else 0) = ((if t ∈ cIco u v ∧ s ∈ cIoo t v then 1 else 0) + if t ∈ cIco v u ∧ s ∈ cIoo t u then 1 else 0) + if s ∈ cIco u v ∧ t ∈ cIco v u then 1 else 0

Cutting the circle at distinct points u and v splits the event that v lies after s and at or before t into three disjoint cyclic orders. The first two place both t and s on one side of the cut, with t before s; the third separates them across the cut.

theorem TauCeti.Grid.not_mem_cIoo_iff {n : ℕ} {a b x : Fin n} (h : a ≠ b) : x ∉ cIoo a b ↔ x = a ∨ x = b ∨ x ∈ cIoo b a

A point outside the clockwise interval from a to b is either an endpoint or lies in the opposite clockwise interval.

theorem TauCeti.Grid.mem_insert_cIco_iff_notMem_cIoo {n : ℕ} {a b x : Fin n} (h : a ≠ b) : x ∈ insert b (cIco a b) ↔ x ∉ cIoo b a

For distinct endpoints, the closed cyclic interval from a to b is the complement of the open cyclic interval from b to a.

theorem TauCeti.Grid.mem_cIoo_cyclic_left {n : ℕ} {a b c : Fin n} (h : b ∈ cIoo a c) : c ∈ cIoo b a

Rotating a cyclic order: if b lies on the clockwise arc from a to c, then c lies on the clockwise arc from b to a.

theorem TauCeti.Grid.mem_cIoo_cyclic_right {n : ℕ} {a b c : Fin n} (h : b ∈ cIoo a c) : a ∈ cIoo c b

Rotating a cyclic order the other way: if b lies on the clockwise arc from a to c, then a lies on the clockwise arc from c to b.

theorem TauCeti.Grid.notMem_cIoo_of_mem_cIoo {n : ℕ} {a b d : Fin n} (h : a ∈ cIoo d b) : d ∉ cIoo a b

If a lies on the clockwise arc from d to b, then d does not lie on the clockwise arc from a to b.

theorem TauCeti.Grid.mem_cIoo_swap_of_notMem {n : ℕ} {a b u : Fin n} (hab : a ≠ b) (hua : u ≠ a) (hub : u ≠ b) (hout : u ∉ cIoo a b) : u ∈ cIoo b a

A point off both endpoints and outside one cyclic arc lies on the opposite arc.

theorem TauCeti.Grid.mem_cIoo_of_mem_cIoo_of_mem_cIoo_swap {n : ℕ} {a b c d : Fin n} (ha : a ∈ cIoo c d) (hb : b ∈ cIoo d c) : d ∈ cIoo a b

If a and b lie on opposite arcs from c to d, then d lies on the clockwise arc from a to b.

If a lies on the clockwise arc from c to d while b lies on the opposite arc, then the four points occur in the cyclic order c, a, d, b, so d lies on the clockwise arc from a to b.

theorem TauCeti.Grid.mem_cIoo_and_mem_cIoo_swap_of_notMem {n : ℕ} {a b c d : Fin n} (hbc : b ≠ c) (hbd : b ≠ d) (hbout : b ∉ cIoo c d) (ha : a ∈ cIoo c d) : d ∈ cIoo a b ∧ c ∈ cIoo b a

Cyclic separation is symmetric: if a lies on the clockwise arc from c to d while b, distinct from both endpoints, lies off it, then c and d lie on the two opposite arcs between a and b.

@[simp]

theorem TauCeti.Grid.cIoo_union_swap {n : ℕ} {a b : Fin n} (h : a ≠ b) : cIoo a b ∪ cIoo b a = (Finset.univ.erase a).erase b

The two opposite cyclic intervals cover exactly the complement of their endpoints.

theorem TauCeti.Grid.cIoo_swap_eq_erase_erase_sdiff {n : ℕ} {a b : Fin n} (h : a ≠ b) : cIoo b a = (Finset.univ.erase a).erase b \ cIoo a b

The opposite cyclic interval is the endpoint complement with the first interval removed.

theorem TauCeti.Grid.card_cIoo_add_card_cIoo_swap {n : ℕ} {a b : Fin n} (h : a ≠ b) : (cIoo a b).card + (cIoo b a).card = n - 2

The two complementary cyclic intervals have total cardinality n - 2.

theorem TauCeti.Grid.cIoo_eq_empty_of_le_two {n : ℕ} (hn : n ≤ 2) (a b : Fin n) : cIoo a b = ∅

In a grid of size at most two, every open cyclic interval is empty. There are no grid points strictly between two endpoints on either of the two complementary arcs.

theorem TauCeti.Grid.cIoo_image_rev {n : ℕ} (a b : Fin n) : Finset.image Fin.rev (cIoo a b) = cIoo b.rev a.rev

A clockwise open cyclic interval reversed by Fin.rev is the clockwise open cyclic interval with the two endpoints reversed and exchanged.

Coordinate reversal reverses the cyclic order, so it turns the clockwise arc from a to b into the clockwise arc from bᵒ to aᵒ.

theorem TauCeti.Grid.mem_cIoo_rev_rev {n : ℕ} (a b x : Fin n) : x.rev ∈ cIoo a.rev b.rev ↔ x ∈ cIoo b a

Membership in a clockwise open arc with both endpoints and the queried point reversed by Fin.rev. Since coordinate reversal reverses the cyclic order, the reversed point lies in the reversed arc exactly when the original point lies in the opposite arc.

theorem TauCeti.Grid.mem_cIoo_finRotate_finRotate {n : ℕ} (a b x : Fin n) : (finRotate n) x ∈ cIoo ((finRotate n) a) ((finRotate n) b) ↔ x ∈ cIoo a b

The cyclic permutation finRotate n preserves and reflects membership in open cyclic intervals.

theorem TauCeti.Grid.mem_cIco_finRotate_finRotate {n : ℕ} (a b x : Fin n) : (finRotate n) x ∈ cIco ((finRotate n) a) ((finRotate n) b) ↔ x ∈ cIco a b

The cyclic permutation finRotate n preserves and reflects membership in half-open cyclic intervals.

theorem TauCeti.Grid.mem_cIoo_finRotate_rev {n : ℕ} (a b x : Fin n) : (finRotate n) x.rev ∈ cIoo ((finRotate n) b.rev) ((finRotate n) a.rev) ↔ x ∈ cIoo a b

The half-turn x ↦ finRotate n x.rev of the cycle, which is negation modulo n, reverses the cyclic order: it carries the clockwise open arc from a to b onto the clockwise open arc between the images of b and a.

theorem TauCeti.Grid.rev_mem_cIco_finRotate_rev {n : ℕ} (a b x : Fin n) : x.rev ∈ cIco ((finRotate n) b.rev) ((finRotate n) a.rev) ↔ x ∈ cIco a b

On squares named by their lower-left grid points, the half-turn x ↦ finRotate n x.rev of the grid points acts as Fin.rev: it carries the clockwise half-open arc of squares from a to b onto the one between the images of b and a under the half-turn of the grid points.

theorem TauCeti.Grid.mem_cIoo_finRotate_pow_finRotate_pow {n : ℕ} (k : ℕ) (a b x : Fin n) : (finRotate n ^ k) x ∈ cIoo ((finRotate n ^ k) a) ((finRotate n ^ k) b) ↔ x ∈ cIoo a b

Powers of the cyclic permutation finRotate n preserve and reflect membership in open cyclic intervals.

theorem TauCeti.Grid.mem_cIco_finRotate_pow_finRotate_pow {n : ℕ} (k : ℕ) (a b x : Fin n) : (finRotate n ^ k) x ∈ cIco ((finRotate n ^ k) a) ((finRotate n ^ k) b) ↔ x ∈ cIco a b

Powers of the cyclic permutation finRotate n preserve and reflect membership in half-open cyclic intervals.

theorem TauCeti.Grid.mem_cIco_finRotate_iff_of_ne {n : ℕ} {a b c : Fin n} (ha : a ≠ (finRotate n) c) (hb : b ≠ (finRotate n) c) : (finRotate n) c ∈ cIco a b ↔ c ∈ cIco a b

Replacing a point by its cyclic successor preserves membership in a half-open cyclic interval when the successor is not an endpoint.

theorem TauCeti.Grid.val_finRotate_cases {m : ℕ} (i : Fin (m + 1)) : ↑i = m ∧ ↑((finRotate (m + 1)) i) = 0 ∨ ↑i < m ∧ ↑((finRotate (m + 1)) i) = ↑i + 1

The value of the cyclic successor, split into the wrapping and the non-wrapping case.

theorem TauCeti.Grid.mem_cIco_finRotate_iff_mem_insert_cIoo {n : ℕ} {a b x : Fin n} (h : a ≠ b) : x ∈ cIco ((finRotate n) a) ((finRotate n) b) ↔ x ∈ insert b (cIoo a b)

Between distinct endpoints, the half-open cyclic interval between the cyclic successors of a and b is the open interval from a to b with its terminal endpoint b restored. On a grid, with a and b naming rows of squares, these are the lines a + 1, …, b.

theorem TauCeti.Grid.ite_mem_cIco_finRotate_sub_ite_mem_cIco_finRotate {n : ℕ} {p q α β : Fin n} (hpq : p ≠ q) (hαβ : α ≠ β) : ((if q ∈ cIco ((finRotate n) α) ((finRotate n) β) then 1 else 0) - if p ∈ cIco ((finRotate n) α) ((finRotate n) β) then 1 else 0) = (if α ∈ cIco p q then 1 else 0) - if β ∈ cIco p q then 1 else 0

Crossing count for a shifted arc. For distinct α and β, going from p to q enters the half-open arc from finRotate n α to finRotate n β once if the arc from p to q passes α, and leaves it once if it passes β. On a grid, with α and β naming rows of squares and p, q horizontal grid lines, the shifted arc is the band of lines α + 1, …, β strictly above the centre of square row α and below the centre of square row β.

theorem TauCeti.Grid.ite_mem_cIco_finRotate_eq {n : ℕ} {s α β : Fin n} (hαβ : α ≠ β) : (if s ∈ cIco ((finRotate n) α) ((finRotate n) β) then 1 else 0) = (1 - if α = s then 1 else 0) - if s ∈ cIoo β α then 1 else 0

For distinct α and β, a point s lies on the half-open arc from finRotate n α to finRotate n β unless it is α or lies strictly between β and α. On a grid, with α and β naming rows of squares, the band of lines α + 1, …, β is the complement of the lines β + 1, …, α.

theorem TauCeti.Grid.ite_mem_cIco_finRotate_sub_one_add_two_mul_eq {n : ℕ} {B T s α β : Fin n} (hs : s ∈ cIco B T) (hαβ : α ≠ β) : (if T ∈ cIco ((finRotate n) α) ((finRotate n) β) then 1 else -1) - 1 + 2 * (((if β ∈ cIco B T then 1 else 0) - if α ∈ cIoo s T then 1 else 0) - if β ∈ cIco B s then 1 else 0) = -2 * if s ∈ cIoo β α then 1 else 0

Cutting a half-open arc at an interior point. Let s lie on the half-open arc from B to T and let α ≠ β. The crossing count of T for the arc from finRotate n α to finRotate n β, corrected by the positions of α and β relative to the cut at s, vanishes unless s lies strictly between β and α. On a grid this is the bookkeeping of a pentagon at the replaced grid line: its terminal side runs from row B up to row T through the turn row s, and α, β are the square rows of two markings next to the line. The total also vanishes when α and β lie in the two bigons below and above the turn of a column commutation.

theorem TauCeti.Grid.finRotate_ne_self {n : ℕ} (hn : 1 < n) (a : Fin n) : (finRotate n) a ≠ a

On a cycle of length at least two, no point is fixed by the cyclic successor finRotate n.

theorem TauCeti.Grid.cIoo_finRotate_eq_empty {n : ℕ} (a : Fin n) : cIoo a ((finRotate n) a) = ∅

The open cyclic interval from a point to its cyclic successor is empty.

theorem TauCeti.Grid.cIoo_castSucc_succ {n : ℕ} (r : Fin n) : cIoo r.castSucc r.succ = ∅

The open cyclic interval between consecutive rows r.castSucc and r.succ of a grid with one more row is empty.

theorem TauCeti.Grid.finRotate_mem_cIoo_iff {n : ℕ} {a b x : Fin n} (ha : a ≠ x) (hb : b ≠ (finRotate n) x) : (finRotate n) x ∈ cIoo a b ↔ x ∈ cIoo a b

Moving from a point x to its cyclic successor does not cross the endpoints of an open cyclic interval that starts away from x and ends away from its successor.

theorem TauCeti.Grid.mem_cIoo_finRotate_left_iff {n : ℕ} {a x : Fin n} (ha : a ≠ (finRotate n) a) : x ∈ cIoo ((finRotate n) a) a ↔ x ≠ a ∧ x ≠ (finRotate n) a

The open cyclic interval from the cyclic successor of a back to a contains every point except these two, provided they are distinct.

theorem TauCeti.Grid.noninterleaving_of_eq_finRotate {n : ℕ} {a₀ a₁ b₀ b₁ : Fin n} (ha : a₁ = (finRotate n) a₀) (hb₀ : b₀ ≠ a₀) (hb₁ : b₁ ≠ a₁) : Noninterleaving a₀ a₁ b₀ b₁

An endpoint pair whose second point is the cyclic successor of its first is non-interleaving with every endpoint pair whose first point avoids the first and whose second point avoids the second.

theorem TauCeti.Grid.noninterleaving_of_finRotate_eq {n : ℕ} {a₀ a₁ b₀ b₁ : Fin n} (ha : a₀ = (finRotate n) a₁) (hb₀ : b₀ ≠ a₀) (hb₀' : b₀ ≠ a₁) (hb₁ : b₁ ≠ a₀) (hb₁' : b₁ ≠ a₁) : Noninterleaving a₀ a₁ b₀ b₁

An endpoint pair whose first point is the cyclic successor of its second is non-interleaving with every endpoint pair disjoint from it.

theorem TauCeti.Grid.cIco_eq_singleton_iff {n : ℕ} {a b c : Fin n} : cIco a b = {c} ↔ a = c ∧ b = (finRotate n) c ∧ a ≠ b

A half-open cyclic interval is a single point exactly when that point is its initial endpoint and its terminal endpoint is the distinct cyclic successor of that point.

theorem TauCeti.Grid.noninterleaving_rev {n : ℕ} (a₀ a₁ b₀ b₁ : Fin n) : Noninterleaving a₀.rev a₁.rev b₀.rev b₁.rev ↔ Noninterleaving a₁ a₀ b₁ b₀

Non-interleaving is preserved by reversing every endpoint with Fin.rev, with the cyclic orientation reversal accounted for by exchanging the two endpoints within each pair.

Inserting a point into a cycle

theorem TauCeti.Grid.mem_cIoo_succAbove_succAbove {n : ℕ} (p : Fin (n + 1)) (a b x : Fin n) : p.succAbove x ∈ cIoo (p.succAbove a) (p.succAbove b) ↔ x ∈ cIoo a b

Inserting a new point into the cycle Fin n preserves the clockwise open arcs between old points.

theorem TauCeti.Grid.mem_cIco_succAbove_succAbove {n : ℕ} (p : Fin (n + 1)) (a b x : Fin n) : p.succAbove x ∈ cIco (p.succAbove a) (p.succAbove b) ↔ x ∈ cIco a b

Inserting a new point into the cycle Fin n preserves the clockwise half-open arcs between old points.

theorem TauCeti.Grid.mem_cIoo_succ_succAbove_succ_succAbove_iff {n : ℕ} (i a b : Fin n) : i.succ ∈ cIoo (i.succ.succAbove a) (i.succ.succAbove b) ↔ i ∈ cIco a b

A point inserted immediately after i lies strictly inside the arc between two old points exactly when the arc passes from i to its successor, that is, when i lies in the half-open arc.

theorem TauCeti.Grid.mem_cIco_succ_succAbove_succ_succAbove_iff {n : ℕ} (i a b : Fin n) (x : Fin (n + 1)) : x ∈ cIco (i.succ.succAbove a) (i.succ.succAbove b) ↔ i.predAbove x ∈ cIco a b

Collapsing the point inserted immediately after i back onto i with Fin.predAbove identifies the half-open arcs between old points before and after the insertion.

theorem TauCeti.Grid.castSucc_mem_cIco_succ {n : ℕ} {a : Fin (n + 1)} {i : Fin n} (h : a ≠ i.succ) : i.castSucc ∈ cIco a i.succ

The cyclic predecessor of the terminal endpoint i.succ lies in every nondegenerate half-open arc ending there.

theorem TauCeti.Grid.cIco_subset_of_mem_cIoo {n : ℕ} {a b r : Fin n} (h : b ∈ cIoo a r) : cIco b r ⊆ cIco a r

A half-open cyclic interval starting strictly inside another is contained in it.

theorem TauCeti.Grid.cIco_subset_cIco_union_cIco {n : ℕ} {t w u : Fin n} : cIco t u ⊆ cIco w u ∪ cIco t w

Moving the initial endpoint of a half-open cyclic interval covers it by the interval from the new initial endpoint and the interval between the two initial endpoints: every point of cIco t u lies in cIco w u ∪ cIco t w. With no hypothesis on w the two intervals may overlap, so this is a covering by a union, not a partition; the strict cut is cIco_union_cIco_eq_cIco_of_mem_cIoo.

theorem TauCeti.Grid.mem_cIco_of_mem_cIco_of_mem_cIoo {n : ℕ} {A B C s : Fin n} (hmem : s ∈ cIco A B) (hB : B ∈ cIoo A C) : s ∈ cIco A C

Interval nesting: a point in cIco A B with B strictly inside cIco A C lies in cIco A C. This is the cIco-membership version of cIco_subset_of_mem_cIoo.

theorem TauCeti.Grid.insert_cIco_subset_cIco {n : ℕ} {A C s s' : Fin n} (hs : s ∈ cIco A C) (hs' : s' ∈ cIoo s C) : insert s' (cIco s s') ⊆ cIco A C

If s lies in the half-open cyclic interval from A to C and s' lies strictly between s and C, then the closed cyclic interval from s to s' lies in the one from A to C.

theorem TauCeti.Grid.mem_cIoo_of_mem_cIco_of_mem_cIoo {n : ℕ} {a b c s s' : Fin n} (hb : b ∈ cIoo a c) (hs : s ∈ cIco a b) (hs' : s' ∈ cIoo s b) : s' ∈ cIoo s c

A point strictly between s and an interior point b of cIoo a c, where s lies in the initial piece cIco a b, also lies strictly between s and c.

@[simp]

theorem TauCeti.Grid.notMem_cIco_finRotate_left {n : ℕ} (c r : Fin n) : c ∉ cIco (c + 1) r

A point is never in the half-open cyclic interval starting at its own successor. Going clockwise from c + 1, the point c is the last point reached — only after a full cycle. The half-open arc cIco (c + 1) r stops before r, hence before completing the cycle, so it never reaches c. Stated with c + 1 rather than finRotate n c so the left-hand side is already in simp normal form (finRotate_apply would otherwise rewrite it). The NeZero n instance needed for c + 1 is supplied locally from c itself (as in finRotate_apply), so no typeclass hypothesis is required.

theorem TauCeti.Grid.self_mem_cIco_finRotate {n : ℕ} {a c : Fin n} (h : c ≠ (finRotate n) a) : a ∈ cIco c ((finRotate n) a)

A point lies in every nondegenerate half-open cyclic interval ending at its own cyclic successor: going clockwise, a is the last point reached before finRotate n a, so any arc that stops there and does not start there has already passed through a.

theorem TauCeti.Grid.notMem_cIco_of_mem_cIoo_finRotate {n : ℕ} {l m a : Fin n} (h : m ∈ cIoo l ((finRotate n) a)) : a ∉ cIco l m ∧ (finRotate n) a ∉ cIco l m

If m lies strictly between l and the cyclic successor of a, then neither a nor its successor lies in the half-open arc from l to m.

theorem TauCeti.Grid.notMem_cIco_of_cIco_union {n : ℕ} {p r₀ r₁ s : Fin n} (h₁ : p ∉ cIco r₀ r₁) (h₂ : p ∉ cIco r₁ s) (hcyc : r₁ ∈ cIoo r₀ s) : p ∉ cIco r₀ s

A point missing both halves of a half-open cyclic interval cut at an interior point misses the whole interval.

theorem TauCeti.Grid.mem_cIco_of_mem_cIco_of_notMem_cIco_left {n : ℕ} {a b c s : Fin n} (hs : s ∈ cIco a c) (hb : b ∈ cIoo a c) (h : s ∉ cIco a b) : s ∈ cIco b c

A point of a half-open cyclic interval cut at an interior point b that misses the initial piece lies in the final piece.

theorem TauCeti.Grid.mem_cIco_of_mem_cIco_of_notMem_cIco_right {n : ℕ} {a b c s : Fin n} (hs : s ∈ cIco a c) (hb : b ∈ cIoo a c) (h : s ∉ cIco b c) : s ∈ cIco a b

A point of a half-open cyclic interval cut at an interior point b that misses the final piece lies in the initial piece.

theorem TauCeti.Grid.cIco_subset_cIco_of_mem_cIco {n : ℕ} {a b s : Fin n} (hs : s ∈ cIco a b) : cIco a s ⊆ cIco a b

The half-open cyclic interval from a to a point s of the interval from a to b is contained in it.

theorem TauCeti.Grid.cIoo_subset_cIco_of_mem_cIco {n : ℕ} {a b s : Fin n} (hs : s ∈ cIco a b) : cIoo s b ⊆ cIco a b

The open cyclic interval from a point s of the half-open interval from a to b up to b is contained in that interval.

theorem TauCeti.Grid.mem_cIco_and_mem_cIoo_of_mem_cIoo_of_mem_cIco {n : ℕ} {a b c s s' : Fin n} (hs : s ∈ cIco a c) (hs' : s' ∈ cIoo s c) (h : s' ∈ cIco a b) : s ∈ cIco a b ∧ s' ∈ cIoo s b

Two points s and then s' of the half-open cyclic interval from a to c lie, in the same order, in every initial piece of it containing s'.

theorem TauCeti.Grid.mem_cIco_and_mem_cIoo_of_mem_cIco_of_mem_cIco {n : ℕ} {a m c s s' : Fin n} (hm : m ∈ cIoo a c) (hs : s ∈ cIco a m) (hs' : s' ∈ cIco m c) : s ∈ cIco a c ∧ s' ∈ cIoo s c

Let m lie strictly between a and c, let s lie in the half-open cyclic interval from a to m and s' in the one from m to c. Then s lies in the half-open interval from a to c and s' strictly between s and c.

theorem TauCeti.Grid.mem_cIco_or_mem_cIoo_iff_mem_cIco_and_notMem_insert_cIco {n : ℕ} {a m c s s' r : Fin n} (hm : m ∈ cIoo a c) (hs : s ∈ cIco a m) (hs' : s' ∈ cIco m c) : (r ∈ cIco a s ∨ r ∈ cIoo s' c ↔ r ∈ cIco a c ∧ r ∉ insert s' (cIco s s')) ∧ ¬(r ∈ cIco a s ∧ r ∈ cIoo s' c)

Let m lie strictly between a and c, let s lie in the half-open cyclic interval from a to m and s' in the one from m to c. A point lies in the half-open interval from a to s or strictly between s' and c exactly when it lies in the half-open interval from a to c outside the closed interval from s to s', and it never lies in both.

theorem TauCeti.Grid.mem_cIoo_or_mem_cIco_iff_mem_cIoo {n : ℕ} {a m c s s' r : Fin n} (hm : m ∈ cIoo a c) (hs : s ∈ cIco a m) (hs' : s' ∈ cIco m c) : (r ∈ cIoo s m ∨ r ∈ cIco m s' ↔ r ∈ cIoo s s') ∧ ¬(r ∈ cIoo s m ∧ r ∈ cIco m s')

Let m lie strictly between a and c, let s lie in the half-open cyclic interval from a to m and s' in the one from m to c. A point lies strictly between s and m or in the half-open interval from m to s' exactly when it lies strictly between s and s', and it never lies in both.

theorem TauCeti.Grid.notMem_cIoo_and_notMem_cIco_of_mem_insert_cIco_of_notMem_cIco {n : ℕ} {a b s s' r r' : Fin n} (hs : s ∈ cIco a b) (hs' : s' ∉ cIco a b) (hr : r ∈ insert s (cIco s' s)) (hr' : r' ∈ insert s' (cIco s s')) : r ∉ cIoo s b ∧ r' ∉ cIco a s

A point of the closed arc from s' to s misses the open arc from s to b, and a point of the closed arc from s to s' misses the arc from a to s, when s but not s' lies in the arc from a to b.

theorem TauCeti.Grid.notMem_cIoo_and_notMem_cIco_of_mem_insert_cIco_of_mem_cIoo {n : ℕ} {a b s s' r : Fin n} (hs : s ∈ cIco a b) (hs' : s' ∈ cIoo s b) (hr : r ∈ insert s' (cIco s s')) : r ∉ cIoo s' b ∧ r ∉ cIco a s

A point of the closed arc between two points s and then s' of the arc from a to b misses the arc after the second point and the arc before the first.

theorem TauCeti.Grid.notMem_cIco_of_mem_insert_cIco_of_notMem_cIco {n : ℕ} {a b m s s' r : Fin n} (hs' : s' ∈ cIco a b) (hs : s ∈ cIoo s' b) (hm : s' ∈ cIco a m) (hr : r ∈ insert s' (cIco s s')) (hrm : r ∉ cIco a m) : r ∉ cIco a s

A point of the closed arc from s to s' misses the arc from a to s when s' precedes s in the arc from a to b, and the point misses an arc from a containing s'.

theorem TauCeti.Grid.notMem_cIoo_of_mem_insert_cIco_of_notMem_cIco {n : ℕ} {b m s s' r : Fin n} (hs' : s' ∈ cIoo s b) (hm : s' ∈ cIco m b) (hr : r ∈ insert s (cIco s' s)) (hrm : r ∉ cIco m b) : r ∉ cIoo s b

A point of the closed arc from s' to s misses the open arc from s to b when s' follows s in that arc, and the point misses an arc ending at b containing s'.

theorem TauCeti.Grid.mem_cIco_of_mem_insert_cIco {n : ℕ} {a b c d : Fin n} (hc : c ∈ insert a (cIco b a)) (hd : d ∈ insert b (cIco a b)) (hcd : c ≠ d) (ha : a ≠ d) : a ∈ cIco c d

If c lies on the closed arc from b to a and d lies on the closed arc from a to b, with c ≠ d, then a lies on the half-open arc from c to d unless a = d.

theorem TauCeti.Grid.notMem_cIoo_of_mem_insert_cIco {n : ℕ} {a b c d : Fin n} (hc : c ∈ insert a (cIco b a)) (hd : d ∈ insert b (cIco a b)) : c ∉ cIoo a d

A point c of the closed arc from b to a is not strictly between a and any point d of the closed arc from a to b.

theorem TauCeti.Grid.notMem_cIco_of_mem_insert_cIco {n : ℕ} {a b c d : Fin n} (hc : c ∈ insert a (cIco b a)) (hd : d ∈ insert b (cIco a b)) (h : c ≠ d) : d ∉ cIco c a

If c lies on the closed arc from b to a and d ≠ c lies on the closed arc from a to b, then d is not on the half-open arc from c to a.

theorem TauCeti.Grid.notMem_cIco_of_noninterleaving {n : ℕ} {a b c₀ c₁ d₀ d₁ : Fin n} (hc₀ : c₀ ∈ insert a (cIco b a)) (hc₁ : c₁ ∈ insert a (cIco b a)) (hd₀ : d₀ ∈ insert b (cIco a b)) (hd₁ : d₁ ∈ insert b (cIco a b)) (hnon : Noninterleaving c₀ c₁ d₀ d₁) (hc : c₀ ≠ c₁) (hd : d₀ ≠ d₁) (ha : a ≠ d₁) : d₀ ∉ cIco c₁ a

Let the distinct points c₀, c₁ lie on the closed arc from b to a and the distinct points d₀, d₁ on the closed arc from a to b. If the pairs do not interleave and a ≠ d₁, then d₀ is not on the half-open arc from c₁ to a.

Positions on the cycle

noncomputable def TauCeti.Grid.cyclicPosition {n : ℕ} (p r : Fin n) : ℕ

The position of r on the cycle Fin n read clockwise from the cyclic successor of p: the length of the half-open arc from finRotate n p to r. The successor of p has position 0 and p itself comes last.

@[simp]

theorem TauCeti.Grid.cyclicPosition_add_one_self {n : ℕ} (p : Fin n) : cyclicPosition p (p + 1) = 0

The cyclic successor p + 1 of p (that is, finRotate n p) comes first, in position 0.

@[simp]

theorem TauCeti.Grid.cyclicPosition_self {n : ℕ} (p : Fin n) : cyclicPosition p p = n - 1

The point p itself comes last, in position n - 1.

theorem TauCeti.Grid.cyclicPosition_lt_of_notMem_cIco {n : ℕ} {p a b : Fin n} (hab : a ≠ b) (h : p ∉ cIco a b) : cyclicPosition p a < cyclicPosition p b

Two distinct points whose half-open arc avoids p come in strictly increasing order of position read from the cyclic successor of p.