Parity splitting: a crosscut adds the two crossing counts

Lemma 2.7. A crosscut P of a simple closed polygon C cuts it into two arcs A₁, A₂, and the two closed curves Jᵢ = Aᵢ ∪ P satisfy π_C = π_{J₁} + π_{J₂} off C ∪ P. The blueprint calls this identity "the whole of the polygonal crosscut theorem": Lemma 2.6 exhibits two cells of Ω ∖ P, and this is what says there are no others.

Where the split is made, and why

The crossing count of Schoenflies/Parity.lean is a function of a List Piece, not of a set, and not of a ClosedPolygon. Two edge lists with the same carrier can have different parity — a list that traverses one segment twice is the obvious example — so the identity cannot be stated for the sets Aᵢ ∪ P. It is stated, and proved, for edge lists:

the edge list of `C` is `A₁ ++ A₂`, that of `Jᵢ` is `Aᵢ ++ K`,

where K is the edge list of the crosscut. Then π_{J₁} + π_{J₂} = π_{A₁} + π_{A₂} + 2 π_K and the crosscut's contribution cancels mod 2. That is parity_split, and it needs no geometry at all — no simplicity, no direction, no separation. Everything the blueprint's picture contributes is in the hypothesis that the lists decompose that way.

Two mismatches between "the edge list of Jᵢ is Aᵢ together with K" and literal list equality have to be absorbed, because a consumer building Jᵢ as a ClosedPolygon controls neither:

• the edges come in some cyclic order of that polygon's own choosing, and
• one of the two curves must traverse the crosscut backwards, so its pieces are the reversed pairs.

SameEdges is the equivalence that forgives exactly these two: a permutation of the lists after each piece has been put in canonical order by Schoenflies.orientPiece. Parity, carrier, closedness and non-levelness are all invariant under it (SameEdges.parity_eq, SameEdges.cover_eq, SameEdges.isChainFrom, SameEdges.hgt_ne), so a consumer may hand over its edge list in whatever order and orientation it happens to have — sameEdges_of_perm_reverse_swap absorbs both mismatches in one step.

Nothing is assumed about the sets: ClosedPolygon.carrier_eq_of_sameEdges derives Jᵢ.carrier = Aᵢ ∪ P from the edge lists alone, so the geometric hypothesis a consumer has to discharge is only ever combinatorial.

The construction

ClosedPolygon.arcPieces C a k is the edge list of the arc of C that leaves vertex a and runs forward through k edges — the object the split produces, exported as an object rather than hidden behind an existential. Its two governing facts are

• ClosedPolygon.arcPieces_split_perm: arcPieces C a k ++ arcPieces C (a + k) (m + 3 - k) is a permutation of C.pieces — the arcs really do partition the edges; and
• ClosedPolygon.isChainFrom_arcPieces: the arc's mod-2 boundary is its two end vertices, which is what makes Aᵢ ++ K a closed chain and hence eligible for every parity theorem.

IsChainFrom is the open-path companion of Schoenflies.IsClosedChain, stated by the same duality; IsChainFrom.isClosedChain_append is the one-line reason that an arc and a crosscut with the same two ends close up. pathPieces turns a polyline into such a chain, which is how the crosscut itself is normally presented.

The endpoints of the crosscut are taken to be vertices of C; the blueprint's opening move, "subdivide C at p and q", is what puts them there, and is parity_subdivide (Lemma 2.1) applied before any of this. Nothing below re-proves it. A consumer whose crosscut lands in the interiors of edges rewrites with parity_subdivide first and then applies parity_split to the subdivided list, whose hypotheses are about lists and not about polygons; what such a consumer must supply for itself is the decomposition of the subdivided list into two arcs, which arcPieces does not provide — arcPieces splits C.pieces at vertices.

Blueprint

• SameEdges, IsChainFrom, pathPieces, ClosedPolygon.arcPieces — the definition of the split. "After the subdivision the edge set of C is the disjoint union of the edge sets of A₁ and A₂, and the edge set of Jᵢ is that of Aᵢ together with that of P."
• parity_split, ClosedPolygon.parity_splitting — Lemma 2.7, equation (2.2) π_C = π_{J₁} + π_{J₂}.
• ClosedPolygon.crosscut_inside_exactly_one, ClosedPolygon.crosscut_outside_agree — the "Consequently" of Lemma 2.7, which is where Theorem 2.3 enters: a point of Int(C) off P lies inside exactly one of J₁, J₂, and a point of Ext(C) off P lies inside both or inside neither.
• ClosedPolygon.parity_eq_one_iff — the two halves of the last sentence of Theorem 2.3, read as a single criterion.
• ClosedPolygon.carrier_eq_of_sameEdges, ClosedPolygon.notMem_carrier_of_sameEdges — the bridge back to the sets: Jᵢ occupies Aᵢ ∪ P, so "off C and off P" is "off Jᵢ".

One lemma here strengthens one on main: mark_swap' drops the non-levelness hypothesis of Schoenflies.mark_swap, because a level edge is crossed from nowhere and so contributes 0 under either name. Its home is Schoenflies/Parity.lean.

Edge lists up to order and orientation

Parity, carrier and closedness are all functions of the multiset of unoriented edges. This section says so, so that a consumer may present the edge list of a curve in any order and with either name for each edge.

theorem Schoenflies.not_crosses_of_level {u c d : Plane} (h : hgt u c = hgt u d) (q : Plane) : ¬Crosses u (c, d) q

A level edge is crossed from nowhere: the ray from q would have to leave at a height both ≥ and < the common height of the two ends.

theorem Schoenflies.mark_swap' (u : Plane) (P : Piece) (q : Plane) : mark u (P.2, P.1) q = mark u P q

The contribution of an edge does not depend on which end is named first. This is Schoenflies.mark_swap with its non-levelness hypothesis removed: a level edge contributes 0 under either name.

theorem Schoenflies.parity_perm {L₁ L₂ : List Piece} (h : L₁.Perm L₂) (u q : Plane) : parity u L₁ q = parity u L₂ q

Reordering the edges does not change the count.

theorem Schoenflies.cover_perm {L₁ L₂ : List Piece} (h : L₁.Perm L₂) : cover L₁ = cover L₂

Reordering the edges does not change what they occupy.

theorem Schoenflies.orientPiece_eq_or (P : Piece) : orientPiece P = P ∨ orientPiece P = (P.2, P.1)

orientPiece either leaves a piece alone or reverses it; that is all this file uses.

theorem Schoenflies.mark_orientPiece (u : Plane) (P : Piece) (q : Plane) : mark u (orientPiece P) q = mark u P q

theorem Schoenflies.parity_map_orientPiece (u : Plane) (L : List Piece) (q : Plane) : parity u (List.map orientPiece L) q = parity u L q

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

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

theorem Schoenflies.chainSum_map_orientPiece (f : Plane → ZMod 2) (L : List Piece) : (List.map (fun (P : Piece) => f P.1 + f P.2) (List.map orientPiece L)).sum = (List.map (fun (P : Piece) => f P.1 + f P.2) L).sum

Orienting a piece does not change its mod-2 boundary.

def Schoenflies.SameEdges (L₁ L₂ : List Piece) : Prop

Two edge lists carry the same edges: they agree after reordering, each edge being free to be named by either of its two ends first. This is the relation under which "the edge list of Jᵢ is that of Aᵢ together with that of P" is true — a ClosedPolygon built on Aᵢ ∪ P lists its edges in its own cyclic order, and traverses one of the two pieces backwards.

Equations

• Schoenflies.SameEdges L₁ L₂ = (List.map Schoenflies.orientPiece L₁).Perm (List.map Schoenflies.orientPiece L₂)

theorem Schoenflies.SameEdges.refl (L : List Piece) : SameEdges L L

theorem Schoenflies.SameEdges.symm {L₁ L₂ : List Piece} (h : SameEdges L₁ L₂) : SameEdges L₂ L₁

theorem Schoenflies.SameEdges.trans {L₁ L₂ L₃ : List Piece} (h₁ : SameEdges L₁ L₂) (h₂ : SameEdges L₂ L₃) : SameEdges L₁ L₃

theorem Schoenflies.SameEdges.of_perm {L₁ L₂ : List Piece} (h : L₁.Perm L₂) : SameEdges L₁ L₂

A reordering is in particular the same edges.

theorem Schoenflies.SameEdges.append {L₁ L₂ L₁' L₂' : List Piece} (h₁ : SameEdges L₁ L₁') (h₂ : SameEdges L₂ L₂') : SameEdges (L₁ ++ L₂) (L₁' ++ L₂')

theorem Schoenflies.sameEdges_reverse (L : List Piece) : SameEdges L.reverse L

theorem Schoenflies.sameEdges_map_swap (L : List Piece) : SameEdges (List.map (fun (P : Piece) => (P.2, P.1)) L) L

Reversing every edge changes nothing. This is the clause a consumer needs when its second curve traverses the crosscut backwards.

theorem Schoenflies.sameEdges_of_perm_reverse_swap {L A K : List Piece} (h : L.Perm (A ++ (List.map (fun (P : Piece) => (P.2, P.1)) K).reverse)) : SameEdges L (A ++ K)

The shape a consumer arrives with. A ClosedPolygon built on Aᵢ ∪ P lists its edges in a cyclic order of its own choosing — any permutation — and one of the two must run the crosscut backwards, which reverses the list and names every piece the other way round. All of that is forgiven at once.

theorem Schoenflies.SameEdges.parity_eq {L₁ L₂ : List Piece} (h : SameEdges L₁ L₂) (u q : Plane) : parity u L₁ q = parity u L₂ q

theorem Schoenflies.SameEdges.cover_eq {L₁ L₂ : List Piece} (h : SameEdges L₁ L₂) : cover L₁ = cover L₂

theorem Schoenflies.SameEdges.exists_mem {L₁ L₂ : List Piece} (h : SameEdges L₁ L₂) {Q : Piece} (hQ : Q ∈ L₁) : ∃ R ∈ L₂, orientPiece R = orientPiece Q

Every edge of L₁ is an edge of L₂, up to the naming of its two ends.

theorem Schoenflies.SameEdges.hgt_ne {u : Plane} {L₁ L₂ : List Piece} (h : SameEdges L₁ L₂) (hL : ∀ Q ∈ L₂, hgt u Q.1 ≠ hgt u Q.2) (Q : Piece) : Q ∈ L₁ → hgt u Q.1 ≠ hgt u Q.2

Non-levelness for a direction transfers: it is a property of the unoriented edge.

theorem Schoenflies.hgt_ne_append {u : Plane} {L₁ L₂ : List Piece} (h₁ : ∀ Q ∈ L₁, hgt u Q.1 ≠ hgt u Q.2) (h₂ : ∀ Q ∈ L₂, hgt u Q.1 ≠ hgt u Q.2) (Q : Piece) : Q ∈ L₁ ++ L₂ → hgt u Q.1 ≠ hgt u Q.2

Chains with two ends

Schoenflies.IsClosedChain says the mod-2 boundary of an edge list vanishes. An arc and a crosscut are not closed; each has a boundary, namely its two ends, and closing them up is the statement that the two boundaries agree. Stated by the same duality as IsClosedChain, so that the two definitions compose with nothing but List.sum_append.

def Schoenflies.IsChainFrom (L : List Piece) (p q : Plane) : Prop

L is a chain from p to q: its mod-2 boundary is p together with q. Stated by duality, exactly as Schoenflies.IsClosedChain is.

Equations

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

theorem Schoenflies.isChainFrom_self_iff {p : Plane} {L : List Piece} : IsChainFrom L p p ↔ IsClosedChain L

A chain whose two ends coincide is a closed chain, and conversely.

theorem Schoenflies.isChainFrom_nil (p : Plane) : IsChainFrom [] p p

theorem Schoenflies.IsChainFrom.append {p q r : Plane} {L₁ L₂ : List Piece} (h₁ : IsChainFrom L₁ p q) (h₂ : IsChainFrom L₂ q r) : IsChainFrom (L₁ ++ L₂) p r

Chains compose end to end.

theorem Schoenflies.IsChainFrom.isClosedChain_append {p q : Plane} {L₁ L₂ : List Piece} (h₁ : IsChainFrom L₁ p q) (h₂ : IsChainFrom L₂ p q) : IsClosedChain (L₁ ++ L₂)

Two chains with the same two ends close up. This is the whole reason Aᵢ ∪ P is a closed curve as far as the crossing count is concerned.

theorem Schoenflies.SameEdges.isChainFrom {p q : Plane} {L₁ L₂ : List Piece} (h : SameEdges L₁ L₂) (h₂ : IsChainFrom L₂ p q) : IsChainFrom L₁ p q

theorem Schoenflies.SameEdges.isClosedChain {L₁ L₂ : List Piece} (h : SameEdges L₁ L₂) (h₂ : IsClosedChain L₂) : IsClosedChain L₁

The edges of a polyline

How a crosscut is normally presented: a list of points. pathPieces reads off its edges, and isChainFrom_pathPieces says its boundary is the two ends of the list.

def Schoenflies.pathPieces : List Plane → List Piece

The edges of the polyline v₀, v₁, …, v_k.

Equations

• Schoenflies.pathPieces [] = []
• Schoenflies.pathPieces [head] = []
• Schoenflies.pathPieces (v :: w :: rest) = (v, w) :: Schoenflies.pathPieces (w :: rest)

@[simp]

theorem Schoenflies.pathPieces_nil : pathPieces [] = []

@[simp]

theorem Schoenflies.pathPieces_singleton (v : Plane) : pathPieces [v] = []

@[simp]

theorem Schoenflies.pathPieces_cons_cons (v w : Plane) (rest : List Plane) : pathPieces (v :: w :: rest) = (v, w) :: pathPieces (w :: rest)

theorem Schoenflies.isChainFrom_pathPieces (p : Plane) (mid : List Plane) (q : Plane) : IsChainFrom (pathPieces (p :: (mid ++ [q]))) p q

A polyline is a chain from its first point to its last.

theorem Schoenflies.cover_pathPieces (p : Plane) (mid : List Plane) (q : Plane) : cover (pathPieces (p :: (mid ++ [q]))) = poly (p :: (mid ++ [q]))

The edges of a polyline occupy the polyline.

The two arcs of a polygon

arcPieces C a k is the edge list of the arc of C that leaves vertex a and runs forward through k edges. Its two ends are vertices a and a + k, and for k ≤ m + 3 the two arcs arcPieces C a k and arcPieces C (a + k) (m + 3 - k) between them use each edge of C exactly once.

def Schoenflies.ClosedPolygon.arcPieces {m : ℕ} (C : ClosedPolygon m) (a : ZMod (m + 3)) (k : ℕ) : List Piece

The edge list of the arc of C that leaves vertex a and runs forward through k edges. For k ≤ m + 3 this is one of the two arcs a crosscut with endpoints C.vertex a and C.vertex (a + k) cuts C into; the other is arcPieces C (a + k) (m + 3 - k).

Equations

• C.arcPieces a k = List.map (fun (t : ℕ) => (C.vertex (a + ↑t), C.vertex (a + ↑t + 1))) (List.range k)

@[simp]

theorem Schoenflies.ClosedPolygon.arcPieces_zero {m : ℕ} (C : ClosedPolygon m) (a : ZMod (m + 3)) : C.arcPieces a 0 = []

theorem Schoenflies.ClosedPolygon.arcPieces_add {m : ℕ} (C : ClosedPolygon m) (a : ZMod (m + 3)) (k l : ℕ) : C.arcPieces a (k + l) = C.arcPieces a k ++ C.arcPieces (a + ↑k) l

Running through k + l edges is running through k and then through l.

theorem Schoenflies.ClosedPolygon.arcPieces_full {m : ℕ} (C : ClosedPolygon m) : C.arcPieces 0 (m + 3) = C.pieces

Running through all m + 3 edges from vertex 0 is the whole edge list.

theorem Schoenflies.ClosedPolygon.mem_pieces_of_mem_arcPieces {m : ℕ} {C : ClosedPolygon m} {a : ZMod (m + 3)} {k : ℕ} {Q : Piece} (hQ : Q ∈ C.arcPieces a k) : Q ∈ C.pieces

Every edge of an arc is an edge of the polygon; non-levelness and nondegeneracy follow.

theorem Schoenflies.ClosedPolygon.arcPieces_nondeg {m : ℕ} (C : ClosedPolygon m) (a : ZMod (m + 3)) (k : ℕ) (Q : Piece) : Q ∈ C.arcPieces a k → Q.Nondeg

theorem Schoenflies.ClosedPolygon.arcPieces_hgt_ne {u : Plane} {m : ℕ} {C : ClosedPolygon m} {a : ZMod (m + 3)} {k : ℕ} (hL : ∀ Q ∈ C.pieces, hgt u Q.1 ≠ hgt u Q.2) (Q : Piece) : Q ∈ C.arcPieces a k → hgt u Q.1 ≠ hgt u Q.2

theorem Schoenflies.ClosedPolygon.isChainFrom_arcPieces {m : ℕ} (C : ClosedPolygon m) (a : ZMod (m + 3)) (k : ℕ) : IsChainFrom (C.arcPieces a k) (C.vertex a) (C.vertex (a + ↑k))

An arc is a chain from its first vertex to its last. The telescoping sum of the blueprint's "counting edge by edge", read off Schoenflies.sum_range_boundary.

theorem Schoenflies.ClosedPolygon.arcPieces_full_perm {m : ℕ} (C : ClosedPolygon m) (a : ZMod (m + 3)) : (C.arcPieces a (m + 3)).Perm C.pieces

The two arcs from a vertex use every edge exactly once. Cutting the cycle at a is a rotation, and a rotation is a permutation: the list is X ++ Y and C.pieces is Y ++ X.

theorem Schoenflies.ClosedPolygon.arcPieces_split_perm {m k : ℕ} (C : ClosedPolygon m) (a : ZMod (m + 3)) (hk : k ≤ m + 3) : (C.arcPieces a k ++ C.arcPieces (a + ↑k) (m + 3 - k)).Perm C.pieces

The split. For k ≤ m + 3 the two arcs at a and a + k between them use every edge of C exactly once.

theorem Schoenflies.ClosedPolygon.sameEdges_arcPieces_split {m k : ℕ} (C : ClosedPolygon m) (a : ZMod (m + 3)) (hk : k ≤ m + 3) : SameEdges C.pieces (C.arcPieces a k ++ C.arcPieces (a + ↑k) (m + 3 - k))

theorem Schoenflies.ClosedPolygon.cover_arcPieces_union {m k : ℕ} (C : ClosedPolygon m) (a : ZMod (m + 3)) (hk : k ≤ m + 3) : cover (C.arcPieces a k) ∪ cover (C.arcPieces (a + ↑k) (m + 3 - k)) = C.carrier

The two arcs between them carry the polygon.

theorem Schoenflies.ClosedPolygon.cover_arcPieces_subset {m : ℕ} (C : ClosedPolygon m) (a : ZMod (m + 3)) (k : ℕ) : cover (C.arcPieces a k) ⊆ C.carrier

theorem Schoenflies.ClosedPolygon.isClosedChain_arcPieces_append {m : ℕ} {C : ClosedPolygon m} {a : ZMod (m + 3)} {k : ℕ} {K : List Piece} (hK : IsChainFrom K (C.vertex a) (C.vertex (a + ↑k))) : IsClosedChain (C.arcPieces a k ++ K)

The two curves of the split are closed chains. An arc from C.vertex a to C.vertex (a + k) and a crosscut with the same two ends close up.

theorem Schoenflies.ClosedPolygon.arcPieces_append_hgt_ne {u : Plane} {m : ℕ} {C : ClosedPolygon m} {a : ZMod (m + 3)} {k : ℕ} {K : List Piece} (hC : ∀ Q ∈ C.pieces, hgt u Q.1 ≠ hgt u Q.2) (hK : ∀ Q ∈ K, hgt u Q.1 ≠ hgt u Q.2) (Q : Piece) : Q ∈ C.arcPieces a k ++ K → hgt u Q.1 ≠ hgt u Q.2

theorem Schoenflies.ClosedPolygon.carrier_eq_of_sameEdges {m : ℕ} {C : ClosedPolygon m} {a : ZMod (m + 3)} {k m' : ℕ} {J : ClosedPolygon m'} {K : List Piece} (h : SameEdges J.pieces (C.arcPieces a k ++ K)) : J.carrier = cover (C.arcPieces a k) ∪ cover K

A curve of the split occupies its arc together with the crosscut. Only the edge list of J is assumed related to the split; its carrier then is what the blueprint calls Aᵢ ∪ P.

theorem Schoenflies.ClosedPolygon.notMem_carrier_of_sameEdges {m : ℕ} {C : ClosedPolygon m} {a : ZMod (m + 3)} {k m' : ℕ} {J : ClosedPolygon m'} {K : List Piece} (h : SameEdges J.pieces (C.arcPieces a k ++ K)) {x : Plane} (hxC : x ∉ C.carrier) (hxK : x ∉ cover K) : x ∉ J.carrier

Hence a point off C and off the crosscut is off J: the blueprint's "a point of Int(C) off P" needs nothing else.

The identity

Everything above was the definition. The identity itself is one line of ZMod 2 arithmetic: the crosscut is counted once in each of π_{J₁} and π_{J₂}, so its contribution cancels.

theorem Schoenflies.parity_split {L₁ L₂ : List Piece} (u : Plane) {LC A₁ A₂ K : List Piece} (hC : SameEdges LC (A₁ ++ A₂)) (h₁ : SameEdges L₁ (A₁ ++ K)) (h₂ : SameEdges L₂ (A₂ ++ K)) (q : Plane) : parity u L₁ q + parity u L₂ q = parity u LC q

Parity splitting (Lemma 2.7), in edge-list form and with no geometry whatever. If the edge list of C is the two arcs A₁, A₂ and the edge list of Jᵢ is Aᵢ together with the crosscut's list K — in each case up to reordering and up to reversing individual edges — then π_{J₁} + π_{J₂} = π_C at every point of the plane.

The hypotheses carry all of the blueprint's picture; the proof is that K is counted twice.

theorem Schoenflies.ClosedPolygon.parity_splitting {L₁ L₂ : List Piece} {m k : ℕ} (C : ClosedPolygon m) (u : Plane) (a : ZMod (m + 3)) (hk : k ≤ m + 3) {K : List Piece} (h₁ : SameEdges L₁ (C.arcPieces a k ++ K)) (h₂ : SameEdges L₂ (C.arcPieces (a + ↑k) (m + 3 - k) ++ K)) (q : Plane) : parity u L₁ q + parity u L₂ q = parity u C.pieces q

Parity splitting (Lemma 2.7) for a simple closed polygon cut at two of its vertices. K is the edge list of the crosscut, L₁ and L₂ the edge lists of the two curves Jᵢ = Aᵢ ∪ P; each is required only to carry the right edges, in any order and with either name for each edge.

No hypothesis on K is needed: whatever it is, it is counted once on each side and cancels.

What the identity says about the regions

Theorem 2.3 fixes the two values of π for each of the three curves — 1 on the bounded region, 0 on the unbounded one — and the identity then reads off the blueprint's "consequently".

theorem Schoenflies.ClosedPolygon.parity_eq_one_iff {m : ℕ} (C : ClosedPolygon m) {u : Plane} (hu : u.IsDirection) (hL : ∀ Q ∈ C.pieces, hgt u Q.1 ≠ hgt u Q.2) {x : Plane} (hx : x ∉ C.carrier) : parity u C.pieces x = 1 ↔ x ∈ inside C.carrier

The crossing count decides the region (Theorem 2.3, last sentence, as a criterion). Off the polygon, π_C = 1 exactly on the bounded region.

theorem Schoenflies.ClosedPolygon.crosscut_inside_exactly_one {m : ℕ} {a : ZMod (m + 3)} {k m₁ m₂ : ℕ} (C : ClosedPolygon m) (J₁ : ClosedPolygon m₁) (J₂ : ClosedPolygon m₂) {u : Plane} (hu : u.IsDirection) (hC : ∀ Q ∈ C.pieces, hgt u Q.1 ≠ hgt u Q.2) {K : List Piece} (hK : ∀ Q ∈ K, hgt u Q.1 ≠ hgt u Q.2) (hk : k ≤ m + 3) (h₁ : SameEdges J₁.pieces (C.arcPieces a k ++ K)) (h₂ : SameEdges J₂.pieces (C.arcPieces (a + ↑k) (m + 3 - k) ++ K)) {x : Plane} (hx : x ∈ inside C.carrier) (hxK : x ∉ cover K) : x ∈ inside J₁.carrier ↔ x ∉ inside J₂.carrier

A point inside C and off the crosscut is inside exactly one of J₁, J₂ — the first half of the "Consequently" of Lemma 2.7. The left side of the splitting identity is 1, so exactly one of the two right-hand terms is.

"Off the crosscut" is x ∉ cover K; that x is off J₁ and off J₂ as well is not assumed but derived, by notMem_carrier_of_sameEdges.

theorem Schoenflies.ClosedPolygon.crosscut_outside_agree {m : ℕ} {a : ZMod (m + 3)} {k m₁ m₂ : ℕ} (C : ClosedPolygon m) (J₁ : ClosedPolygon m₁) (J₂ : ClosedPolygon m₂) {u : Plane} (hu : u.IsDirection) (hC : ∀ Q ∈ C.pieces, hgt u Q.1 ≠ hgt u Q.2) {K : List Piece} (hK : ∀ Q ∈ K, hgt u Q.1 ≠ hgt u Q.2) (hk : k ≤ m + 3) (h₁ : SameEdges J₁.pieces (C.arcPieces a k ++ K)) (h₂ : SameEdges J₂.pieces (C.arcPieces (a + ↑k) (m + 3 - k) ++ K)) {x : Plane} (hx : x ∈ outside C.carrier) (hxK : x ∉ cover K) : x ∈ inside J₁.carrier ↔ x ∈ inside J₂.carrier

A point outside C and off the crosscut is inside both of J₁, J₂ or inside neither — the second half of the "Consequently" of Lemma 2.7. The left side of the splitting identity is 0, so the two right-hand terms agree.