Documentation

LeanPool.Schoenflies.CrosscutEncloses

thm:polygonal-crosscut at the level of sets, and the geometric half of the outer-chain descent #

The blueprint sentence this module discharges is one line of the proof of lem:outer-chain:

The path R lies on one side of C and is a crosscut there. By thm:polygonal-crosscut, exactly one of the two cycles R ∪ C₁, R ∪ C₂ encloses x.

Graph.CrosscutEncloses of Schoenflies/OuterChain.lean is that sentence weakened to at least one, which is all the descent uses; the weakening is not undone here.

One theorem, no case split #

The blueprint — and the note in Schoenflies/OuterChain.lean — distinguishes the crosscut running inside C (settled by Schoenflies.crosscutSplitsRegion) from the crosscut running outside it (Schoenflies.IsPolygonalCrosscut.inside_exactly_one). Neither case distinction is needed. Both are consequences of Lemma 2.7, the parity identity

π_{A₁ ∪ P} + π_{A₂ ∪ P} = π_J        at *every* point of the plane,

which holds with no geometry whatever (Schoenflies.parity_split), together with the one direction of Theorem 2.3 that needs no realization of the two spliced curves:

a closed chain whose cover separates has crossing count `0` on the unbounded region

(Schoenflies.parity_eq_zero_of_mem_outside_cover). If x were outside both spliced curves the identity would read 0 + 0 = π_J(x), whereas π_J(x) = 1 because x is inside J. That is the whole proof of Schoenflies.crosscut_inside_at_least_one, and it is uniform in which side the crosscut runs on. The ClosedPolygon-level Schoenflies.IsPolygonalCrosscut.inside_exactly_one, whose SameEdges hypotheses cannot be met at graph vertices (see the section docstring of Schoenflies/FaceCyclesLand.lean), is therefore not used at all.

The price is that the conclusion is "at least one" rather than "exactly one": the converse direction of Theorem 2.3 for the spliced curves — π = 1 forces the bounded region — does need them realized, and the descent does not want it.

The set-level statement is the artefact #

Schoenflies.crosscut_inside_at_least_one takes sets and arcs, not polygons and not graphs:

`J` a polygonal Jordan curve, `A₁, A₂` arcs from `p` to `q` covering it, `P` a polygonal arc
from `p` to `q` meeting `J` only at `p, q`; then a point inside `J` and off `P` is inside
`A₁ ∪ P` or inside `A₂ ∪ P`.

That is thm:polygonal-crosscut in the shape every plane-graph consumer wants, and Graph.crosscutEnclosesOff is a two-page corollary of it. A second general fact falls out on the way: Schoenflies.two_arcs_inter_of_union — two arcs with the same ends that cover a Jordan curve meet exactly at those ends. That removes the "the two arcs meet only at the cut points" clause from every consumer's obligations, which matters here because Graph.IsCycleCrosscut does not record it (see below).

Two defects of the interface handed to this module — read before integrating #

1. Graph.CrosscutEncloses as stated on main is false, and the deliverable is Graph.CrosscutEnclosesOff, which is it plus one hypothesis: x ∈ exterior H drawing. Nothing in Graph.CrosscutEncloses prevents x from lying on the crosscut's own drawing: x is only assumed to be inside the cycle C, and a crosscut running inside C may pass through x. Then x ∈ (A₁ ∪ P) ∩ (A₂ ∪ P), so x is inside neither spliced curve and the conclusion fails.

The repair costs the chain nothing. Graph.OuterOnPairs already puts x off the whole chain (Graph.IsPlaneChain.mem_exterior_chain), and every block lies inside the chain (Graph.pointSet_mono), so the clause can be produced where it is needed instead of being carried. Graph.IsPlaneChain.descent_of_crosscutOff below therefore proves Graph.Descent exactly as it stands on main, and Graph.IsPlaneChain.outer_chain_of_crosscutExists is lem:outer-chain with Graph.CrosscutEncloses discharged outright. Nothing in Schoenflies/OuterChain.lean has to change; Graph.CrosscutEncloses should simply be deleted, together with Graph.IsPlaneChain.descent_of_crosscut and Graph.IsPlaneChain.outer_chain_of_crosscut, which the two theorems here replace.

2. Graph.IsCycleCrosscut does not record that the two arcs meet only at the two cut points, although Graph.IsCycleThrough.split_at — the theorem that builds them — produces exactly that clause. It is not needed here, because Schoenflies.two_arcs_inter_of_union recovers the geometric consequence from the Jordan curve; but a consumer that wants the combinatorial statement will have to add the field.

Blueprint #

Two arcs that cover a Jordan curve meet at their ends #

Schoenflies.two_arcs_unique_of_isClosed identifies a given two-arc splitting with any other splitting whose two pieces are known to meet exactly at the two points. What a graph consumer has is weaker: two arcs of a cycle whose union is the whole curve, with nothing said about their intersection. This lemma supplies the intersection, by comparing with the splitting that Schoenflies.IsJordanCurve.two_arcs produces out of nothing.

source
theorem Schoenflies.two_arcs_inter_of_union {C A₁ A₂ : Set Plane} {p q : Plane} (hC : IsJordanCurve C) (hA1 : IsArcBetween A₁ p q) (hA2 : IsArcBetween A₂ p q) (hunion : A₁ ∪ A₂ = C) :
A₁ ∩ A₂ = {p, q}

Two arcs with the same ends that cover a Jordan curve meet exactly at those ends.

The proof is the key step of Schoenflies.two_arcs_unique_of_isClosed run against the reference splitting: an arc from p to q inside the curve has connected complement-of-endpoints, so it lands in one piece of any splitting whose two pieces meet exactly at p, q; the two arcs cannot land in the same piece, since the other piece would then be just {p, q}; and once they land in different pieces they exhaust them.

thm:polygonal-crosscut at the level of sets #

The statement a plane-graph consumer wants: sets and arcs, no polygon presentation anywhere in the hypotheses, and the two spliced curves named by the literal unions Aᵢ ∪ P.

source
theorem Schoenflies.crosscut_inside_at_least_one {J A₁ A₂ P : Set Plane} {p q x : Plane} (hJ : IsJordanCurve J) (hJpoly : IsPolygonal J) (hPpoly : IsPolygonal P) (hA1 : IsArcBetween A₁ p q) (hA2 : IsArcBetween A₂ p q) (hunion : A₁ ∪ A₂ = J) (hParc : IsArcBetween P p q) (hPJ : P ∩ J = {p, q}) (hx : x ∈ inside J) (hxP : x ∉ P) :
x ∈ inside (A₁ ∪ P) ∨ x ∈ inside (A₂ ∪ P)

The polygonal crosscut theorem, at the level of sets. J is a polygonal Jordan curve, cut by the two points p, q into the arcs A₁, A₂; P is a polygonal arc from p to q meeting J in nothing but p and q. Then a point inside J and off P lies inside at least one of the two spliced curves A₁ ∪ P, A₂ ∪ P.

Nothing is assumed about which side of J the crosscut runs on; the proof does not distinguish the two cases of the blueprint. Nor is A₁ ∩ A₂ = {p, q} assumed — it is derived, by Schoenflies.two_arcs_inter_of_union.

The route: present J as a Schoenflies.PrePolygon with p and q among its vertices (Schoenflies.exists_prePolygon_split), identify the two given arcs with the two arcs of that presentation (Schoenflies.two_arcs_unique_of_isClosed), and read the parity identity π_{A₁ ∪ P} + π_{A₂ ∪ P} = π_J (Schoenflies.parity_split) at the point. Were the point outside both spliced curves both left-hand terms would vanish (Schoenflies.parity_eq_zero_of_mem_outside_cover, which needs no realization of Aᵢ ∪ P), while the right-hand side is 1 because the point is inside J.

What a walk visits lies on what it draws #

Graph.IsDrawing.mem_walkVertices_of_mem_edgesCover goes the other way; this direction is the first half of the proof of Graph.IsDrawing.pointSet_pathGraphOf, extracted.

source
theorem Graph.IsDrawing.mem_edgesCover_of_mem_walkVertices {β : Type u_1} {H : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (h : H.IsDrawing drawing) {u v y : Schoenflies.Plane} {W : List β} (hW : H.IsWalk u W v) (hne : W ≠ []) (hy : y ∈ H.walkVertices u W) :
y ∈ edgesCover drawing W

Every vertex a nonempty walk visits lies on what the walk draws. The source is an end of the first edge; every other visited vertex is an end of one of the edges by definition.

The geometric half of the descent step #

Graph.CrosscutEncloses of Schoenflies/OuterChain.lean, plus the hypothesis it is missing.

source
def Graph.CrosscutEnclosesOff {β : Type u_1} (drawing : β → ℝ → Schoenflies.Plane) (x : Schoenflies.Plane) :
Prop

Graph.CrosscutEncloses with the clause it is missing: x is off the drawing of H.

Without it the statement is false — see the module docstring. Graph.CrosscutEncloses puts x inside the cycle C and nothing more, so a crosscut running inside C may pass through x; then x lies on both spliced curves and is inside neither. Everything else is Graph.CrosscutEncloses verbatim, so that the substitution into Graph.IsPlaneChain.descent_of_crosscut is mechanical once Graph.Descent carries the same clause.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Graph.crosscutEnclosesOff {β : Type u_1} (drawing : β → ℝ → Schoenflies.Plane) (x : Schoenflies.Plane) :
    CrosscutEnclosesOff drawing x

    The geometric half of the descent step of lem:outer-chain. "The path R lies on one side of C and is a crosscut there; by thm:polygonal-crosscut, exactly one of the two cycles R ∪ C₁, R ∪ C₂ encloses x" — weakened to at least one, and with x required to be off the drawing.

    Everything geometric is Schoenflies.crosscut_inside_at_least_one; what happens here is the translation of the graph data into its hypotheses. The two arcs of the cycle are arcs of the plane by Graph.IsDrawing.path_isArcBetween, they cover the cycle's realisation because their edge lists do, and they meet exactly at the two cut points by Schoenflies.two_arcs_inter_of_union — which is why Graph.IsCycleCrosscut gets away with not recording that. That the crosscut meets the cycle only at its ends is the edges_new and interior clauses read through Graph.IsDrawing.edge_inter.

    lem:outer-chain needs only the combinatorial half now #

    The extra hypothesis of Graph.CrosscutEnclosesOff does not have to be threaded through Graph.Descent: the chain hypothesis Graph.OuterOnPairs already puts x off the whole chain (Graph.IsPlaneChain.mem_exterior_chain), and every block of the chain lies inside it. So the repair costs the interface nothing at all — Graph.Descent is used here exactly as it stands on main, and the two theorems below are drop-in replacements for Graph.IsPlaneChain.descent_of_crosscut and Graph.IsPlaneChain.outer_chain_of_crosscut with Graph.CrosscutEncloses discharged.

    source
    theorem Graph.IsPlaneChain.descent_of_crosscutOff {β : Type u_1} {drawing : β → ℝ → Schoenflies.Plane} {Γ : ℕ → Graph Schoenflies.Plane β} {G : Graph Schoenflies.Plane β} {n : ℕ} {x : Schoenflies.Plane} (h : IsPlaneChain Γ drawing G n) (hout : OuterOnPairs Γ drawing n x) (hce : CrosscutExists Γ drawing n x) (hcen : CrosscutEnclosesOff drawing x) :
    Descent Γ drawing n x

    The descent step from its two halves, with the geometric half taken in the corrected form Graph.CrosscutEnclosesOff. The missing clause "x is off the drawing of the block" is supplied from Graph.OuterOnPairs, so Graph.Descent is produced with its statement on main unchanged.

    source
    theorem Graph.IsPlaneChain.outer_chain_of_crosscutExists {β : Type u_1} {drawing : β → ℝ → Schoenflies.Plane} {Γ : ℕ → Graph Schoenflies.Plane β} {G : Graph Schoenflies.Plane β} {n : ℕ} {x : Schoenflies.Plane} (h : IsPlaneChain Γ drawing G n) (hout : OuterOnPairs Γ drawing n x) (hce : CrosscutExists Γ drawing n x) :
    x ∈ (chainUnion Γ 0 n).exterior drawing ∧ ¬Bornology.IsBounded ((chainUnion Γ 0 n).face drawing x)

    lem:outer-chain (outer face of a chain), with the geometric half of the descent step discharged. Only Graph.CrosscutExists — the purely combinatorial construction of the crosscut — is still assumed.

    This is Graph.IsPlaneChain.outer_chain_of_crosscut with the argument hcen supplied by Graph.crosscutEnclosesOff.