The crossing count of a polygon, and its parity

This is the arithmetic half of the polygonal Jordan curve theorem. A closed polygon is a list of edges; a point off it gets a number, the count of edges the ray leaving the point meets; and the whole separation statement follows from the fact that this number changes by one exactly when the ray's foot sweeps across an edge.

The frame

The blueprint rotates the coordinate system so that no edge is horizontal. Rotating a curve is a change of the curve, which would have to be transported back at the end, so instead the ray direction is carried as a parameter. A direction u (a unit vector, Plane.IsDirection) fixes an orthonormal frame through

• fwd u z — how far along u the point z lies,
• hgt u z — how far across u it lies, positive on the counterclockwise side.

"Horizontal" becomes "level for u", i.e. hgt u a = hgt u b, and exists_direction_hgt_ne — a one-line consequence of Plane.exists_isDirection_det_ne_zero — supplies a u for which no edge of a finite list is level. Nothing below needs the direction to be produced that way: hgt u P.1 ≠ hgt u P.2 for every piece is carried as a hypothesis, so no curve is ever moved and nothing has to be transported back.

The count

An edge is a Piece, i.e. its pair of ends, and a polygon is a List Piece — the same representation the overlay uses, so a subdivision produced by Schoenflies.subdivide can be fed straight in. Crosses u P q says that the level line through q meets P strictly beyond q, with the blueprint's half-open convention at the lower end, which is what makes the count well defined with no genericity assumption. crossings counts and parity reduces mod 2.

Closedness of the polygon enters through IsClosedChain: the boundary of the edge list vanishes mod 2, stated by duality as "every ZMod 2-valued function of the ends sums to zero over the list". edgesOf builds a closed chain from a cyclic vertex list, and IsClosedChain survives subdivide.

Blueprint

• crossings, parity — the count π_C of the section "The polygonal Jordan and crosscut theorems".
• exists_direction_hgt_ne — the setup of that section: a ray direction level for no edge.
• crossings_subdivide, parity_subdivide — Lemma 2.1 (subdivision invariance). Proved for the count, not only its parity, and for the whole subdivide operation of Schoenflies.Subdivide, not only for a single cut.
• parity_eq_of_mem_ball, parity_eq_of_isPreconnected, parity_eq_of_mem_connectedComponentIn — the first half of Lemma 2.2 (crossing parity): π_C is locally constant off the polygon, hence constant on each component of the complement.
• parity_flip — the second half of Lemma 4.4: the two local sides of an edge have opposite parity.
• parity_eq_zero_of_lt — π_C = 0 beyond the polygon in the ray direction; the value on the unbounded region.
• IsClosedChain, edgesOf, isClosedChain_subdivide — the closedness hypothesis, its supply from a cyclic vertex list, and its survival of subdivision.

The frame attached to a direction

def Schoenflies.hgt (u z : Plane) : ℝ

How far across the direction u the point z lies. Edges on which this is constant are the blueprint's horizontal edges.

Equations

• Schoenflies.hgt u z = u.det z

noncomputable def Schoenflies.fwd (u z : Plane) : ℝ

How far along the direction u the point z lies. The ray from q is the set of points of the same hgt and larger fwd.

Equations

• Schoenflies.fwd u z = inner ℝ z u

theorem Schoenflies.hgt_eq (u z : Plane) : hgt u z = u.ofLp 0 * z.ofLp 1 - u.ofLp 1 * z.ofLp 0

theorem Schoenflies.fwd_eq (u z : Plane) : fwd u z = z.ofLp 0 * u.ofLp 0 + z.ofLp 1 * u.ofLp 1

theorem Schoenflies.Plane.add_apply (x y : Plane) (i : Fin 2) : (x + y).ofLp i = x.ofLp i + y.ofLp i

theorem Schoenflies.Plane.smul_apply (r : ℝ) (x : Plane) (i : Fin 2) : (r • x).ofLp i = r * x.ofLp i

theorem Schoenflies.hgt_lin (u a b : Plane) (t : ℝ) : hgt u (a + t • (b - a)) = hgt u a + t * (hgt u b - hgt u a)

The coordinate rewriting used throughout: every claim about hgt and fwd of an affine combination is a polynomial identity in the four coordinates.

theorem Schoenflies.fwd_lin (u a b : Plane) (t : ℝ) : fwd u (a + t • (b - a)) = fwd u a + t * (fwd u b - fwd u a)

theorem Schoenflies.hgt_sub (u x y : Plane) : hgt u (x - y) = hgt u x - hgt u y

theorem Schoenflies.fwd_sub (u x y : Plane) : fwd u (x - y) = fwd u x - fwd u y

theorem Schoenflies.hgt_add_smul (u v x : Plane) (t : ℝ) : hgt u (x + t • v) = hgt u x + t * hgt u v

theorem Schoenflies.fwd_add_smul (u v x : Plane) (t : ℝ) : fwd u (x + t • v) = fwd u x + t * fwd u v

theorem Schoenflies.hgt_eq_fwd_perp (u z : Plane) : hgt u z = fwd u.perp z

hgt against u is fwd against the turned direction. This is how the two coordinates of the frame are bounded by the norm.

theorem Schoenflies.norm_sq_one {u : Plane} (hu : u.IsDirection) : u.ofLp 0 ^ 2 + u.ofLp 1 ^ 2 = 1

@[simp]

theorem Schoenflies.hgt_self {u : Plane} : hgt u u = 0

theorem Schoenflies.fwd_self {u : Plane} (hu : u.IsDirection) : fwd u u = 1

theorem Schoenflies.hgt_perp {u : Plane} (hu : u.IsDirection) : hgt u u.perp = 1

theorem Schoenflies.fwd_perp {u : Plane} : fwd u u.perp = 0

theorem Schoenflies.decomp {u : Plane} (hu : u.IsDirection) (v : Plane) : v = fwd u v • u + hgt u v • u.perp

The frame is a basis: every vector is its two coordinates.

theorem Schoenflies.eq_of_coords {u z w : Plane} (hu : u.IsDirection) (h1 : fwd u z = fwd u w) (h2 : hgt u z = hgt u w) : z = w

Two points with the same frame coordinates are equal.

theorem Schoenflies.abs_fwd_le_norm {u : Plane} (hu : u.IsDirection) (v : Plane) : |fwd u v| ≤ ‖v‖

theorem Schoenflies.abs_hgt_le_norm {u : Plane} (hu : u.IsDirection) (v : Plane) : |hgt u v| ≤ ‖v‖

Where an edge meets a level line

noncomputable def Schoenflies.meet (u a b : Plane) (t : ℝ) : Plane

The point of the line through a and b at height t. Only used when the line is not level, i.e. hgt u a ≠ hgt u b.

Equations

• Schoenflies.meet u a b t = a + ((t - Schoenflies.hgt u a) / (Schoenflies.hgt u b - Schoenflies.hgt u a)) • (b - a)

theorem Schoenflies.hgt_meet {u a b : Plane} (h : hgt u a ≠ hgt u b) (t : ℝ) : hgt u (meet u a b t) = t

theorem Schoenflies.fwd_meet (u a b : Plane) (t : ℝ) : fwd u (meet u a b t) = fwd u a + (t - hgt u a) / (hgt u b - hgt u a) * (fwd u b - fwd u a)

theorem Schoenflies.meet_mem_segment {u a b : Plane} {t : ℝ} (h : hgt u a < hgt u b) (h1 : hgt u a ≤ t) (h2 : t ≤ hgt u b) : meet u a b t ∈ segment ℝ a b

Below the top and above the bottom, the meeting point is on the edge.

theorem Schoenflies.eq_meet {u a b z : Plane} (h : hgt u a ≠ hgt u b) (hz : z ∈ segment ℝ a b) : z = meet u a b (hgt u z)

The meeting point is the only point of the edge at its height.

theorem Schoenflies.meet_swap {u a b : Plane} (h : hgt u a ≠ hgt u b) (t : ℝ) : meet u b a t = meet u a b t

Reversing an edge does not move its meeting point.

The crossing count

def Schoenflies.Crosses (u : Plane) (P : Piece) (q : Plane) : Prop

The edge P meets the level line through q strictly beyond q.

The height test is half-open at the bottom: an edge whose lower end is exactly at the height of q counts, one whose upper end is counts not. That convention is what makes the count well defined at every q off the polygon, with no genericity assumption.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance Schoenflies.decidableCrosses (u : Plane) (P : Piece) (q : Plane) : Decidable (Crosses u P q)

Crossing is decided classically; the count is a noncomputable definition.

Equations

• Schoenflies.decidableCrosses u P q = Classical.dec (Schoenflies.Crosses u P q)

theorem Schoenflies.crosses_swap {u a b : Plane} (h : hgt u a ≠ hgt u b) (q : Plane) : Crosses u (b, a) q ↔ Crosses u (a, b) q

noncomputable def Schoenflies.crossings (u : Plane) (L : List Piece) (q : Plane) : ℕ

How many edges of L the ray from q crosses.

Equations

• Schoenflies.crossings u L q = (List.map (fun (P : Schoenflies.Piece) => if Schoenflies.Crosses u P q then 1 else 0) L).sum

noncomputable def Schoenflies.mark (u : Plane) (P : Piece) (q : Plane) : ZMod 2

The contribution of one edge to the parity.

Equations

• Schoenflies.mark u P q = if Schoenflies.Crosses u P q then 1 else 0

noncomputable def Schoenflies.parity (u : Plane) (L : List Piece) (q : Plane) : ZMod 2

The crossing parity π_C(q).

Equations

• Schoenflies.parity u L q = (List.map (fun (P : Schoenflies.Piece) => Schoenflies.mark u P q) L).sum

@[simp]

theorem Schoenflies.crossings_nil (u q : Plane) : crossings u [] q = 0

@[simp]

theorem Schoenflies.crossings_cons (u : Plane) (P : Piece) (L : List Piece) (q : Plane) : crossings u (P :: L) q = (if Crosses u P q then 1 else 0) + crossings u L q

theorem Schoenflies.crossings_append (u : Plane) (L₁ L₂ : List Piece) (q : Plane) : crossings u (L₁ ++ L₂) q = crossings u L₁ q + crossings u L₂ q

@[simp]

theorem Schoenflies.parity_nil (u q : Plane) : parity u [] q = 0

@[simp]

theorem Schoenflies.parity_cons (u : Plane) (P : Piece) (L : List Piece) (q : Plane) : parity u (P :: L) q = mark u P q + parity u L q

theorem Schoenflies.parity_append (u : Plane) (L₁ L₂ : List Piece) (q : Plane) : parity u (L₁ ++ L₂) q = parity u L₁ q + parity u L₂ q

theorem Schoenflies.parity_eq_crossings (u : Plane) (L : List Piece) (q : Plane) : parity u L q = ↑(crossings u L q)

Subdivision invariance

theorem Schoenflies.nondeg_of_hgt_ne {u : Plane} {P : Piece} (h : hgt u P.1 ≠ hgt u P.2) : P.Nondeg

A piece with distinct end heights is nondegenerate: this is the hypothesis the subdivision machinery of Schoenflies.Subdivide asks for.

theorem Schoenflies.hgt_lt_of_mem_openSegment {u a b c : Plane} (hab : hgt u a < hgt u b) (hc : c ∈ openSegment ℝ a b) : hgt u a < hgt u c ∧ hgt u c < hgt u b

An interior point of a non-level edge is strictly between its ends in height.

theorem Schoenflies.hgt_ne_of_mem_openSegment {u a b c : Plane} (hab : hgt u a ≠ hgt u b) (hc : c ∈ openSegment ℝ a b) : hgt u a ≠ hgt u c ∧ hgt u c ≠ hgt u b

theorem Schoenflies.splitAt_hgt_ne {u : Plane} {P : Piece} (hP : hgt u P.1 ≠ hgt u P.2) (c : Plane) (Q : Piece) : Q ∈ splitAt c P → hgt u Q.1 ≠ hgt u Q.2

Cutting an edge keeps both halves non-level.

theorem Schoenflies.splitAllAt_hgt_ne {u : Plane} {L : List Piece} (hL : ∀ P ∈ L, hgt u P.1 ≠ hgt u P.2) (c : Plane) (Q : Piece) : Q ∈ splitAllAt c L → hgt u Q.1 ≠ hgt u Q.2

theorem Schoenflies.subdivide_hgt_ne {u : Plane} {L : List Piece} (hL : ∀ P ∈ L, hgt u P.1 ≠ hgt u P.2) (points : List Plane) (Q : Piece) : Q ∈ subdivide L points → hgt u Q.1 ≠ hgt u Q.2

theorem Schoenflies.eq_meet_of_smul {u a b z : Plane} (hab : hgt u a ≠ hgt u b) (r : ℝ) (hz : z = a + r • (b - a)) : z = meet u a b (hgt u z)

The meeting point does not move when the edge is cut: both halves lie on the same line, and a non-level line meets a level line only once.

theorem Schoenflies.meet_left_eq {u a b c : Plane} (hab : hgt u a ≠ hgt u b) (hac : hgt u a ≠ hgt u c) {r : ℝ} (hc : c = a + r • (b - a)) (t : ℝ) : meet u a c t = meet u a b t

theorem Schoenflies.meet_right_eq {u a b c : Plane} (hab : hgt u a ≠ hgt u b) (hcb : hgt u c ≠ hgt u b) {r : ℝ} (hc : c = a + r • (b - a)) (t : ℝ) : meet u c b t = meet u a b t

theorem Schoenflies.crossings_splitAt {u : Plane} {P : Piece} (hP : hgt u P.1 ≠ hgt u P.2) (c q : Plane) : crossings u (splitAt c P) q = crossings u [P] q

Cutting one edge does not change the crossing count.

theorem Schoenflies.crossings_splitAllAt {u : Plane} {L : List Piece} (hL : ∀ P ∈ L, hgt u P.1 ≠ hgt u P.2) (c q : Plane) : crossings u (splitAllAt c L) q = crossings u L q

Cutting the whole list at one point does not change the crossing count.

theorem Schoenflies.crossings_subdivide {u : Plane} {L : List Piece} (hL : ∀ P ∈ L, hgt u P.1 ≠ hgt u P.2) (points : List Plane) (q : Plane) : crossings u (subdivide L points) q = crossings u L q

Subdivision invariance (Lemma 2.1). Subdividing changes no crossing count — not even its parity is needed here; the count itself is unchanged.

theorem Schoenflies.parity_subdivide {u : Plane} {L : List Piece} (hL : ∀ P ∈ L, hgt u P.1 ≠ hgt u P.2) (points : List Plane) (q : Plane) : parity u (subdivide L points) q = parity u L q

Subdivision invariance, in the form the crosscut theorem uses.

Closed chains

theorem Schoenflies.sum_map_add {α : Type u_1} (l : List α) (F G : α → ZMod 2) : (List.map (fun (x : α) => F x + G x) l).sum = (List.map F l).sum + (List.map G l).sum

theorem Schoenflies.sum_map_flatMap {α : Type u_1} {β : Type u_2} (l : List α) (g : α → List β) (F : β → ZMod 2) : (List.map F (List.flatMap g l)).sum = (List.map (fun (x : α) => (List.map F (g x)).sum) l).sum

theorem Schoenflies.add_self_zmod_two (x : ZMod 2) : x + x = 0

def Schoenflies.IsClosedChain (L : List Piece) : Prop

The edge list is a closed chain: its boundary vanishes mod 2. Stated by duality — every ZMod 2-valued function of the ends sums to zero over the list — which is exactly what the parity argument consumes, and which isClosedChain_edgesOf supplies for a cyclic vertex list.

Equations

• Schoenflies.IsClosedChain L = ∀ (f : Schoenflies.Plane → ZMod 2), (List.map (fun (P : Schoenflies.Piece) => f P.1 + f P.2) L).sum = 0

theorem Schoenflies.isClosedChain_nil : IsClosedChain []

def Schoenflies.edgesOf (vs : List Plane) : List Piece

The closed edge list of a cyclic vertex list: [v₀v₁, v₁v₂, …, v_{n-1}v₀].

Equations

• Schoenflies.edgesOf vs = vs.zip (vs.rotate 1)

theorem Schoenflies.isClosedChain_edgesOf (vs : List Plane) : IsClosedChain (edgesOf vs)

theorem Schoenflies.isClosedChain_splitAllAt {L : List Piece} (h : IsClosedChain L) (c : Plane) : IsClosedChain (splitAllAt c L)

Cutting an edge in two does not disturb the boundary: the cut point is added twice.

theorem Schoenflies.isClosedChain_subdivide {L : List Piece} (h : IsClosedChain L) (points : List Plane) : IsClosedChain (subdivide L points)

What a list of edges occupies

theorem Schoenflies.mem_cover {z : Plane} {L : List Piece} {P : Piece} (hP : P ∈ L) (hz : z ∈ P.seg) : z ∈ cover L

theorem Schoenflies.isCompact_cover (L : List Piece) : IsCompact (cover L)

theorem Schoenflies.isClosed_cover (L : List Piece) : IsClosed (cover L)

theorem Schoenflies.meet_mem_seg {u : Plane} {t : ℝ} {P : Piece} (h : hgt u P.1 ≠ hgt u P.2) (h1 : min (hgt u P.1) (hgt u P.2) ≤ t) (h2 : t ≤ max (hgt u P.1) (hgt u P.2)) : meet u P.1 P.2 t ∈ P.seg

Where an edge meets the level line, when it does.

Moving the base point

theorem Schoenflies.hgt_along {u : Plane} (q : Plane) (s : ℝ) : hgt u (q + s • u) = hgt u q

theorem Schoenflies.fwd_along {u : Plane} (hu : u.IsDirection) (q : Plane) (s : ℝ) : fwd u (q + s • u) = fwd u q + s

theorem Schoenflies.hgt_across {u : Plane} (hu : u.IsDirection) (q : Plane) (s : ℝ) : hgt u (q + s • u.perp) = hgt u q + s

theorem Schoenflies.fwd_across {u : Plane} (q : Plane) (s : ℝ) : fwd u (q + s • u.perp) = fwd u q

theorem Schoenflies.mem_segment_along {u : Plane} (hu : u.IsDirection) {q y : Plane} {s : ℝ} (hs : 0 ≤ s) (h1 : hgt u y = hgt u q) (h2 : fwd u q ≤ fwd u y) (h3 : fwd u y ≤ fwd u q + s) : y ∈ segment ℝ q (q + s • u)

The segment from q in the ray direction is exactly the points at the same height with fwd in between.

theorem Schoenflies.mem_segment_across {u : Plane} (hu : u.IsDirection) {q y : Plane} {s : ℝ} (hs : 0 ≤ s) (h1 : fwd u y = fwd u q) (h2 : hgt u q ≤ hgt u y) (h3 : hgt u y ≤ hgt u q + s) : y ∈ segment ℝ q (q + s • u.perp)

The segment from q across the ray direction is exactly the points with the same fwd and height in between.

theorem Schoenflies.side_const {u a b z w : Plane} {lo hi ξ : ℝ} (hmiss : ∀ y ∈ segment ℝ a b, fwd u y = ξ → lo ≤ hgt u y → hgt u y ≤ hi → False) (hz : z ∈ segment ℝ a b) (hw : w ∈ segment ℝ a b) (hzl : lo ≤ hgt u z) (hzh : hgt u z ≤ hi) (hwl : lo ≤ hgt u w) (hwh : hgt u w ≤ hi) : ξ < fwd u z ↔ ξ < fwd u w

A connected piece of an edge that stays between two heights and never meets the level line fwd = ξ stays on one side of it.

theorem Schoenflies.parity_move_along {u : Plane} {L : List Piece} (hu : u.IsDirection) (hL : ∀ P ∈ L, hgt u P.1 ≠ hgt u P.2) {q : Plane} {s : ℝ} (hs : 0 ≤ s) (hmiss : ∀ y ∈ segment ℝ q (q + s • u), y ∉ cover L) : parity u L (q + s • u) = parity u L q

Moving the base point along the ray direction, without meeting the polygon, changes no crossing.

Sweeping across the ray direction

noncomputable def Schoenflies.fmark (u q : Plane) (s : ℝ) (v : Plane) : ZMod 2

The marker attached to a vertex when the base point is swept across by s: the vertex counts when its height lies in the half-open band swept out and it lies beyond the base point. Summed over both ends of every edge this vanishes, because the polygon is closed; that is the whole content of crossing parity.

Equations

• One or more equations did not get rendered due to their size.

theorem Schoenflies.mark_swap {u a b : Plane} (h : hgt u a ≠ hgt u b) (q : Plane) : mark u (b, a) q = mark u (a, b) q

theorem Schoenflies.parity_move_across {u : Plane} {L : List Piece} (hu : u.IsDirection) (hL : ∀ P ∈ L, hgt u P.1 ≠ hgt u P.2) (hC : IsClosedChain L) {q : Plane} {s : ℝ} (hs : 0 ≤ s) (hmiss : ∀ y ∈ segment ℝ q (q + s • u.perp), y ∉ cover L) : parity u L (q + s • u.perp) = parity u L q

Sweeping the base point across the ray direction, without meeting the polygon, does not change the parity. This is where the polygon has to be closed.

theorem Schoenflies.parity_move_along' {u : Plane} {L : List Piece} (hu : u.IsDirection) (hL : ∀ P ∈ L, hgt u P.1 ≠ hgt u P.2) {q q' : Plane} (s : ℝ) (hq' : q' = q + s • u) (hmiss : ∀ y ∈ segment ℝ q q', y ∉ cover L) : parity u L q' = parity u L q

The two moves, for a shift of either sign.

theorem Schoenflies.parity_move_across' {u : Plane} {L : List Piece} (hu : u.IsDirection) (hL : ∀ P ∈ L, hgt u P.1 ≠ hgt u P.2) (hC : IsClosedChain L) {q q' : Plane} (s : ℝ) (hq' : q' = q + s • u.perp) (hmiss : ∀ y ∈ segment ℝ q q', y ∉ cover L) : parity u L q' = parity u L q

Crossing parity

theorem Schoenflies.exists_ball_avoiding {L : List Piece} {z : Plane} (h : z ∉ cover L) : ∃ ε > 0, ∀ y ∈ Metric.ball z ε, y ∉ cover L

theorem Schoenflies.parity_eq_of_mem_ball {u : Plane} {L : List Piece} (hu : u.IsDirection) (hL : ∀ P ∈ L, hgt u P.1 ≠ hgt u P.2) (hC : IsClosedChain L) {q q' : Plane} {ε : ℝ} (hq' : q' ∈ Metric.ball q ε) (hmiss : ∀ y ∈ Metric.ball q ε, y ∉ cover L) : parity u L q' = parity u L q

The parity is constant on a ball that misses the polygon: reach any nearby point by a move along the ray direction followed by a move across it.

theorem Schoenflies.parity_eq_of_isPreconnected {u : Plane} {L : List Piece} (hu : u.IsDirection) (hL : ∀ P ∈ L, hgt u P.1 ≠ hgt u P.2) (hC : IsClosedChain L) {S : Set Plane} (hS : IsPreconnected S) (hSC : ∀ z ∈ S, z ∉ cover L) {x y : Plane} (hx : x ∈ S) (hy : y ∈ S) : parity u L x = parity u L y

Crossing parity (Lemma 2.2). π_C is constant on every preconnected subset of the complement of the polygon — in particular on every component.

theorem Schoenflies.parity_eq_of_mem_connectedComponentIn {u : Plane} {L : List Piece} (hu : u.IsDirection) (hL : ∀ P ∈ L, hgt u P.1 ≠ hgt u P.2) (hC : IsClosedChain L) {x y : Plane} (hx : x ∉ cover L) (hy : y ∈ connectedComponentIn (cover L)ᶜ x) : parity u L y = parity u L x

The parity is constant on the component of the complement containing a point.

The value far along the ray, and the jump across an edge

theorem Schoenflies.parity_eq_zero_of_lt {u : Plane} {L : List Piece} (hL : ∀ P ∈ L, hgt u P.1 ≠ hgt u P.2) {q : Plane} (h : ∀ z ∈ cover L, fwd u z < fwd u q) : parity u L q = 0

Beyond the polygon in the ray direction the count is zero.

theorem Schoenflies.parity_flip {u : Plane} (hu : u.IsDirection) {L₁ L₂ : List Piece} {a b p : Plane} (hL : ∀ P ∈ L₁ ++ (a, b) :: L₂, hgt u P.1 ≠ hgt u P.2) (hp : p ∈ openSegment ℝ a b) (h1 : p ∉ cover L₁) (h2 : p ∉ cover L₂) : ∃ δ > 0, ∀ (t : ℝ), 0 < t → t < δ → p - t • u ∉ cover (L₁ ++ (a, b) :: L₂) ∧ p + t • u ∉ cover (L₁ ++ (a, b) :: L₂) ∧ parity u (L₁ ++ (a, b) :: L₂) (p - t • u) = parity u (L₁ ++ (a, b) :: L₂) (p + t • u) + 1

Opposite sides of an edge (Lemma 2.2, second half). At an interior point p of one edge of the list which no other edge of the list passes through, the two points just before and just after p in the ray direction lie off the polygon and have opposite parity: the count changes by one as the base point sweeps across the edge.

Choosing the ray direction

theorem Schoenflies.exists_direction_hgt_ne (L : List Piece) (hnd : ∀ P ∈ L, P.Nondeg) : ∃ (u : Plane), u.IsDirection ∧ ∀ P ∈ L, hgt u P.1 ≠ hgt u P.2

The blueprint's opening move — "rotate so that no edge is horizontal" — without rotating anything: finitely many edge directions rule out only finitely many rays, so some direction is level for none of them.