The vertex squares, the last parameter inside a closed set, and the cores

Three of the ordinary bricks of the polygonal redrawing of a finite plane graph.

The vertex squares. Around each vertex of a finite plane graph sits a closed axis-parallel square which meets no other vertex and no edge arc of an edge not incident with that vertex. One compact separation per other vertex and per non-incident arc, then the single-ε-for-all lemma of Schoenflies/UniformBound.lean. Squares rather than disks because the assembly needs the boundary to be made of segments; convexity, which the radial segments of the last step want, both shapes have.

Because the choice is made once for all vertices rather than vertex by vertex, halving the common radius also makes distinct squares disjoint — which the cores of the next brick need and which the per-vertex statement does not give. That is why exists_vertexSquares is the form to consume and exists_square_at only its ingredient.

The last parameter inside a closed set. The parameters at which an arc lies in a closed set form a compact subset of the parameter interval; if it is nonempty its supremum is attained, and past that supremum the arc has left the set for good. The mirror statement about the infimum is what the far end of an edge wants: the arc leaves the square at v for the last time and enters the square at w for the first time.

The cores. The subarc of an edge between those two parameters. It meets the square at v in its own first endpoint only, the square at w in its own last endpoint only, and — the clause the assembly really uses — it contains no vertex, which makes distinct cores disjoint without any further estimate.

Blueprint

Bricks B2, B3 and B4 of lem:polygonal-redrawing.

• Plane.closedBall_subset_closedSquare, Plane.closedSquare_subset_ball — a square sits inside a ball and vice versa, the comparison every separation argument passes through.
• Plane.supDist_triangle, Plane.closedSquare_mono_center, Plane.mem_closedSquare_self — square arithmetic missing from Schoenflies/Square.lean.
• exists_last_mem_Icc, exists_first_mem_Icc, exists_last_mem, exists_first_mem — B3, with isCompact_parameters_mem behind them.
• Graph.IsDrawing.exists_square_at — B2 at one vertex.
• Graph.IsDrawing.exists_vertexSquares — B2 as consumed: one radius for every vertex, with distinct squares disjoint.
• Graph.IsDrawing.exists_core — B4, the core of one edge.
• Graph.IsDrawing.disjoint_of_subset_edgeArc — B4's "distinct cores are disjoint".
• Graph.IsDrawing.closedSquare_disjoint_edgeArc_of_ne — B4's "meets no other vertex square", which is a property of the whole arc.

Square arithmetic

Schoenflies/Square.lean has convexity, openness and closedness of closedSquare but no triangle inequality for supDist and no monotonicity at a general centre; both are needed here.

theorem Schoenflies.Plane.closedSquare_mono_center (c : Plane) {r s : ℝ} (h : r ≤ s) : c.closedSquare r ⊆ c.closedSquare s

Squares about a common centre grow with the radius. Bounded.closedSquare_mono says this only about the origin.

theorem Schoenflies.Plane.mem_closedSquare_self (c : Plane) {r : ℝ} (hr : 0 ≤ r) : c ∈ c.closedSquare r

The centre lies in its own square.

theorem Schoenflies.Plane.supDist_eq_dist_le (x c : Plane) : x.supDist c ≤ dist x c

theorem Schoenflies.Plane.closedBall_subset_closedSquare (c : Plane) (r : ℝ) : Metric.closedBall c r ⊆ c.closedSquare r

The inscribed ball: a ball is inside the square of the same radius, since the sup norm is at most the Euclidean norm.

theorem Schoenflies.Plane.closedSquare_subset_ball {c : Plane} {ρ : ℝ} (hρ : 0 < ρ) : c.closedSquare (ρ / 2) ⊆ Metric.ball c ρ

The circumscribed ball, in the form the separations want: a square of half a given radius sits inside the open ball of that radius, because √2 < 2.

B3 — the last point of an arc inside a closed set

theorem Schoenflies.isCompact_parameters_mem {f : ℝ → Plane} {α β : ℝ} (hf : ContinuousOn f (Set.Icc α β)) {C : Set Plane} (hC : IsClosed C) : IsCompact {t : ℝ | t ∈ Set.Icc α β ∧ f t ∈ C}

The parameters at which a curve lies in a closed set form a compact subset of the parameter interval: the parametrisation is continuous there and the interval is compact.

Stated over an arbitrary Icc and not only over [0, 1], because the second use of B3 — the first entry into the far vertex's square — has to happen after the last exit from the near one, i.e. on the interval [a, 1].

theorem Schoenflies.exists_last_mem_Icc {f : ℝ → Plane} {α β : ℝ} (hf : ContinuousOn f (Set.Icc α β)) {C : Set Plane} (hC : IsClosed C) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Icc α β) (hmem : f t₀ ∈ C) : ∃ s ∈ Set.Icc α β, t₀ ≤ s ∧ f s ∈ C ∧ ∀ t ∈ Set.Icc α β, s < t → f t ∉ C

The last parameter inside a closed set. Given one parameter whose point lies in C, there is a largest one: the curve is in C there, and at every larger parameter of the interval it has left C for good.

This is the supremum of a nonempty compact set of parameters, which is therefore attained.

theorem Schoenflies.exists_first_mem_Icc {f : ℝ → Plane} {α β : ℝ} (hf : ContinuousOn f (Set.Icc α β)) {C : Set Plane} (hC : IsClosed C) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Icc α β) (hmem : f t₀ ∈ C) : ∃ s ∈ Set.Icc α β, s ≤ t₀ ∧ f s ∈ C ∧ ∀ t ∈ Set.Icc α β, t < s → f t ∉ C

The mirror of exists_last_mem_Icc: the first parameter inside a closed set. Before it the curve has not yet reached C.

theorem Schoenflies.exists_last_mem {f : ℝ → Plane} (hf : ContinuousOn f unitInterval) {C : Set Plane} (hC : IsClosed C) {t₀ : ℝ} (ht₀ : t₀ ∈ unitInterval) (hmem : f t₀ ∈ C) : ∃ s ∈ unitInterval, t₀ ≤ s ∧ f s ∈ C ∧ ∀ t ∈ unitInterval, s < t → f t ∉ C

B3 on the unit interval: the last parameter at which an arc is inside a closed set.

theorem Schoenflies.exists_first_mem {f : ℝ → Plane} (hf : ContinuousOn f unitInterval) {C : Set Plane} (hC : IsClosed C) {t₀ : ℝ} (ht₀ : t₀ ∈ unitInterval) (hmem : f t₀ ∈ C) : ∃ s ∈ unitInterval, s ≤ t₀ ∧ f s ∈ C ∧ ∀ t ∈ unitInterval, t < s → f t ∉ C

B3 on the unit interval, at the other end: the first parameter at which an arc is inside a closed set.

B2 — the vertex squares

theorem Graph.IsDrawing.notMem_edgeArc_of_not_inc {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsDrawing drawing) {e : β} (he : e ∈ G.edgeSet) {v : Schoenflies.Plane} (hv : v ∈ G.vertexSet) (hinc : ¬G.Inc e v) : v ∉ edgeArc drawing e

A vertex lies on no arc of an edge it is not incident with: the arc meets the vertex set only at its own two ends, and those are the vertices it is incident with.

theorem Graph.IsDrawing.exists_square_at {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} [G.Finite] (h : G.IsDrawing drawing) {v : Schoenflies.Plane} (hv : v ∈ G.vertexSet) : ∃ r > 0, (∀ w ∈ G.vertexSet, w ≠ v → w ∉ v.closedSquare r) ∧ ∀ e ∈ G.edgeSet, ¬G.Inc e v → Disjoint (v.closedSquare r) (edgeArc drawing e)

B2 at a single vertex: a closed square about v meeting no other vertex and no arc of an edge not incident with v.

The two families are separated the same way — one compact separation each, then the common positive bound of exists_pos_forall_of_finite — and the two radii are then merged by taking the smaller, which is legitimate because shrinking a square preserves "meets nothing".

theorem Graph.IsDrawing.exists_vertexSquares {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} [G.Finite] (h : G.IsDrawing drawing) : ∃ r > 0, (∀ v ∈ G.vertexSet, ∀ w ∈ G.vertexSet, w ≠ v → w ∉ v.closedSquare r) ∧ (∀ v ∈ G.vertexSet, ∀ e ∈ G.edgeSet, ¬G.Inc e v → Disjoint (v.closedSquare r) (edgeArc drawing e)) ∧ ∀ v ∈ G.vertexSet, ∀ w ∈ G.vertexSet, v ≠ w → Disjoint (v.closedSquare r) (w.closedSquare r)

B2 as its consumers want it: one radius serving every vertex at once, with the squares about distinct vertices disjoint.

Disjointness is not a consequence of the per-vertex statement — a square about v avoiding w says nothing about a square about w reaching towards v. It comes from choosing the radius once for all vertices and then halving it: two squares of radius r that met would put their centres within 2r in the sup metric, i.e. each centre in the other's square of radius 2r, which the unhalved choice forbids.

B4 — the cores

theorem Graph.not_inc_of_ne {β : Type u_1} {G : Graph Schoenflies.Plane β} {e : β} {v w u : Schoenflies.Plane} (hlink : G.IsLink e v w) (huv : u ≠ v) (huw : u ≠ w) : ¬G.Inc e u

An edge is incident only with its own two ends.

theorem Graph.IsDrawing.closedSquare_disjoint_edgeArc_of_ne {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {e : β} {v w u : Schoenflies.Plane} {r : ℝ} (hsq : ∀ e ∈ G.edgeSet, ¬G.Inc e u → Disjoint (u.closedSquare r) (edgeArc drawing e)) (hlink : G.IsLink e v w) (huv : u ≠ v) (huw : u ≠ w) : Disjoint (u.closedSquare r) (edgeArc drawing e)

"The core meets no other vertex square" is really a statement about the whole arc: the square about a vertex which is neither end of the edge misses the edge's arc entirely, by B2. The hypothesis is exactly the second clause of exists_vertexSquares.

theorem Graph.IsDrawing.disjoint_of_subset_edgeArc {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsDrawing drawing) {e f : β} (he : e ∈ G.edgeSet) (hf : f ∈ G.edgeSet) (hef : e ≠ f) {K L : Set Schoenflies.Plane} (hK : K ⊆ edgeArc drawing e) (hKV : Disjoint K G.vertexSet) (hL : L ⊆ edgeArc drawing f) : Disjoint K L

Distinct cores are disjoint. A subset of one edge's arc containing no vertex meets no other edge's arc at all, because distinct edges meet only at vertices. Stated for arbitrary subsets rather than for cores, since that is all the argument uses — and it is why exists_core carries Disjoint K V(G) rather than a clause about other edges.

theorem Graph.IsDrawing.exists_core {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsDrawing drawing) {e : β} {v w : Schoenflies.Plane} {r : ℝ} (hr : 0 < r) (hlink : G.IsLink e v w) (hdisj : Disjoint (v.closedSquare r) (w.closedSquare r)) : ∃ (K : Set Schoenflies.Plane) (p : Schoenflies.Plane) (q : Schoenflies.Plane), K ⊆ edgeArc drawing e ∧ IsCompact K ∧ Schoenflies.IsArcBetween K p q ∧ K ∩ v.closedSquare r = {p} ∧ K ∩ w.closedSquare r = {q} ∧ Disjoint K G.vertexSet

The core of an edge. Between the last parameter at which the edge's arc is inside the square about v and the first parameter after that at which it is inside the square about w sits a subarc K — the core — which meets the square at v in its first endpoint only, meets the square at w in its last endpoint only, and contains no vertex at all.

The two squares must be disjoint, which is what the uniform choice of exists_vertexSquares provides; disjointness in particular forces v ≠ w, so this says nothing about a loop edge — see the module report.

The "first entry after the last exit" is not the same as "first entry": nothing forbids the arc from dipping into the far square and coming back, so the second application of B3 is over [a, 1] and not over [0, 1].

That the endpoints of the core are not the vertices themselves is where the positivity of the radius is used: the arc starts at the centre of the square about v, so it is still inside the square just after leaving it, and the last exit therefore happens at a positive parameter. That fact is what makes Disjoint K V(G) true and hence distinct cores disjoint.