The realisation of a cycle is a Jordan curve #
A cycle of a plane graph arrives as Schoenflies/Graph/Cycle.lean presents it: an edge, and a
path between that edge's two ends which does not use it. Its realisation is the set of points
the arcs of those edges occupy, and the claim is that this set is a Jordan curve.
The argument is set-level; no parametrisation of a walk is built #
The obvious approach — a walkArc definition folding Schoenflies.concatenate along the edge
list — is the wrong shape twice over. The empty-list base case is a constant map, which is
not an arc, so the fold cannot be shown injective at the last step; and threading a
parametrisation through the induction buys nothing, since every consumer wants the point set.
Instead the existence of the arc is what the induction carries, in
Schoenflies.IsArcBetween. The arcs are chosen inside the induction and the concatenation of
them is chosen by the gluing theorem; no parametrisation is ever named.
Where the geometry enters #
Exactly once, in Graph.IsDrawing.first_edge_meets_rest: a common point of the first edge's
arc and the rest of the path is a vertex incident with both edges
(Graph.IsDrawing.arcs_meet_at_vertex), hence one of the two ends of the first edge, and the
path's own freshness clause — the vertex a step departs from is not one the rest visits —
forbids it being the source. Taking the same edge again is refused by the same clause, so a
separate "the edges of a path are distinct" lemma is not needed.
Loops #
Nothing here hypothesises looplessness, and nothing needs to: Graph.IsDrawing.ne_of_isLink
derives it. An edge with equal ends would be drawn by an arc whose parametrisation takes the
same value at 0 and at 1, which its injectivity forbids. That is what rules out the
degenerate cycle Graph.liesOnCycle_of_isLoopAt — a loop with an empty detour — whose
realisation is a single arc and not a Jordan curve.
Blueprint #
Graph.edgesCover— what a list of edges occupies.Graph.pointSetis the vertices together with this, taken over all the edges of the graph.Graph.IsDrawing.path_isArcBetween— the realisation of a path is an arc between its two ends.Graph.IsDrawing.cycle_isJordanCurve— §"Plane graphs and the utility graph": "in a plane graph the realization of a cycle is a Jordan curve: its edges are simple arcs with pairwise disjoint interiors, and consecutive edges meet exactly at their shared vertices, so the edge arcs concatenate injectively into a simple closed curve".Graph.IsDrawing.cycle_inter— the meeting condition in full: the detour and the edge meet in exactly the edge's two ends.Schoenflies.IsJordanCurve.of_two_arcsconsumes only one inclusion of it, but the equality is what the blueprint asserts.
What a list of edges occupies #
The point set of a list of edges: the union of their edge arcs. A walk is a list of edges, so this is what a walk of a plane graph draws.
Equations
- Graph.edgesCover drawing W = ⋃ e ∈ W, Graph.edgeArc drawing e
Instances For
A list of edges of the graph occupies part of what the graph occupies.
A plane graph has no loops #
This is not a hypothesis anywhere in this file; it is a consequence of the drawing condition, and it is what makes the degenerate cycle — a loop, with the empty path back — impossible.
An edge of a plane graph has two distinct ends. An edge with equal ends would be drawn by an arc whose parametrisation returns to its start, which its injectivity forbids.
The realisation of a path #
The induction carries the existence of an arc, not a parametrisation. Its one geometric
step is Graph.IsDrawing.first_edge_meets_rest.
The first edge's arc meets the rest of the path only at the waypoint. Two cases, and
neither is geometric beyond the workhorse Graph.IsDrawing.arcs_meet_at_vertex: if the rest
takes the same edge again, the source is one of its ends; if it takes a different one, a
common point is a vertex incident with both, so it is the source or the waypoint. Either way a
point that was the source would put the source among the vertices the rest visits, which is
what the path's freshness clause forbids.
The realisation of a path is an arc between its two ends. The path must go somewhere: the empty path draws the empty set, which is not an arc.
The induction is on the path, at the source end, and what it carries is the existence of the
arc. At each step the first edge's arc and the rest's arc meet only at the waypoint
(Graph.IsDrawing.first_edge_meets_rest), so Schoenflies.IsArcBetween.concatenate glues
them.
The realisation of a cycle #
The detour of a cycle is a path with at least one edge — an empty detour would return to where it set out, and the edge it is a detour for has two distinct ends — so it is drawn by an arc between those ends.
The detour of a cycle meets the edge only at the edge's two ends. A common point lies on the edge and on some edge of the detour, which the detour does not contain, so it is a vertex incident with the edge — and an edge has only its two ends.
The detour and the edge meet in exactly the edge's two ends. The inclusion
Graph.IsDrawing.detour_meets_edge is what Schoenflies.IsJordanCurve.of_two_arcs consumes;
the reverse one is free, since both ends are endpoints of both arcs.
The realisation of a cycle is a Jordan curve. The detour is drawn by an arc from one
end of the edge to the other, the edge is drawn by an arc back, and the two meet only at those
two ends, so Schoenflies.IsJordanCurve.of_two_arcs closes the loop.
The source of a nonempty walk lies on what the walk draws.
A walk of a polygonal plane graph draws a polygonal set. Consecutive edges share the vertex between them, so the union stays a single vertex list.