Directions, and the two arcs cut out by a pair of rays

This module supplies the direction facts that the two-sided strip lemma runs on. Everything here is stated through the sign of the orientation form Plane.det: no angle is named, no inverse trigonometric function appears, and no case distinction on the sense of a turn is ever made.

A direction is a unit vector (Plane.IsDirection). What actually matters about a direction is its ray — the set of its positive multiples — because every predicate below is invariant under positive scaling (Plane.smul_mem_arcCCW). So the arcs are defined on all nonzero vectors and the unit-vector normalisation Plane.dir is only a convenience.

The two arcs

Two directions u and w that are neither equal nor opposite are exactly two directions with det u w ≠ 0 (Plane.det_ne_zero_iff). They cut the circle of directions into two open arcs. The arc traversed counterclockwise from u to w is Plane.arcCCW u w, defined by Sedgewick's ccw predicate on the triple (u, d, w): at least two of the three consecutive orientation forms are positive. This definition is manifestly invariant under rotating the triple, and — this is the point — it is correct for both arcs at once, the short one and the long one, with no sign hypothesis in the definition itself.

Plane.mem_ray_or_mem_arcCCW and Plane.arcCCW_disjoint say that the two arcs and the two bounding rays partition the nonzero vectors.

The transfer fact

Plane.same_arc_of_det_neg_of_det_pos is Appendix C's transfer fact: a direction with negative det against the first ray lies on the same arc as a direction with positive det against the second. Note that no nearness hypothesis is needed for it — see the module note below.

Blueprint

• Plane.IsDirection, Plane.dir, Plane.arcCCW, Plane.det_ne_zero_iff, Plane.mem_ray_or_mem_arcCCW, Plane.arcCCW_disjoint — Appendix C, item 1, "two distinct, non-opposite unit vectors bound two open arcs of directions".
• Plane.same_arc_of_det_neg_of_det_pos — Appendix C, item 1, the transfer fact.
• Plane.exists_isDirection_det_ne_zero, Plane.exists_isDirection_det_and_inner_ne_zero — Appendix C, item 1, "the existence of a unit vector avoiding any prescribed finite set of directions".
• Plane.germs_split, Plane.exists_germ_threshold — the vertex matching inside Lemma 1.8 (Two-sided polygonal strips): the two left half-strip germs land on one arc and the two right ones on the other.

A note on "near"

Appendix C states the transfer fact for directions near the two bounding rays. The nearness is not needed: Plane.mem_arcCCW_rev_iff shows that the arc counterclockwise from w to u is cut out by a disjunction of two sign conditions, so a single sign suffices to land on it. The mirror statement — a direction with positive det against u and one with negative det against w both lie on arcCCW u w — is not available from one sign each, because that arc is cut out by the conjunction (Plane.mem_arcCCW_iff). Lemma 1.8 needs the mirror statement too, for the two right germs, and there the missing second sign is exactly what "s/t small" buys: Plane.exists_germ_threshold supplies it, with an explicit threshold.

Directions

def Schoenflies.Plane.IsDirection (u : Plane) : Prop

A direction is a unit vector. Only the ray a direction spans ever matters below, but normalising to unit length gives a canonical representative of that ray.

Equations

• u.IsDirection = (‖u‖ = 1)

theorem Schoenflies.Plane.IsDirection.ne_zero {u : Plane} (hu : u.IsDirection) : u ≠ 0

theorem Schoenflies.Plane.IsDirection.norm {u : Plane} (hu : u.IsDirection) : ‖u‖ = 1

noncomputable def Schoenflies.Plane.dir (u : Plane) : Plane

The unit vector along a nonzero vector.

Equations

• u.dir = ‖u‖⁻¹ • u

theorem Schoenflies.Plane.isDirection_dir {u : Plane} (hu : u ≠ 0) : u.dir.IsDirection

theorem Schoenflies.Plane.dir_ne_zero {u : Plane} (hu : u ≠ 0) : u.dir ≠ 0

theorem Schoenflies.Plane.dir_eq_smul {u : Plane} (hu : u ≠ 0) : ∃ (c : ℝ), 0 < c ∧ u.dir = c • u

dir u is a positive multiple of u, which is why every sign-of-det predicate is blind to the difference.

Nonvanishing of det

theorem Schoenflies.Plane.ne_zero_left_of_det_ne_zero {u w : Plane} (h : u.det w ≠ 0) : u ≠ 0

theorem Schoenflies.Plane.ne_zero_right_of_det_ne_zero {u w : Plane} (h : u.det w ≠ 0) : w ≠ 0

theorem Schoenflies.Plane.det_ne_zero_iff {u w : Plane} (hu : u.IsDirection) (hw : w.IsDirection) : u.det w ≠ 0 ↔ w ≠ u ∧ w ≠ -u

Two directions are neither equal nor opposite exactly when the orientation form does not kill them. This is the angle-free reading of "two distinct, non-opposite unit vectors".

The two arcs

def Schoenflies.Plane.arcCCW (u w : Plane) : Set Plane

The open arc of directions traversed counterclockwise from u to w.

A nonzero d lies on it when at least two of the three consecutive orientation forms of the triple (u, d, w) are positive. The definition is a cyclic condition, so it is correct for the short arc and for the long arc alike, with no hypothesis on the sign of det u w.

Equations

• u.arcCCW w = {d : Schoenflies.Plane | 0 < u.det d ∧ 0 < d.det w ∨ 0 < d.det w ∧ 0 < w.det u ∨ 0 < w.det u ∧ 0 < u.det d}

theorem Schoenflies.Plane.mem_arcCCW_iff {u w d : Plane} (h : 0 < u.det w) : d ∈ u.arcCCW w ↔ 0 < u.det d ∧ 0 < d.det w

Fix the orientation by 0 < det u w, so that w is counterclockwise of u by less than a half turn. Then the arc counterclockwise from u to w is the short one, and membership is the conjunction of two sign conditions.

theorem Schoenflies.Plane.mem_arcCCW_rev_iff {u w d : Plane} (h : 0 < u.det w) : d ∈ w.arcCCW u ↔ u.det d < 0 ∨ d.det w < 0

With the same orientation 0 < det u w, the arc counterclockwise from w back to u is the long one — more than a half turn — and membership is a disjunction. This asymmetry is the whole content of the transfer fact: one sign suffices here, two are needed on the short arc.

theorem Schoenflies.Plane.arcCCW_disjoint {u w : Plane} (h : 0 < u.det w) : Disjoint (u.arcCCW w) (w.arcCCW u)

The two arcs are disjoint.

theorem Schoenflies.Plane.smul_mem_arcCCW {u w d : Plane} {r : ℝ} (hr : 0 < r) : r • d ∈ u.arcCCW w ↔ d ∈ u.arcCCW w

Every sign-of-det condition is blind to positive rescaling, so the arcs really are sets of rays, not of vectors.

theorem Schoenflies.Plane.dir_mem_arcCCW_iff {u w d : Plane} (hd : d ≠ 0) : d.dir ∈ u.arcCCW w ↔ d ∈ u.arcCCW w

theorem Schoenflies.Plane.mem_ray_or_mem_arcCCW {u w d : Plane} (h : 0 < u.det w) (hd : d ≠ 0) : (∃ (c : ℝ), 0 < c ∧ d = c • u) ∨ (∃ (c : ℝ), 0 < c ∧ d = c • w) ∨ d ∈ u.arcCCW w ∨ d ∈ w.arcCCW u

The two rays and the two arcs exhaust the nonzero vectors. Together with Plane.arcCCW_disjoint this is the statement that two distinct, non-opposite directions bound two arcs.

The transfer fact

theorem Schoenflies.Plane.mem_arcCCW_rev_of_det_neg {u w d : Plane} (h : 0 < u.det w) (hd : u.det d < 0) : d ∈ w.arcCCW u

A direction with negative det against u lies on the arc counterclockwise from w to u. No nearness hypothesis is needed.

theorem Schoenflies.Plane.mem_arcCCW_rev_of_det_pos {u w d : Plane} (h : 0 < u.det w) (hd : 0 < w.det d) : d ∈ w.arcCCW u

A direction with positive det against w lies on the arc counterclockwise from w to u. No nearness hypothesis is needed.

theorem Schoenflies.Plane.same_arc_of_det_neg_of_det_pos {u w d₁ d₂ : Plane} (h : 0 < u.det w) (h₁ : u.det d₁ < 0) (h₂ : 0 < w.det d₂) : d₁ ∈ w.arcCCW u ∧ d₂ ∈ w.arcCCW u

Appendix C, transfer. A direction with negative det against the first ray lies on the same arc as a direction with positive det against the second: both lie on the arc traversed counterclockwise from the second ray to the first.

theorem Schoenflies.Plane.mem_arcCCW_of_det_pos_of_det_neg {u w d : Plane} (h : 0 < u.det w) (h₁ : 0 < u.det d) (h₂ : w.det d < 0) : d ∈ u.arcCCW w

The mirror form, for the other pair of germs: a direction with positive det against u and negative det against w lies on the arc counterclockwise from u to w. Here both signs are genuinely needed; see the module note.

Half-strip germs

Fix a vertex with incoming unit tangent u and outgoing unit tangent w, and let r₁ = -u, r₂ = w be the two rays leaving the vertex, so that perp r₁ = -u^⊥ and perp r₂ = w^⊥. Then the four half-strip germs of Lemma 1.8 are, in the blueprint's own notation,

• incoming left, -t u + s u^⊥ = t • r₁ - s • perp r₁;
• outgoing left, t w + s w^⊥ = t • r₂ + s • perp r₂;
• incoming right, -t u - s u^⊥ = t • r₁ + s • perp r₁;
• outgoing right, t w - s w^⊥ = t • r₂ - s • perp r₂,

each with t, s > 0. The four computations below place them on the two arcs.

theorem Schoenflies.Plane.det_germ_self (r : Plane) (t s : ℝ) : r.det (t • r + s • r.perp) = s * ‖r‖ ^ 2

The orientation form of a germ against its own tangent sees only the transverse coefficient: this is the blueprint's det(r₁, d) = -s and det(r₂, d) = s.

theorem Schoenflies.Plane.det_germ_self' (r : Plane) (t s : ℝ) : (t • r + s • r.perp).det r = -(s * ‖r‖ ^ 2)

theorem Schoenflies.Plane.det_germ (r₁ r₂ : Plane) (t s : ℝ) : (t • r₁ + s • r₁.perp).det r₂ = t * r₁.det r₂ - s * inner ℝ r₁ r₂

The orientation form of a germ at r₁ against the other ray. The inner-product term is what makes the transverse coefficient have to be small relative to the longitudinal one.

theorem Schoenflies.Plane.det_germ' (r₁ r₂ : Plane) (t s : ℝ) : r₁.det (t • r₂ + s • r₂.perp) = t * r₁.det r₂ + s * inner ℝ r₁ r₂

The orientation form of a germ at r₂ against the other ray.

theorem Schoenflies.Plane.germ_mem_arcCCW_rev_of_left {r₁ r₂ : Plane} {s : ℝ} (h : 0 < r₁.det r₂) (hs : 0 < s) (t : ℝ) : t • r₁ - s • r₁.perp ∈ r₂.arcCCW r₁

The incoming left germ lands on the arc counterclockwise from r₂ to r₁, for every longitudinal coefficient t: this is the half of the vertex matching that costs nothing, because that arc is cut out by a disjunction.

theorem Schoenflies.Plane.germ_mem_arcCCW_rev_of_right {r₁ r₂ : Plane} {s : ℝ} (h : 0 < r₁.det r₂) (hs : 0 < s) (t : ℝ) : t • r₂ + s • r₂.perp ∈ r₂.arcCCW r₁

The outgoing left germ lands on the same arc, again for every t.

theorem Schoenflies.Plane.germ_mem_arcCCW_of_left {r₁ r₂ : Plane} {t s : ℝ} (h : 0 < r₁.det r₂) (hs : 0 < s) (hsmall : s * inner ℝ r₁ r₂ < t * r₁.det r₂) : t • r₁ + s • r₁.perp ∈ r₁.arcCCW r₂

The incoming right germ lands on the arc counterclockwise from r₁ to r₂ provided the transverse coefficient is small enough against the longitudinal one. The inequality s ⟪r₁, r₂⟫ < t det(r₁, r₂) is exactly "s/t small", written without a division.

theorem Schoenflies.Plane.germ_mem_arcCCW_of_right {r₁ r₂ : Plane} {t s : ℝ} (h : 0 < r₁.det r₂) (hs : 0 < s) (hsmall : s * inner ℝ r₁ r₂ < t * r₁.det r₂) : t • r₂ - s • r₂.perp ∈ r₁.arcCCW r₂

The outgoing right germ lands on the same arc, under the same smallness condition.

theorem Schoenflies.Plane.germs_split {r₁ r₂ : Plane} {t s : ℝ} (h : 0 < r₁.det r₂) (hs : 0 < s) (hsmall : s * inner ℝ r₁ r₂ < t * r₁.det r₂) : (t • r₁ - s • r₁.perp ∈ r₂.arcCCW r₁ ∧ t • r₂ + s • r₂.perp ∈ r₂.arcCCW r₁) ∧ t • r₁ + s • r₁.perp ∈ r₁.arcCCW r₂ ∧ t • r₂ - s • r₂.perp ∈ r₁.arcCCW r₂

The vertex matching of Lemma 1.8. With the strips narrow enough — s ⟪r₁, r₂⟫ under t det(r₁, r₂) — the two left germs lie on one arc and the two right germs on the other. No angle is named and no case distinction on the sense of the turn arises: the two cases of the turn are the two orders in which r₁ and r₂ may be presented, and det_comm exchanges them.

theorem Schoenflies.Plane.exists_germ_threshold {r₁ r₂ : Plane} (h : 0 < r₁.det r₂) : ∃ ε > 0, ∀ (t s : ℝ), 0 < t → 0 < s → s < ε * t → (t • r₁ - s • r₁.perp ∈ r₂.arcCCW r₁ ∧ t • r₂ + s • r₂.perp ∈ r₂.arcCCW r₁) ∧ t • r₁ + s • r₁.perp ∈ r₁.arcCCW r₂ ∧ t • r₂ - s • r₂.perp ∈ r₁.arcCCW r₂

The quantitative form: there is a slope threshold below which the vertex matching holds. This is what "make the strips narrow enough that this side matching holds in every vertex disk" means in Lemma 1.8, and it is the one place where a size condition, rather than a bare sign of det, is unavoidable.

A direction avoiding finitely many others

The argument is a counting one, with no measure and no trigonometry: the one-parameter family a ↦ (1, a) meets the line of any fixed nonzero vector at most once, so finitely many vectors rule out only finitely many parameters, and ℝ has more than finitely many.

theorem Schoenflies.Plane.exists_isDirection_det_ne_zero {S : Set Plane} (hS : S.Finite) : ∃ (u : Plane), u.IsDirection ∧ ∀ v ∈ S, v ≠ 0 → u.det v ≠ 0

Appendix C. There is a unit vector not parallel to any of a prescribed finite set of nonzero vectors. This is what lets one rotate coordinates so that no edge of a finite polygonal figure is horizontal.

theorem Schoenflies.Plane.exists_isDirection_det_and_inner_ne_zero {S : Set Plane} (hS : S.Finite) : ∃ (u : Plane), u.IsDirection ∧ ∀ v ∈ S, v ≠ 0 → u.det v ≠ 0 ∧ inner ℝ u v ≠ 0

The same, dodging the perpendicular directions too: a unit vector u for which no member of a prescribed finite set of nonzero vectors is either parallel or perpendicular to u. In the rotated coordinates this says that no edge is horizontal and none is vertical.

The arcs are open

Not needed by Lemma 1.8, which uses only the partition, but it justifies the word "open" in "two open arcs of directions".

theorem Schoenflies.Plane.continuous_det_right (u : Plane) : Continuous fun (d : Plane) => u.det d

theorem Schoenflies.Plane.continuous_det_left (w : Plane) : Continuous fun (d : Plane) => d.det w

theorem Schoenflies.Plane.isOpen_arcCCW (u w : Plane) : IsOpen (u.arcCCW w)