The model curve, and the parametrization of a Jordan curve by it

The blueprint's model curve is S = ∂Q, the boundary of the square Q = [-1,1]², and not the unit circle. That is a deliberate choice: this development is trigonometry-free, so a traversal of the round circle by an interval is unavailable, whereas S is four segments glued end to end and each segment is an arc by isArcBetween_segment. The blueprint says so explicitly ("Nothing in this document needs the unit circle in place of S").

modelCurve is defined by the sup norm, ‖x‖∞ = 1, which is the same square the rest of the development already speaks about (Plane.closedSquare 0 1), and it is cut into its four sides by modelCurve_eq_sides.

The content of Lemma 3.1

The lemma has three clauses. Only the first is proved here; the other two are already on main, transported along the homeomorphism the first clause supplies:

• "γ induces a homeomorphism from S onto C" — isJordanCurve_modelCurve together with IsJordanCurve.homeomorph_modelCurve. The general fact behind it is IsLoop.exists_homeomorph: a loop is a quotient map of [0,1] which identifies exactly 0 with 1, so any two loops induce a homeomorphism between their images, matching parameter for parameter.
• "two distinct points divide C into two simple arcs meeting exactly in those points" — this is IsJordanCurve.two_arcs in Schoenflies/TwoArcs.lean, proved directly on the parameter interval, which is strictly stronger than transporting it from S.
• "the relatively open subarcs form a basis of the subspace topology" — openArc_isRelOpen, openArc_subarc_isRelOpen and basic_piece_inside_ball in Schoenflies/Subarc.lean.

The route to the homeomorphism is the blueprint's, with the sequence argument replaced by its point-set content: t ↦ γ t is a continuous surjection from the compact [0,1] onto the Hausdorff C, hence a closed map, hence a quotient map; so a map out of C is continuous as soon as its composite with the parametrization is. That is exactly what the blueprint's subsequence chase establishes, and it is one line here.

Blueprint

• modelCurve — Lemma 3.1, the model curve S = ∂Q with Q = [-1,1]².
• modelCurve_eq_sides — the decomposition of S into its four sides.
• modelCurve_eq_frontier — S is literally the topological boundary of Q.
• isJordanCurve_modelCurve — S is a Jordan curve.
• IsLoop.param_eq_or, IsLoop.eq_of_eq — a loop identifies exactly the two endpoints of the parameter interval.
• IsLoop.exists_homeomorph — two loops induce a homeomorphism of their images.
• IsJordanCurve.homeomorph, IsJordanCurve.homeomorph_modelCurve, IsJordanCurve.modelCurve_homeomorph — Lemma 3.1, first clause.

Segments with a constant coordinate

The four sides of the square are axis-parallel, so each is pinned by one coordinate and swept by the other. Two lemmas serve all four.

theorem Schoenflies.mem_segment_horiz {u v c : ℝ} {x : Plane} : x ∈ segment ℝ (Plane.mk u c) (Plane.mk v c) ↔ x.ofLp 1 = c ∧ x.ofLp 0 ∈ segment ℝ u v

A horizontal segment: constant second coordinate, first coordinate sweeping a real segment.

theorem Schoenflies.mem_segment_vert {c u v : ℝ} {x : Plane} : x ∈ segment ℝ (Plane.mk c u) (Plane.mk c v) ↔ x.ofLp 0 = c ∧ x.ofLp 1 ∈ segment ℝ u v

A vertical segment: constant first coordinate, second coordinate sweeping a real segment.

theorem Schoenflies.segment_one_neg_one : segment ℝ 1 (-1) = Set.Icc (-1) 1

theorem Schoenflies.segment_neg_one_one : segment ℝ (-1) 1 = Set.Icc (-1) 1

The model curve and its four sides

def Schoenflies.modelCurve : Set Plane

The model curve S = ∂Q, the boundary of the square Q = [-1,1]², described by the sup norm.

Equations

• Schoenflies.modelCurve = {x : Schoenflies.Plane | x.supNorm = 1}

def Schoenflies.cornerNE : Plane

The corner (1, 1).

Equations

• Schoenflies.cornerNE = Schoenflies.Plane.mk 1 1

def Schoenflies.cornerNW : Plane

The corner (-1, 1).

Equations

• Schoenflies.cornerNW = Schoenflies.Plane.mk (-1) 1

def Schoenflies.cornerSW : Plane

The corner (-1, -1).

Equations

• Schoenflies.cornerSW = Schoenflies.Plane.mk (-1) (-1)

def Schoenflies.cornerSE : Plane

The corner (1, -1).

Equations

• Schoenflies.cornerSE = Schoenflies.Plane.mk 1 (-1)

def Schoenflies.sideTop : Set Plane

The top side of the square, traversed from (1,1) to (-1,1).

Equations

• Schoenflies.sideTop = segment ℝ Schoenflies.cornerNE Schoenflies.cornerNW

def Schoenflies.sideLeft : Set Plane

The left side of the square, traversed from (-1,1) to (-1,-1).

Equations

• Schoenflies.sideLeft = segment ℝ Schoenflies.cornerNW Schoenflies.cornerSW

def Schoenflies.sideBottom : Set Plane

The bottom side of the square, traversed from (-1,-1) to (1,-1).

Equations

• Schoenflies.sideBottom = segment ℝ Schoenflies.cornerSW Schoenflies.cornerSE

def Schoenflies.sideRight : Set Plane

The right side of the square, traversed from (1,-1) to (1,1).

Equations

• Schoenflies.sideRight = segment ℝ Schoenflies.cornerSE Schoenflies.cornerNE

theorem Schoenflies.mem_sideTop {x : Plane} : x ∈ sideTop ↔ x.ofLp 1 = 1 ∧ |x.ofLp 0| ≤ 1

theorem Schoenflies.mem_sideLeft {x : Plane} : x ∈ sideLeft ↔ x.ofLp 0 = -1 ∧ |x.ofLp 1| ≤ 1

theorem Schoenflies.mem_sideBottom {x : Plane} : x ∈ sideBottom ↔ x.ofLp 1 = -1 ∧ |x.ofLp 0| ≤ 1

theorem Schoenflies.mem_sideRight {x : Plane} : x ∈ sideRight ↔ x.ofLp 0 = 1 ∧ |x.ofLp 1| ≤ 1

theorem Schoenflies.modelCurve_eq_sides : modelCurve = sideTop ∪ sideLeft ∪ (sideBottom ∪ sideRight)

The model curve is the union of the four sides. The sup norm reaches 1 exactly when one coordinate is ±1 and the other is dominated by it.

The model curve is a Jordan curve

theorem Schoenflies.cornerNE_ne_cornerNW : cornerNE ≠ cornerNW

theorem Schoenflies.cornerNW_ne_cornerSW : cornerNW ≠ cornerSW

theorem Schoenflies.cornerSW_ne_cornerSE : cornerSW ≠ cornerSE

theorem Schoenflies.cornerSE_ne_cornerNE : cornerSE ≠ cornerNE

theorem Schoenflies.isArcBetween_sideTop : IsArcBetween sideTop cornerNE cornerNW

theorem Schoenflies.isArcBetween_sideLeft : IsArcBetween sideLeft cornerNW cornerSW

theorem Schoenflies.isArcBetween_sideBottom : IsArcBetween sideBottom cornerSW cornerSE

theorem Schoenflies.isArcBetween_sideRight : IsArcBetween sideRight cornerSE cornerNE

theorem Schoenflies.sideTop_meet_sideLeft (z : Plane) : z ∈ sideTop → z ∈ sideLeft → z = cornerNW

Consecutive sides meet only in the corner they share.

theorem Schoenflies.sideBottom_meet_sideRight (z : Plane) : z ∈ sideBottom → z ∈ sideRight → z = cornerSE

theorem Schoenflies.isArcBetween_upperSides : IsArcBetween (sideTop ∪ sideLeft) cornerNE cornerSW

The upper half of the model curve: two sides from (1,1) to (-1,-1).

theorem Schoenflies.isArcBetween_lowerSides : IsArcBetween (sideBottom ∪ sideRight) cornerSW cornerNE

The lower half of the model curve: two sides back from (-1,-1) to (1,1).

theorem Schoenflies.upperSides_meet_lowerSides (z : Plane) : z ∈ sideTop ∪ sideLeft → z ∈ sideBottom ∪ sideRight → z = cornerNE ∨ z = cornerSW

The two halves of the model curve meet exactly in the two corners they share: opposite sides are pinned to opposite values of one coordinate, so they are disjoint.

theorem Schoenflies.isJordanCurve_modelCurve : IsJordanCurve modelCurve

The model curve is a Jordan curve. Four segments glued end to end; no trigonometry anywhere.

theorem Schoenflies.isCompact_modelCurve : IsCompact modelCurve

theorem Schoenflies.cornerNE_mem_modelCurve : cornerNE ∈ modelCurve

The model curve is the boundary of the square

This is the blueprint's description S = ∂Q with Q = [-1,1]², and the check that the sup-norm definition above is the intended one. The only content is that a point of sup norm exactly 1 is not interior to the square: scaling it out by a factor 1 + δ leaves the square while moving an arbitrarily small distance.

theorem Schoenflies.smul_coord (a : ℝ) (x : Plane) (i : Fin 2) : (a • x).ofLp i = a * x.ofLp i

theorem Schoenflies.mem_closedSquare_zero_one {x : Plane} : x ∈ Plane.closedSquare 0 1 ↔ x.supNorm ≤ 1

theorem Schoenflies.mem_openSquare_zero_one {x : Plane} : x ∈ Plane.openSquare 0 1 ↔ x.supNorm < 1

theorem Schoenflies.modelCurve_subset_closedSquare : modelCurve ⊆ Plane.closedSquare 0 1

theorem Schoenflies.notMem_interior_closedSquare {x : Plane} (hx : x.supNorm = 1) : x ∉ interior (Plane.closedSquare 0 1)

A point of the model curve is not interior to the square: pushing it radially outwards by a factor 1 + δ leaves the square, and δ may be taken as small as one likes.

theorem Schoenflies.interior_closedSquare_zero_one : interior (Plane.closedSquare 0 1) = Plane.openSquare 0 1

theorem Schoenflies.modelCurve_eq_frontier : modelCurve = frontier (Plane.closedSquare 0 1)

The model curve is ∂Q, the topological boundary of the closed square Q = [-1,1]².

A loop identifies exactly the ends of the parameter interval

theorem Schoenflies.IsLoop.param_eq_or {f : ℝ → Plane} (hf : IsLoop f) {s t : ℝ} (hs : s ∈ unitInterval) (ht : t ∈ unitInterval) (h : f s = f t) : s = t ∨ s = 0 ∧ t = 1 ∨ s = 1 ∧ t = 0

Two parameters of [0,1] with the same image under a loop are equal, or are the two ends of the interval. This is the whole of a loop's non-injectivity.

theorem Schoenflies.IsLoop.eq_of_eq {f g : ℝ → Plane} (hf : IsLoop f) (hg : IsLoop g) {s t : ℝ} (hs : s ∈ unitInterval) (ht : t ∈ unitInterval) (h : f s = f t) : g s = g t

Every loop makes the same identifications on [0,1]. This is what lets a loop be transported to any other loop: the induced map on images is well defined.

theorem Schoenflies.IsLoop.exists_homeomorph {f g : ℝ → Plane} (hf : IsLoop f) (hg : IsLoop g) : ∃ (h : ↑(f '' unitInterval) ≃ₜ ↑(g '' unitInterval)), ∀ (t : ℝ) (ht : t ∈ unitInterval), ↑(h ⟨f t, ⋯⟩) = g t

Any two loops induce a homeomorphism between their images, matching parameters.

t ↦ f t is a continuous surjection of the compact [0,1] onto the Hausdorff image, hence a closed map, hence a quotient map; so a map out of the image is continuous as soon as its composite with the parametrization is. The induced map is well defined by eq_of_eq, and bijective because eq_of_eq runs in both directions.

Lemma 3.1: parametrization by the model curve

theorem Schoenflies.IsJordanCurve.homeomorph {C D : Set Plane} (hC : IsJordanCurve C) (hD : IsJordanCurve D) : Nonempty (↑C ≃ₜ ↑D)

Any two Jordan curves are homeomorphic.

theorem Schoenflies.IsJordanCurve.homeomorph_modelCurve {C : Set Plane} (hC : IsJordanCurve C) : Nonempty (↑C ≃ₜ ↑modelCurve)

Lemma 3.1. A Jordan curve is homeomorphic to the model curve S = ∂Q.

theorem Schoenflies.IsJordanCurve.modelCurve_homeomorph {C : Set Plane} (hC : IsJordanCurve C) : Nonempty (↑modelCurve ≃ₜ ↑C)

Lemma 3.1, the other direction: the model curve maps homeomorphically onto any Jordan curve. This is the form the blueprint states — γ induces a homeomorphism from S onto C.