Composition checks

Each layer of this development was built against an interface rather than against its consumer, so the interfaces can drift apart while every module still compiles on its own. These are the checks that they actually fit: short theorems that use two or more layers together and are worth nothing except as a tripwire.

The first one has already earned its place. polygonal_overlay originally concluded only IsDrawing G segmentDrawing ∧ pointSet G segmentDrawing = cover pieces, with G bound by an existential. Every statement about faces carries a [G.Finite] instance, and there is no way to recover an instance for a graph hidden behind a binder — so the overlay could not be handed to the face machinery at all, even though both halves compiled. The overlay now carries Graph.Finite in its conclusion, and this file is what would have caught that.

What is checked

• overlay_has_outer_face — Layer 6's overlay composes with Layer 6's outer face.
• two_arcs_roundtrip — Layer 4's cutting theorem composes with its gluing theorem.
• polygonal_collar — Lemma 1.8 (a), the three strip modules composed.

theorem Schoenflies.overlay_has_outer_face (pieces : List Piece) (hnd : ∀ P ∈ pieces, P.Nondeg) : ∃ (G : Graph Plane Piece), G.pointSet segmentDrawing = cover pieces ∧ ∃ base ∈ G.exterior segmentDrawing, ¬Bornology.IsBounded (G.face segmentDrawing base)

The overlay of finitely many nondegenerate segments is a plane graph to which the outer-face theorem applies. Uses polygonal_overlay, Graph.Finite, IsDrawing, face and exists_unbounded_face together.

theorem Schoenflies.two_arcs_roundtrip {C : Set Plane} (hC : IsJordanCurve C) {p q : Plane} (hp : p ∈ C) (hq : q ∈ C) (hpq : p ≠ q) : ∃ (A : Set Plane) (B : Set Plane), A ∪ B = C ∧ IsJordanCurve (A ∪ B)

Cutting a Jordan curve at two points and gluing the pieces back returns a Jordan curve — IsJordanCurve.two_arcs composed with IsJordanCurve.of_two_arcs. The two are converse, and this is what says so.

theorem Schoenflies.polygonal_collar {m : ℕ} (P : ClosedPolygon m) {U : Set Plane} (hU : IsOpen U) (hPU : P.carrier ⊆ U) : ∃ (N : Set Plane) (L : Set Plane) (R : Set Plane), IsOpen N ∧ P.carrier ⊆ N ∧ N ⊆ U ∧ IsOpen L ∧ IsOpen R ∧ N \ P.carrier = L ∪ R ∧ Disjoint L R ∧ IsConnected L ∧ IsConnected R

Lemma 1.8 (a) (two-sided polygonal strips). A simple closed polygonal curve has an open neighbourhood N, inside any prescribed open set containing it, such that N minus the curve is the disjoint union of two connected open sets.

This is Strip.lean (the apparatus, the germ argument and the disjointness), StripConstants.lean (the constants exist) and StripConnected.lean (each side is connected, and the collar minus the curve is exactly the two sides) composed. It is stated here rather than in any one of them because no one of them can state it.

IsOpen N and P.carrier ⊆ N are not decoration: without them "neighbourhood" is not being asserted at all, and the Jordan curve argument needs N to be a neighbourhood of the curve — it has to land the final portion of a segment [x, a) inside N. An earlier version of this statement omitted both and was correspondingly useless to its consumer.

ClosedPolygon.exists_two_sided_collar strengthens this further with the local clauses: every point of the curve lies in the closure of both sides.