lem:skeleton-crosscuts: a crosscut inside one stage of the skeleton #
Two anchors lying in a common finite stage are joined by a polygonal crosscut of the Jordan
domain that lies in that stage's skeleton (jordan_schoenflies.tex 2857-2872). This file
proves the first clause, for the source side.
Everything here concerns one finite plane graph: a stage is a
finite plane graph whose point set carries the Jordan curve C as its outer boundary
(Graph.IsStageOn), and nothing below mentions the sequence of stages that produces it.
The blueprint's proof splits on whether some nonboundary edge — one whose arc is not
contained in C — has both of its ends on C. If one does, its open interior is a whole
component of the open nonboundary part, so it is the only nonboundary edge and is itself the
crosscut. Otherwise every nonboundary edge meeting C has its other end inside, and the
interior subgraph interiorPart is connected because the half-open attached edges partition
the open nonboundary part into relatively clopen pieces.
What is here, and what is not #
This module was written in one sitting that ended early, and it stops after the source-side
crosscut. The rest of the section — the target crosscut of clause 2,
lem:crosscut-side-correspondence, prop:boundary-continuity, and the assembly of
thm:square-extension — is in Schoenflies/BoundaryContinuity2.lean, which imports this one.
An earlier version of this docstring listed those as if they were here; they never were.
Blueprint #
Graph.IsStageOn— a finite plane graph carryingCas its outer boundary.Graph.Nonboundary,Graph.interiorPart,Graph.attachEdges,Graph.isPreconnected_interiorPart— the interior subgraph and its connectedness, which is the substance of the second case.Graph.IsStageOn.exists_crosscut—lem:skeleton-crosscuts, clause 1: the source-side polygonal crosscut between two prescribed points ofCthat the stage joins. Clause 2, the target crosscut, is inSchoenflies/BoundaryContinuity2.lean.
lem:skeleton-crosscuts #
A stage of the skeleton is a finite plane graph whose point set carries the Jordan curve C as
its outer boundary. The blueprint's proof splits on whether some nonboundary edge — an edge
whose arc is not contained in C — has both of its ends on C.
Everything in this section speaks about one finite plane graph and never about the stages that produce it.
An edge is nonboundary when its arc is not contained in the outer boundary.
Equations
- Graph.Nonboundary drawing C e = ¬Graph.edgeArc drawing e ⊆ C
Instances For
One finite stage of the skeleton, as lem:skeleton-crosscuts uses it.
C is the outer boundary and D the region it bounds. The two substantive clauses are
edge_split — every edge either runs inside C or has all of its non-endpoint points in D —
and isConnected_diff, the admissibility hypothesis that the open nonboundary part
|Γ| ∖ C is connected.
D is an arbitrary set disjoint from C, not Schoenflies.inside C: the proof uses nothing
about it, and the consumer instantiates it with the Jordan domain.
- isDrawing : G.IsDrawing drawing
the graph is drawn in the plane
- polygonal ⦃e : β⦄ : e ∈ G.edgeSet → Nonboundary drawing C e → Schoenflies.IsPolygonal (edgeArc drawing e)
every nonboundary edge is drawn as a polygonal arc.
Only the nonboundary edges:
def:admissible-graphsays "its edges not contained inCare polygonal arcs", and for a source stage that restriction is not a convenience but a necessity. The outer edges of a source stage are subarcs of the wild Jordan curveC, which is in general nowhere polygonal, so a field askingIsPolygonalof every edge would makeIsStageOnunsatisfiable for exactly the graphslem:skeleton-crosscutsis about. It was stated that way and is repaired here; both proofs below already applied it only to nonboundary edges. - disjoint : Disjoint C D
the outer boundary and the region it bounds are disjoint
- vertex_mem ⦃v : Schoenflies.Plane⦄ : v ∈ G.vertexSet → v ∉ C → v ∈ D
a vertex off the outer boundary lies in the region
- edge_split ⦃e : β⦄ ⦃x y : Schoenflies.Plane⦄ : G.IsLink e x y → edgeArc drawing e ⊆ C ∨ edgeArc drawing e \ {x, y} ⊆ D
an edge either lies on the outer boundary or has its interior in the region
- isConnected_diff : IsConnected (G.pointSet drawing \ C)
admissibility: the open nonboundary part is connected
Instances For
Off the outer boundary, the point set of the stage lies in the region. This is the reading
of edge_split and vertex_mem the crosscut extraction needs.
On a nonboundary edge the outer boundary is met only at the two ends.
The two ends of an edge lie on its arc.
A nonboundary edge whose two ends lie in the region runs entirely inside it.
Case 1: a nonboundary edge with both ends on the outer boundary #
Its open interior e° is a connected component of X = |Γ| ∖ C, because an edge interior
meets the rest of the graph only at its endpoints, and those endpoints have been removed. Hence
X = e°, and there is then only one nonboundary edge.
Case 1, first half. If a nonboundary edge e has both ends on C, the whole open
nonboundary part lies on e.
The proof is lem:clopen-component in the closed-set form: edgeArc e and the rest of the
drawing are two closed sets covering the point set whose common part misses X.
Case 1, second half. With X reduced to one edge interior there is only one nonboundary
edge, so the two prescribed boundary points are exactly the ends of e.
Case 2: the interior subgraph #
Let Λ be the finite subgraph consisting of all vertices in D and all edges whose two
endpoints lie in D, allowing isolated interior vertices. Only its point set is ever needed,
so interiorPart is that set rather than a Graph.
The point set of the blueprint's interior subgraph Λ: the vertices lying in the region,
together with the edges that run entirely inside it.
Equations
- G.interiorPart drawing D = G.vertexSet ∩ D ∪ ⋃ e ∈ {e : β | e ∈ G.edgeSet ∧ Graph.edgeArc drawing e ⊆ D}, Graph.edgeArc drawing e
Instances For
The union of a subset of Λ with the closed edges meeting it. The blueprint attaches the
half-open edges; taking the whole closed edge instead gives a set that is closed in the
plane, and intersecting back with X = |Γ| ∖ C recovers the blueprint's set, because the
removed ends are exactly the points of those edges lying on C.
Equations
- G.attachEdges drawing S = S ∪ ⋃ e ∈ {e : β | e ∈ G.edgeSet ∧ (Graph.edgeArc drawing e ∩ S).Nonempty}, Graph.edgeArc drawing e
Instances For
A half edge — a nonboundary edge with exactly one end on C — meets Λ only in its
other end. This is what makes the attached pieces of X half-open.
The selection step. If Λ is split into two disjoint closed pieces S, S' and an
edge meets S, then everything that edge shares with Λ lies in S.
An edge running inside D is connected and contained in S ∪ S', so it lies in one piece; a
half edge meets Λ in a single point.
Case 2, the connectedness of Λ. For each component L of |Λ|, the union of L
with all half-open edges attached to vertices of L is both open and closed in X; these sets
partition X. Connectedness of X therefore implies that |Λ| is connected.
lem:skeleton-crosscuts #
lem:skeleton-crosscuts. Two distinct points of the outer boundary, each incident with
a nonboundary edge of the stage, are joined by a polygonal crosscut lying in the stage's
skeleton: a simple polygonal arc between them meeting C only at its two ends.
In case 1 the crosscut is a single edge; in case 2 it is extracted from
Y = e_a ∪ |Λ| ∪ e_b by lem:finite-polygonal-union
(Schoenflies.exists_crosscut_arc_of_biUnion_finite).