Documentation

LeanPool.Schoenflies.InitialPair

The initial matched pair #

The entry point of Part II (prop:initial-pair). def:generated-structure builds every later stage from this one by two elementary operations, so the construction is exported as data — one abstract CellStructure, two Realizations of it, and the SkeletonHomeo between them — and not as an existentially packaged bundle. Schoenflies.initial_pair at the end is only a restatement of the blueprint sentence; nothing should be consumed through it.

The shape of the construction #

The blueprint's u : C → S is taken as data, not produced inside the proof, because every later stage uses the same u. Schoenflies.IsSetHomeoOn is the set-level form of it, and Schoenflies.exists_isSetHomeoOn_modelCurve produces one from lem:jordan-circle.

The target side is completely explicit: six marked points on S (four corners, u(a) on the top side and u(b) on the bottom side), seven straight edges. The source side is the pushforward of the target's outer cycle along w = u⁻¹, plus the polygonal crosscut. That asymmetry is deliberate: nothing about the six source arcs has to be proved, because w is injective on S and each drawing condition transfers.

The nonadjacency hypothesis of prop:initial-pair is used in exactly one place, Schoenflies.openSegment_chord_supNorm_lt: u(a) and u(b) lie on opposite sides, so every interior point of the straight chord has sup norm < 1, hence lies in Q°.

What is assumed #

Exactly two hypotheses are carried, and only by the theorems that need them. Neither is a restatement of anything proved here.

Blueprint #

Set-level homeomorphisms #

lem:jordan-circle is stated in this library with subtype homeomorphisms ↥C ≃ₜ ↥modelCurve. Everything below needs u as a map of the plane restricted to C, because it has to be glued to a map defined on the crosscut. IsSetHomeoOn is that shape, with the inverse supplied as data — the same convention as CellStructure.SkeletonHomeo.

source
structure Schoenflies.IsSetHomeoOn (u w : Plane → Plane) (X Y : Set Plane) :
Prop

u maps X homeomorphically onto Y, with inverse w.

  • continuousOn : ContinuousOn u X

    The map is continuous on its domain.

  • continuousOn_inv : ContinuousOn w Y

    The inverse is continuous on its domain.

  • mapsTo : Set.MapsTo u X Y

    The map sends the domain into the codomain.

  • mapsTo_inv : Set.MapsTo w Y X

    The inverse sends the codomain into the domain.

  • leftInvOn : Set.LeftInvOn w u X

    The inverse undoes the map.

  • rightInvOn : Set.RightInvOn w u Y

    The map undoes the inverse.

Instances For
    source
    theorem Schoenflies.IsSetHomeoOn.symm {u w : Plane → Plane} {X Y : Set Plane} (h : IsSetHomeoOn u w X Y) :
    IsSetHomeoOn w u Y X

    Running the homeomorphism backwards.

    source
    theorem Schoenflies.IsSetHomeoOn.injOn {u w : Plane → Plane} {X Y : Set Plane} (h : IsSetHomeoOn u w X Y) :
    Set.InjOn u X
    source
    theorem Schoenflies.IsSetHomeoOn.injOn_inv {u w : Plane → Plane} {X Y : Set Plane} (h : IsSetHomeoOn u w X Y) :
    Set.InjOn w Y
    source
    theorem Schoenflies.IsSetHomeoOn.image_eq {u w : Plane → Plane} {X Y : Set Plane} (h : IsSetHomeoOn u w X Y) :
    u '' X = Y
    source
    theorem Schoenflies.IsSetHomeoOn.image_inv_eq {u w : Plane → Plane} {X Y : Set Plane} (h : IsSetHomeoOn u w X Y) :
    w '' Y = X
    source
    theorem Schoenflies.IsSetHomeoOn.image_isRelOpen {u w : Plane → Plane} {X Y : Set Plane} (h : IsSetHomeoOn u w X Y) {U V : Set Plane} (hV : IsOpen V) (hU : U = V ∩ X) :
    ∃ (W : Set Plane), IsOpen W ∧ u '' U = W ∩ Y

    The image of a relatively open subset of the domain is relatively open in the codomain. This is what makes the two open arcs of prop:initial-pair relatively open in C, hence able to meet the countable dense set of strongly accessible points.

    source
    theorem Schoenflies.exists_isSetHomeoOn_modelCurve {C : Set Plane} (hC : IsJordanCurve C) :
    ∃ (u : Plane → Plane) (w : Plane → Plane), IsSetHomeoOn u w C modelCurve

    lem:jordan-circle, in set-level form. A Jordan curve carries a homeomorphism onto the model curve, presented as a pair of maps of the plane.

    The fifteen cells of the initial structure #

    The blueprint fixes the base value of ≼_abs immediately after def:generated-structure (tex 1590–1602). Its cells are the six boundary vertices — the four corner preimages together with a, b —, the six open outer edges into which they divide C, the crosscut edge P, and the two 2-cells R₁, R₂.

    The six vertices are indexed cyclically by Fin 6, in the order they occur along C:

    vert 0 = u⁻¹(1,1)   vert 1 = a   vert 2 = u⁻¹(-1,1)
vert 3 = u⁻¹(-1,-1) vert 4 = b   vert 5 = u⁻¹(1,-1)

    so that a lies in the corner arc between corners 0 and 1 and b in the corner arc between corners 2 and 3 — the nonadjacency of prop:initial-pair, here visible as vert 1 and vert 4 being antipodal in Fin 6. edge i runs from vert i to vert (i+1), and chord from vert 1 to vert 4.

    The two boundary edge-paths from a to b are therefore B₁ = [edge 1, edge 2, edge 3] (through the corners 2, 3) and B₂ = [edge 4, edge 5, edge 0] (through the corners 5, 0); both contain corner vertices, as the blueprint observes. face false is R₁ and face true is R₂.

    source
    inductive Schoenflies.InitialCell :
    Type

    A cell of the initial matched cell structure.

    • vert : Fin 6 → InitialCell

      One of the six boundary vertices, in cyclic order along C.

    • edge : Fin 6 → InitialCell

      The outer edge from vert i to vert (i + 1).

    • chord : InitialCell

      The crosscut edge, from vert 1 to vert 4.

    • face : Bool → InitialCell

      One of the two 2-cells: face false is R₁, face true is R₂.

    • aux : ℕ → InitialCell

      A spare name, belonging to no cell of the initial structure.

      The initial structure uses fifteen names; this constructor adds countably many more that it never uses. It is here for one reason: thm:finite-transfer needs [Infinite γ], because an ear insertion consumes fresh cell names and on a finite name type the step is false. Without a spare supply the base case could not feed the recursion at all. Nothing below ever produces an aux, and no cell of initialStructure is one.

    Instances For
      source
      def Schoenflies.instDecidableEqInitialCell.decEq (x✝ x✝¹ : InitialCell) :
      Decidable (x✝ = x✝¹)
      Equations
      Instances For
        source
        @[instance_reducible]
        instance Schoenflies.instDecidableEqInitialCell :
        DecidableEq InitialCell
        Equations
        source
        def Schoenflies.InitialCell.ends :
        InitialCell → InitialCell × InitialCell

        The two ends of a cell, when it is an edge. Junk elsewhere; the graph below only ever consults it on an edge name.

        Equations
        Instances For
          source
          def Schoenflies.InitialCell.vertices :
          Set InitialCell

          The six 0-cells.

          Equations
          Instances For
            source
            def Schoenflies.InitialCell.edges :
            Set InitialCell

            The seven 1-cells: six outer edges and the crosscut.

            Equations
            Instances For
              source
              def Schoenflies.InitialCell.outerEdges :
              Set InitialCell

              The six outer 1-cells.

              Equations
              Instances For
                source
                def Schoenflies.InitialCell.faces :
                Set InitialCell

                The two 2-cells.

                Equations
                Instances For
                  source
                  theorem Schoenflies.InitialCell.outerEdges_subset_edges :
                  outerEdges ⊆ edges
                  source
                  theorem Schoenflies.InitialCell.edge_mem_edges (i : Fin 6) :
                  edge i ∈ edges
                  source
                  theorem Schoenflies.InitialCell.chord_mem_edges :
                  chord ∈ edges
                  source
                  theorem Schoenflies.InitialCell.vert_mem_vertices (i : Fin 6) :
                  vert i ∈ vertices
                  source
                  theorem Schoenflies.InitialCell.ends_mem_vertices {e : InitialCell} (he : e ∈ edges) :
                  e.ends.1 ∈ vertices ∧ e.ends.2 ∈ vertices

                  Both ends of a 1-cell are 0-cells.

                  source
                  theorem Schoenflies.InitialCell.finite_vertices :
                  vertices.Finite
                  source
                  theorem Schoenflies.InitialCell.finite_edges :
                  edges.Finite
                  source
                  theorem Schoenflies.InitialCell.finite_faces :
                  faces.Finite
                  source
                  theorem Schoenflies.InitialCell.disjoint_vertices_edges :
                  Disjoint vertices edges
                  source
                  theorem Schoenflies.InitialCell.disjoint_faces_vertices :
                  Disjoint faces vertices
                  source
                  theorem Schoenflies.InitialCell.disjoint_faces_edges :
                  Disjoint faces edges
                  source
                  def Schoenflies.initSkel :
                  Graph InitialCell InitialCell

                  The abstract 1-skeleton of the initial structure: a hexagon with one long chord.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Schoenflies.initOuter :
                    Graph InitialCell InitialCell

                    The distinguished outer cycle: the same hexagon without the chord.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[simp]
                      theorem Schoenflies.vertexSet_initSkel :
                      initSkel.vertexSet = InitialCell.vertices
                      source
                      @[simp]
                      theorem Schoenflies.edgeSet_initSkel :
                      initSkel.edgeSet = InitialCell.edges
                      source
                      @[simp]
                      theorem Schoenflies.vertexSet_initOuter :
                      initOuter.vertexSet = InitialCell.vertices
                      source
                      @[simp]
                      theorem Schoenflies.edgeSet_initOuter :
                      initOuter.edgeSet = InitialCell.outerEdges
                      source
                      theorem Schoenflies.initOuter_le_initSkel :
                      initOuter ≤ initSkel
                      source
                      def Schoenflies.faceCells :
                      Bool → Set InitialCell

                      The cells lying on the closed boundary of a 2-cell: the vertices and edges of Bᵢ together with the crosscut. face false = R₁ is bounded by B₁ ∪ P, face true = R₂ by B₂ ∪ P.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def Schoenflies.initBoundary :
                        InitialCell → List InitialCell

                        The cyclic boundary walk of each 2-cell, as a list of edge names.

                        Equations
                        Instances For
                          source
                          def Schoenflies.cellNames :
                          Set InitialCell

                          The names that initialStructure declares to be cells: the six 0-cells, the seven 1-cells and the two 2-cells. This is initialStructure.cells unfolded, written out here because initSub is a field of initialStructure and cannot refer to it.

                          Equations
                          Instances For
                            source
                            theorem Schoenflies.aux_notMem_cellNames (n : ℕ) :
                            InitialCell.aux n ∉ cellNames
                            source
                            def Schoenflies.initSub (c d : InitialCell) :
                            Prop

                            The base value of ≼_abs (tex 1590–1602): the reflexive pairs, the incidence of each vertex with the edges it bounds, and, for i = 1, 2, the incidence of every vertex and edge of Bᵢ ∪ P with Rᵢ. Nothing else.

                            The reflexive clause is restricted to cellNames. ≼_abs must relate cells to cells — CellStructure.CombInvariants.sub_mem_left and .sub_mem_right say so — and InitialCell carries a spare supply of names beyond the fifteen cells, so unrestricted reflexivity would relate a spare name to itself and make both false.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              theorem Schoenflies.initSub_refl {c : InitialCell} (hc : c ∈ cellNames) :
                              initSub c c
                              source
                              theorem Schoenflies.initSub_ends {e : InitialCell} (he : e ∈ InitialCell.edges) :
                              initSub e.ends.1 e ∧ initSub e.ends.2 e
                              source
                              theorem Schoenflies.initSub_face {k : Bool} {c : InitialCell} (h : c ∈ faceCells k) :
                              initSub c (InitialCell.face k)
                              source
                              def Schoenflies.initialStructure :
                              CellStructure InitialCell

                              The abstract record of the initial matched cellulation.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                @[simp]
                                theorem Schoenflies.initialStructure_skel :
                                initialStructure.skel = initSkel
                                source
                                @[simp]
                                theorem Schoenflies.initialStructure_sub :
                                initialStructure.sub = initSub
                                source
                                @[simp]
                                theorem Schoenflies.initialStructure_faces :
                                initialStructure.faces = InitialCell.faces
                                source
                                @[simp]
                                theorem Schoenflies.initialStructure_outerGraph :
                                initialStructure.outerGraph = initOuter
                                source
                                theorem Schoenflies.outerEdgeUniqueFace_initialStructure :
                                initialStructure.OuterEdgeUniqueFace

                                Every outer edge is a subcell of exactly one 2-cell — assertion (vi) of lem:cellulation-invariants for the base structure, and the hypothesis of CellStructure.outerEdge_face_corresponds. The edges of B₁ bound R₁ only and those of B₂ bound R₂ only, which is the whole content.

                                A realization of the initial structure, from six points and seven parametrizations #

                                Both realizations of prop:initial-pair have the same shape: six points in cyclic position, six parametrized arcs joining consecutive ones, and one chord from the second point to the fifth. HexData bundles that shape together with the three geometric side conditions a plane drawing needs, and HexData.realization turns it into a CellStructure.Realization of initialStructure. Building it once means the square side and the curve side are checked against the same list.

                                The pairwise-meeting conditions are stated in the weakest usable form: two outer arcs meet only in points that are ends of both, and the chord meets each outer arc only in its own two ends. Everything IsDrawing asks for follows, including "an arc contains no vertex but its own two ends", which is derived rather than assumed (HexData.mem_outer_iff).

                                source
                                structure Schoenflies.HexData :
                                Type

                                The geometric data of one realization of initialStructure.

                                Instances For
                                  source
                                  def Schoenflies.HexData.point (H : HexData) :
                                  InitialCell → Plane

                                  Where each 0-cell sits. Junk on the other cells, which Realization never reads.

                                  Equations
                                  Instances For
                                    source
                                    def Schoenflies.HexData.draw (H : HexData) :
                                    InitialCell → ℝ → Plane

                                    How each 1-cell is drawn. Junk on the other cells.

                                    Equations
                                    Instances For
                                      source
                                      def Schoenflies.HexData.chordSet (H : HexData) :
                                      Set Plane

                                      The crosscut, as a set.

                                      Equations
                                      Instances For
                                        source
                                        def Schoenflies.HexData.arcOf (H : HexData) :
                                        Bool → Set Plane

                                        The two boundary edge-paths from pos 1 to pos 4, as sets: arcOf false is A₁, the union of the outer edges 1, 2, 3, and arcOf true is A₂, the union of 4, 5, 0.

                                        Equations
                                        Instances For
                                          source
                                          def Schoenflies.HexData.outerArcs (H : HexData) :
                                          Set Plane

                                          The realized outer cycle, as the union of the six outer edges.

                                          Equations
                                          Instances For
                                            source
                                            def Schoenflies.HexData.cellSet (H : HexData) :
                                            InitialCell → Set Plane

                                            The point set of each open cell.

                                            The 2-cell face k is realized by the side of the crosscut belonging to Aₖ, exactly as the blueprint prescribes (tex 1590–1602): "the 2-cell Rᵢ is realized in the source as the crosscut side whose closure meets C in Aᵢ". By thm:general-crosscut that side is Int(Aᵢ ∪ P) = inside (arcOf k ∪ chordSet), and taking this as the definition makes the crosscut theorem apply to it with nothing to transport.

                                            Equations
                                            Instances For
                                              source
                                              @[simp]
                                              theorem Schoenflies.HexData.point_vert (H : HexData) (i : Fin 6) :
                                              H.point (InitialCell.vert i) = H.pos i
                                              source
                                              @[simp]
                                              theorem Schoenflies.HexData.draw_edge (H : HexData) (i : Fin 6) :
                                              H.draw (InitialCell.edge i) = H.outer i
                                              source
                                              @[simp]
                                              theorem Schoenflies.HexData.draw_chord (H : HexData) :
                                              H.draw InitialCell.chord = H.chordParam
                                              source
                                              @[simp]
                                              theorem Schoenflies.HexData.edgeArc_edge (H : HexData) (i : Fin 6) :
                                              Graph.edgeArc H.draw (InitialCell.edge i) = H.outer i '' unitInterval
                                              source
                                              @[simp]
                                              theorem Schoenflies.HexData.edgeArc_chord (H : HexData) :
                                              Graph.edgeArc H.draw InitialCell.chord = H.chordParam '' unitInterval
                                              source
                                              theorem Schoenflies.HexData.pos_mem_outer (H : HexData) (i : Fin 6) :
                                              H.pos i ∈ H.outer i '' unitInterval
                                              source
                                              theorem Schoenflies.HexData.pos_succ_mem_outer (H : HexData) (i : Fin 6) :
                                              H.pos (i + 1) ∈ H.outer i '' unitInterval
                                              source
                                              theorem Schoenflies.HexData.mem_outer_iff (H : HexData) {k i : Fin 6} (h : H.pos k ∈ H.outer i '' unitInterval) :
                                              k = i ∨ k = i + 1

                                              A vertex lies on an outer edge only if it is one of its two ends. Not an axiom of HexData: a vertex is an end of its own outer edge, so a vertex on a second edge is a point of two edges, and the meeting condition places it among the ends of both.

                                              source
                                              theorem Schoenflies.HexData.mem_chord_iff (H : HexData) {k : Fin 6} (h : H.pos k ∈ H.chordParam '' unitInterval) :
                                              k = 1 ∨ k = 4

                                              A vertex lies on the crosscut only if it is one of its two ends.

                                              source
                                              theorem Schoenflies.HexData.injOn_point (H : HexData) :
                                              Set.InjOn H.point initSkel.vertexSet
                                              source
                                              theorem Schoenflies.HexData.isDrawing (H : HexData) :
                                              (Graph.map H.point initSkel).IsDrawing H.draw

                                              The drawn skeleton: the pushforward of initSkel along the six positions.

                                              source
                                              def Schoenflies.HexData.realization (H : HexData) :
                                              initialStructure.Realization

                                              The realization of initialStructure determined by a HexData.

                                              Equations
                                              Instances For
                                                source
                                                @[simp]
                                                theorem Schoenflies.HexData.realization_pos (H : HexData) :
                                                H.realization.pos = H.point
                                                source
                                                @[simp]
                                                theorem Schoenflies.HexData.realization_drawing (H : HexData) :
                                                H.realization.drawing = H.draw
                                                source
                                                @[simp]
                                                theorem Schoenflies.HexData.realization_cell (H : HexData) :
                                                H.realization.cell = H.cellSet

                                                The realized skeleton and the two boundary arcs #

                                                source
                                                theorem Schoenflies.HexData.pos_ne (H : HexData) {i j : Fin 6} (h : i ≠ j) :
                                                H.pos i ≠ H.pos j
                                                source
                                                theorem Schoenflies.HexData.outer_meet_pair (H : HexData) {i j : Fin 6} (hij : i ≠ j) {z : Plane} (hi : z ∈ H.outer i '' unitInterval) (hj : z ∈ H.outer j '' unitInterval) :
                                                (z = H.pos i ∨ z = H.pos (i + 1)) ∧ (z = H.pos j ∨ z = H.pos (j + 1))
                                                source
                                                theorem Schoenflies.HexData.isArcBetween_outer (H : HexData) (i : Fin 6) :
                                                IsArcBetween (H.outer i '' unitInterval) (H.pos i) (H.pos (i + 1))

                                                Each outer edge is drawn as an arc between consecutive vertices.

                                                source
                                                theorem Schoenflies.HexData.isArcBetween_chordSet (H : HexData) :
                                                IsArcBetween H.chordSet (H.pos 1) (H.pos 4)

                                                The crosscut is drawn as an arc from a to b.

                                                source
                                                theorem Schoenflies.HexData.outerArcs_eq (H : HexData) :
                                                H.outerArcs = H.outer 0 '' unitInterval ∪ (H.outer 1 '' unitInterval ∪ (H.outer 2 '' unitInterval ∪ (H.outer 3 '' unitInterval ∪ (H.outer 4 '' unitInterval ∪ H.outer 5 '' unitInterval))))
                                                source
                                                theorem Schoenflies.HexData.arcOf_union (H : HexData) :
                                                H.arcOf false ∪ H.arcOf true = H.outerArcs
                                                source
                                                theorem Schoenflies.HexData.arcOf_false_isArcBetween (H : HexData) :
                                                IsArcBetween (H.arcOf false) (H.pos 1) (H.pos 4)

                                                A₁ is an arc from a to b. Three consecutive outer edges, glued at the two corner vertices between them.

                                                source
                                                theorem Schoenflies.HexData.arcOf_true_isArcBetween (H : HexData) :
                                                IsArcBetween (H.arcOf true) (H.pos 4) (H.pos 1)

                                                A₂ is an arc from b to a.

                                                source
                                                theorem Schoenflies.HexData.arcOf_inter (H : HexData) :
                                                H.arcOf false ∩ H.arcOf true = {H.pos 1, H.pos 4}

                                                The two boundary arcs meet exactly at a and b. Nine pairs of outer edges; six of them have no vertex in common at all and contribute nothing.

                                                source
                                                theorem Schoenflies.HexData.chordSet_inter_outerArcs (H : HexData) :
                                                H.chordSet ∩ H.outerArcs = {H.pos 1, H.pos 4}

                                                The crosscut meets the outer cycle exactly at its two endpoints.

                                                source
                                                theorem Schoenflies.HexData.outerSet_realization (H : HexData) :
                                                H.realization.outerSet = H.outerArcs
                                                source
                                                theorem Schoenflies.HexData.skeletonSet_realization (H : HexData) :
                                                H.realization.skeletonSet = H.outerArcs ∪ H.chordSet
                                                source
                                                theorem Schoenflies.HexData.nonboundary_realization (H : HexData) :
                                                H.realization.nonboundary = H.chordSet \ H.outerArcs

                                                The open nonboundary part is the crosscut without its two endpoints. With chord_meet this is the connectedness clause of def:admissible-graph in one line: an arc minus its endpoints is connected.

                                                source
                                                theorem Schoenflies.HexData.nonboundary_eq (H : HexData) :
                                                H.realization.nonboundary = H.chordSet \ {H.pos 1, H.pos 4}

                                                The open nonboundary part is the crosscut without its endpoints — the open arc.

                                                source
                                                theorem Schoenflies.HexData.isConnected_nonboundary (H : HexData) :
                                                IsConnected H.realization.nonboundary

                                                The open nonboundary part is connected — the last clause of def:admissible-graph. With a single crosscut it is the open arc of the chord, a continuous injective image of (0, 1).

                                                The initial skeleton is 2-connected #

                                                The first clause of def:admissible-graph. It is a fact about the abstract graph — a hexagon with one chord — and Graph.isTwoConnected_map_iff carries it to both realizations at once, so it is proved here and nowhere else. The chord plays no part: the hexagon alone is 2-connected, because deleting one of its vertices leaves a path. All the cyclic index arithmetic is decide.

                                                source
                                                theorem Schoenflies.connected_initSkel :
                                                initSkel.Connected

                                                The abstract hexagon-with-chord is connected.

                                                source
                                                theorem Schoenflies.deleteVert_connected_initSkel (k : Fin 6) :
                                                (initSkel.deleteVerts {InitialCell.vert k}).Connected

                                                Deleting one vertex of the hexagon leaves a path, hence a connected graph.

                                                source
                                                theorem Schoenflies.isTwoConnected_initSkel :
                                                initSkel.IsTwoConnected

                                                The initial skeleton is 2-connected — the first clause of def:admissible-graph.

                                                source
                                                theorem Schoenflies.HexData.isTwoConnected_graph (H : HexData) :
                                                H.realization.graph.IsTwoConnected

                                                Both drawn skeleta are 2-connected. By lem:combinatorial-invariance (a) there is only one statement to prove, and it is the abstract one.

                                                The target realization: the square with one straight chord #

                                                The target side of prop:initial-pair is completely explicit. The six marked points of S are the four corners together with u(a) = (α, 1) in the relative interior of the top side and u(b) = (β, -1) in the relative interior of the bottom side, |α|, |β| < 1. This is the one place the nonadjacency hypothesis is used: opposite sides, so the straight chord [(α,1), (β,-1)] has every point other than its ends of sup norm < 1, hence in the open square and off S.

                                                All seven edges are straight, so each is pinned by one coordinate and swept by the other, and the fifteen pairwise intersections are interval arithmetic. hPiece and vPiece are those two shapes.

                                                source
                                                theorem Schoenflies.Plane.eq_mk {p : Plane} {x y : ℝ} (h0 : p.ofLp 0 = x) (h1 : p.ofLp 1 = y) :
                                                p = mk x y

                                                Two plane points agree when their coordinates do.

                                                source
                                                theorem Schoenflies.Plane.mk_inj {x y x' y' : ℝ} (h : mk x y = mk x' y') :
                                                x = x' ∧ y = y'
                                                source
                                                def Schoenflies.hPiece (c lo hi : ℝ) :
                                                Set Plane

                                                A horizontal piece of the square boundary: second coordinate pinned, first coordinate sweeping an interval.

                                                Equations
                                                Instances For
                                                  source
                                                  def Schoenflies.vPiece (c lo hi : ℝ) :
                                                  Set Plane

                                                  A vertical piece of the square boundary.

                                                  Equations
                                                  Instances For
                                                    source
                                                    theorem Schoenflies.segment_eq_hPiece (c : ℝ) {lo hi : ℝ} (h : lo ≤ hi) :
                                                    segment ℝ (Plane.mk lo c) (Plane.mk hi c) = hPiece c lo hi
                                                    source
                                                    theorem Schoenflies.segment_eq_vPiece (c : ℝ) {lo hi : ℝ} (h : lo ≤ hi) :
                                                    segment ℝ (Plane.mk c lo) (Plane.mk c hi) = vPiece c lo hi
                                                    source
                                                    theorem Schoenflies.hPiece_subset_modelCurve {c lo hi : ℝ} (hc : |c| = 1) (hlo : -1 ≤ lo) (hhi : hi ≤ 1) :
                                                    hPiece c lo hi ⊆ modelCurve
                                                    source
                                                    theorem Schoenflies.vPiece_subset_modelCurve {c lo hi : ℝ} (hc : |c| = 1) (hlo : -1 ≤ lo) (hhi : hi ≤ 1) :
                                                    vPiece c lo hi ⊆ modelCurve
                                                    source
                                                    def Schoenflies.tgtPos (α β : ℝ) :
                                                    Fin 6 → Plane

                                                    The six marked points of S, in cyclic order: the corner (1,1), u(a) = (α,1), the corners (-1,1) and (-1,-1), u(b) = (β,-1), and the corner (1,-1).

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      source
                                                      noncomputable def Schoenflies.tgtOuter (α β : ℝ) (i : Fin 6) :
                                                      ℝ → Plane

                                                      The six outer edges of the target, straight.

                                                      Equations
                                                      Instances For
                                                        source
                                                        noncomputable def Schoenflies.tgtChord (α β : ℝ) :
                                                        ℝ → Plane

                                                        The straight chord [u(a), u(b)].

                                                        Equations
                                                        Instances For
                                                          source
                                                          theorem Schoenflies.tgtOuter_image (α β : ℝ) (i : Fin 6) :
                                                          tgtOuter α β i '' unitInterval = segment ℝ (tgtPos α β i) (tgtPos α β (i + 1))
                                                          source
                                                          theorem Schoenflies.tgtChord_image (α β : ℝ) :
                                                          tgtChord α β '' unitInterval = segment ℝ (Plane.mk α 1) (Plane.mk β (-1))
                                                          source
                                                          theorem Schoenflies.segment_tgtPos {α β : ℝ} (hα : |α| < 1) (hβ : |β| < 1) (i : Fin 6) :
                                                          segment ℝ (tgtPos α β i) (tgtPos α β (i + 1)) = ![hPiece 1 α 1, hPiece 1 (-1) α, vPiece (-1) (-1) 1, hPiece (-1) (-1) β, hPiece (-1) β 1, vPiece 1 (-1) 1] i

                                                          The six target arcs, in the pinned-coordinate normal form.

                                                          source
                                                          theorem Schoenflies.injective_tgtPos {α β : ℝ} (hα : |α| < 1) (hβ : |β| < 1) :
                                                          Function.Injective (tgtPos α β)
                                                          source
                                                          theorem Schoenflies.tgtOuter_subset_modelCurve {α β : ℝ} (hα : |α| < 1) (hβ : |β| < 1) (i : Fin 6) :
                                                          tgtOuter α β i '' unitInterval ⊆ modelCurve
                                                          source
                                                          theorem Schoenflies.tgtOuter_meet {α β : ℝ} (hα : |α| < 1) (hβ : |β| < 1) (i j : Fin 6) (hij : i ≠ j) :
                                                          tgtOuter α β i '' unitInterval ∩ tgtOuter α β j '' unitInterval ⊆ {tgtPos α β i, tgtPos α β (i + 1)} ∩ {tgtPos α β j, tgtPos α β (j + 1)}

                                                          The fifteen pairwise intersections of the six target edges. Two edges on the same side of the square overlap in at most the marked point between them; two on adjacent sides meet at most in the corner they share, and the four cases where a corner is not on the piece in question are empty because |α|, |β| < 1; two on opposite sides never meet. Every one of them is a comparison of two real intervals.

                                                          source
                                                          theorem Schoenflies.openSegment_chord_supNorm_lt {α β : ℝ} (hα : |α| < 1) (hβ : |β| < 1) (p : Plane) :
                                                          p ∈ openSegment ℝ (Plane.mk α 1) (Plane.mk β (-1)) → p.supNorm < 1

                                                          The straight chord between opposite sides has all its other points in the open square. This is the single use of the nonadjacency hypothesis of prop:initial-pair.

                                                          source
                                                          theorem Schoenflies.openSegment_chord_notMem_modelCurve {α β : ℝ} (hα : |α| < 1) (hβ : |β| < 1) (p : Plane) :
                                                          p ∈ openSegment ℝ (Plane.mk α 1) (Plane.mk β (-1)) → p ∉ modelCurve
                                                          source
                                                          theorem Schoenflies.tgtChord_meet {α β : ℝ} (hα : |α| < 1) (hβ : |β| < 1) (i : Fin 6) :
                                                          tgtChord α β '' unitInterval ∩ tgtOuter α β i '' unitInterval ⊆ {tgtPos α β 1, tgtPos α β 4}

                                                          The chord meets each outer edge only at its own two ends.

                                                          source
                                                          theorem Schoenflies.tgtOuter_image_eq {α β : ℝ} (hα : |α| < 1) (hβ : |β| < 1) (i : Fin 6) :
                                                          tgtOuter α β i '' unitInterval = ![hPiece 1 α 1, hPiece 1 (-1) α, vPiece (-1) (-1) 1, hPiece (-1) (-1) β, hPiece (-1) β 1, vPiece 1 (-1) 1] i
                                                          source
                                                          theorem Schoenflies.iUnion_tgtOuter {α β : ℝ} (hα : |α| < 1) (hβ : |β| < 1) :
                                                          ⋃ (i : Fin 6), tgtOuter α β i '' unitInterval = modelCurve

                                                          The six target edges cover S. Each side of the square is one piece, except the top and the bottom, which are cut in two at u(a) and u(b).

                                                          source
                                                          theorem Schoenflies.tgtPos_mem_modelCurve {α β : ℝ} (hα : |α| < 1) (hβ : |β| < 1) (i : Fin 6) :
                                                          tgtPos α β i ∈ modelCurve
                                                          source
                                                          theorem Schoenflies.tgtPos_succ_ne {α β : ℝ} (hα : |α| < 1) (hβ : |β| < 1) (i : Fin 6) :
                                                          tgtPos α β i ≠ tgtPos α β (i + 1)
                                                          source
                                                          noncomputable def Schoenflies.targetHex {α β : ℝ} (hα : |α| < 1) (hβ : |β| < 1) :
                                                          HexData

                                                          The target realization of prop:initial-pair: the square S, subdivided at its four corners and at u(a) = (α,1), u(b) = (β,-1), together with the straight chord between the last two.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            source
                                                            @[simp]
                                                            theorem Schoenflies.targetHex_pos {α β : ℝ} (hα : |α| < 1) (hβ : |β| < 1) :
                                                            (targetHex hα hβ).pos = tgtPos α β
                                                            source
                                                            @[simp]
                                                            theorem Schoenflies.targetHex_outer {α β : ℝ} (hα : |α| < 1) (hβ : |β| < 1) :
                                                            (targetHex hα hβ).outer = tgtOuter α β
                                                            source
                                                            @[simp]
                                                            theorem Schoenflies.targetHex_chordParam {α β : ℝ} (hα : |α| < 1) (hβ : |β| < 1) :
                                                            (targetHex hα hβ).chordParam = tgtChord α β
                                                            source
                                                            theorem Schoenflies.targetHex_outerArcs {α β : ℝ} (hα : |α| < 1) (hβ : |β| < 1) :
                                                            (targetHex hα hβ).outerArcs = modelCurve

                                                            The target outer cycle is exactly S.

                                                            The source realization: the curve with one polygonal crosscut #

                                                            The source realization is the pushforward of the target's outer cycle along w = u⁻¹, together with the polygonal crosscut P as its seventh edge. Nothing about the six outer arcs has to be proved again: w is injective on S, so each of the three drawing conditions transfers.

                                                            The crosscut arrives as a parametrization together with the one geometric fact lem:accessible- endpoints supplies — that every point of it other than its two ends lies in D — from which P ∩ C = {a, b} follows, and with it the last meeting condition.

                                                            source
                                                            noncomputable def Schoenflies.sourceHex {α β : ℝ} {C : Set Plane} {u w : Plane → Plane} {sp : ℝ → Plane} (hw : IsSetHomeoOn u w C modelCurve) (hα : |α| < 1) (hβ : |β| < 1) (hspc : ContinuousOn sp unitInterval) (hspi : Set.InjOn sp unitInterval) (hsp0 : sp 0 = w (tgtPos α β 1)) (hsp1 : sp 1 = w (tgtPos α β 4)) (hspin : sp '' unitInterval \ {w (tgtPos α β 1), w (tgtPos α β 4)} ⊆ inside C) :
                                                            HexData

                                                            The source realization of prop:initial-pair: C, subdivided at the u-preimages of the four corners and of u(a), u(b), together with the polygonal crosscut P from a to b.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              source
                                                              @[simp]
                                                              theorem Schoenflies.sourceHex_pos {α β : ℝ} {C : Set Plane} {u w : Plane → Plane} {sp : ℝ → Plane} (hw : IsSetHomeoOn u w C modelCurve) (hα : |α| < 1) (hβ : |β| < 1) (hspc : ContinuousOn sp unitInterval) (hspi : Set.InjOn sp unitInterval) (hsp0 : sp 0 = w (tgtPos α β 1)) (hsp1 : sp 1 = w (tgtPos α β 4)) (hspin : sp '' unitInterval \ {w (tgtPos α β 1), w (tgtPos α β 4)} ⊆ inside C) :
                                                              (sourceHex hw hα hβ hspc hspi hsp0 hsp1 hspin).pos = fun (i : Fin 6) => w (tgtPos α β i)
                                                              source
                                                              @[simp]
                                                              theorem Schoenflies.sourceHex_chordParam {α β : ℝ} {C : Set Plane} {u w : Plane → Plane} {sp : ℝ → Plane} (hw : IsSetHomeoOn u w C modelCurve) (hα : |α| < 1) (hβ : |β| < 1) (hspc : ContinuousOn sp unitInterval) (hspi : Set.InjOn sp unitInterval) (hsp0 : sp 0 = w (tgtPos α β 1)) (hsp1 : sp 1 = w (tgtPos α β 4)) (hspin : sp '' unitInterval \ {w (tgtPos α β 1), w (tgtPos α β 4)} ⊆ inside C) :
                                                              (sourceHex hw hα hβ hspc hspi hsp0 hsp1 hspin).chordParam = sp
                                                              source
                                                              theorem Schoenflies.sourceHex_outerArcs {α β : ℝ} {C : Set Plane} {u w : Plane → Plane} {sp : ℝ → Plane} (hw : IsSetHomeoOn u w C modelCurve) (hα : |α| < 1) (hβ : |β| < 1) (hspc : ContinuousOn sp unitInterval) (hspi : Set.InjOn sp unitInterval) (hsp0 : sp 0 = w (tgtPos α β 1)) (hsp1 : sp 1 = w (tgtPos α β 4)) (hspin : sp '' unitInterval \ {w (tgtPos α β 1), w (tgtPos α β 4)} ⊆ inside C) :
                                                              (sourceHex hw hα hβ hspc hspi hsp0 hsp1 hspin).outerArcs = C

                                                              The source outer cycle is exactly C.

                                                              The skeleton homeomorphism #

                                                              g is u on C and a chosen homeomorphism P → [u(a), u(b)] on the crosscut. The chosen homeomorphism is the one that matches the parameters: sp t ↦ [u(a), u(b)](t). The two definitions agree at a and b, which is where C and P meet, so the pasting lemma applies to the two closed pieces of the skeleton.

                                                              source
                                                              theorem Schoenflies.continuousOn_invFunOn_image {f : ℝ → Plane} {s : Set ℝ} (hs : IsCompact s) (hf : ContinuousOn f s) (hinj : Set.InjOn f s) :
                                                              ContinuousOn (Function.invFunOn f s) (f '' s)

                                                              A continuous injection of a compact set has a continuous inverse on its image. Stated for the set-level Function.invFunOn, which is what a parametrized arc has to be inverted with.

                                                              The initial matched pair, bundled #

                                                              InitialData C is the data prop:initial-pair produces before any of its conclusions are drawn: the boundary homeomorphism u with its inverse w, the two abscissae xa, xb of u(a) and u(b) on the two opposite sides, and the polygonal crosscut as a parametrization. Both realizations, the skeleton homeomorphism, and every conclusion below are functions of it.

                                                              source
                                                              structure Schoenflies.InitialData (C : Set Plane) :
                                                              Type

                                                              The data of an initial matched pair over the Jordan curve C.

                                                              Instances For
                                                                source
                                                                def Schoenflies.InitialData.a {C : Set Plane} (d : InitialData C) :
                                                                Plane

                                                                The first chosen boundary point, a = u⁻¹(xa, 1).

                                                                Equations
                                                                Instances For
                                                                  source
                                                                  def Schoenflies.InitialData.b {C : Set Plane} (d : InitialData C) :
                                                                  Plane

                                                                  The second chosen boundary point, b = u⁻¹(xb, -1).

                                                                  Equations
                                                                  Instances For
                                                                    source
                                                                    def Schoenflies.InitialData.crossSet {C : Set Plane} (d : InitialData C) :
                                                                    Set Plane

                                                                    The polygonal crosscut P, as a set.

                                                                    Equations
                                                                    Instances For
                                                                      source
                                                                      noncomputable def Schoenflies.InitialData.src {C : Set Plane} (d : InitialData C) :
                                                                      HexData

                                                                      The source realization data.

                                                                      Equations
                                                                      Instances For
                                                                        source
                                                                        noncomputable def Schoenflies.InitialData.tgt {C : Set Plane} (d : InitialData C) :
                                                                        HexData

                                                                        The target realization data.

                                                                        Equations
                                                                        Instances For
                                                                          source
                                                                          noncomputable def Schoenflies.InitialData.sourceRealization {C : Set Plane} (d : InitialData C) :
                                                                          initialStructure.Realization

                                                                          The source realization of initialStructure — Γ of prop:initial-pair.

                                                                          Equations
                                                                          Instances For
                                                                            source
                                                                            noncomputable def Schoenflies.InitialData.targetRealization {C : Set Plane} (d : InitialData C) :
                                                                            initialStructure.Realization

                                                                            The target realization of initialStructure — Γ' of prop:initial-pair.

                                                                            Equations
                                                                            Instances For
                                                                              source
                                                                              @[simp]
                                                                              theorem Schoenflies.InitialData.src_pos_one {C : Set Plane} (d : InitialData C) :
                                                                              d.src.pos 1 = d.a
                                                                              source
                                                                              @[simp]
                                                                              theorem Schoenflies.InitialData.src_pos_four {C : Set Plane} (d : InitialData C) :
                                                                              d.src.pos 4 = d.b
                                                                              source
                                                                              @[simp]
                                                                              theorem Schoenflies.InitialData.src_chordSet {C : Set Plane} (d : InitialData C) :
                                                                              d.src.chordSet = d.crossSet
                                                                              source
                                                                              @[simp]
                                                                              theorem Schoenflies.InitialData.tgt_pos_one {C : Set Plane} (d : InitialData C) :
                                                                              d.tgt.pos 1 = Plane.mk d.xa 1
                                                                              source
                                                                              @[simp]
                                                                              theorem Schoenflies.InitialData.tgt_pos_four {C : Set Plane} (d : InitialData C) :
                                                                              d.tgt.pos 4 = Plane.mk d.xb (-1)
                                                                              source
                                                                              theorem Schoenflies.InitialData.tgt_chordSet {C : Set Plane} (d : InitialData C) :
                                                                              d.tgt.chordSet = segment ℝ (Plane.mk d.xa 1) (Plane.mk d.xb (-1))
                                                                              source
                                                                              theorem Schoenflies.InitialData.src_outerArcs {C : Set Plane} (d : InitialData C) :
                                                                              d.src.outerArcs = C
                                                                              source
                                                                              theorem Schoenflies.InitialData.tgt_outerArcs {C : Set Plane} (d : InitialData C) :
                                                                              d.tgt.outerArcs = modelCurve
                                                                              source
                                                                              theorem Schoenflies.InitialData.a_mem {C : Set Plane} (d : InitialData C) :
                                                                              d.a ∈ C
                                                                              source
                                                                              theorem Schoenflies.InitialData.b_mem {C : Set Plane} (d : InitialData C) :
                                                                              d.b ∈ C
                                                                              source
                                                                              theorem Schoenflies.InitialData.u_a {C : Set Plane} (d : InitialData C) :
                                                                              d.u (d.w (tgtPos d.xa d.xb 1)) = tgtPos d.xa d.xb 1
                                                                              source
                                                                              theorem Schoenflies.InitialData.u_b {C : Set Plane} (d : InitialData C) :
                                                                              d.u (d.w (tgtPos d.xa d.xb 4)) = tgtPos d.xa d.xb 4
                                                                              source
                                                                              @[simp]
                                                                              theorem Schoenflies.InitialData.u_apply_a {C : Set Plane} (d : InitialData C) :
                                                                              d.u d.a = Plane.mk d.xa 1
                                                                              source
                                                                              @[simp]
                                                                              theorem Schoenflies.InitialData.u_apply_b {C : Set Plane} (d : InitialData C) :
                                                                              d.u d.b = Plane.mk d.xb (-1)
                                                                              source
                                                                              theorem Schoenflies.InitialData.sourceRealization_skeletonSet {C : Set Plane} (d : InitialData C) :
                                                                              d.sourceRealization.skeletonSet = C ∪ d.crossSet
                                                                              source
                                                                              theorem Schoenflies.InitialData.targetRealization_skeletonSet {C : Set Plane} (d : InitialData C) :
                                                                              d.targetRealization.skeletonSet = modelCurve ∪ d.tgt.chordSet
                                                                              source
                                                                              theorem Schoenflies.InitialData.sourceRealization_outerSet {C : Set Plane} (d : InitialData C) :
                                                                              d.sourceRealization.outerSet = C
                                                                              source
                                                                              theorem Schoenflies.InitialData.targetRealization_outerSet {C : Set Plane} (d : InitialData C) :
                                                                              d.targetRealization.outerSet = modelCurve
                                                                              source
                                                                              theorem Schoenflies.InitialData.isConnected_sourceRealization_nonboundary {C : Set Plane} (d : InitialData C) :
                                                                              IsConnected d.sourceRealization.nonboundary
                                                                              source
                                                                              theorem Schoenflies.InitialData.isConnected_targetRealization_nonboundary {C : Set Plane} (d : InitialData C) :
                                                                              IsConnected d.targetRealization.nonboundary
                                                                              source
                                                                              theorem Schoenflies.InitialData.isTwoConnected_sourceRealization {C : Set Plane} (d : InitialData C) :
                                                                              d.sourceRealization.graph.IsTwoConnected
                                                                              source
                                                                              theorem Schoenflies.InitialData.isTwoConnected_targetRealization {C : Set Plane} (d : InitialData C) :
                                                                              d.targetRealization.graph.IsTwoConnected

                                                                              a and b are the only points the crosscut shares with the curve #

                                                                              source
                                                                              theorem Schoenflies.InitialData.cross_mem_curve_iff {C : Set Plane} (d : InitialData C) {t : ℝ} (ht : t ∈ unitInterval) :
                                                                              d.cross t ∈ C ↔ t = 0 ∨ t = 1
                                                                              source
                                                                              theorem Schoenflies.InitialData.crossSet_inter_curve {C : Set Plane} (d : InitialData C) :
                                                                              d.crossSet ∩ C = {d.a, d.b}

                                                                              The map #

                                                                              source
                                                                              noncomputable def Schoenflies.InitialData.skelMap {C : Set Plane} (d : InitialData C) :
                                                                              Plane → Plane

                                                                              The skeleton map: u on the curve, and the parameter-matching homeomorphism from the crosscut onto the straight chord.

                                                                              Equations
                                                                              Instances For
                                                                                source
                                                                                noncomputable def Schoenflies.InitialData.skelInv {C : Set Plane} (d : InitialData C) :
                                                                                Plane → Plane

                                                                                Its inverse: w on the model curve, and the parameter-matching homeomorphism back.

                                                                                Equations
                                                                                Instances For
                                                                                  source
                                                                                  theorem Schoenflies.InitialData.skelMap_of_mem {C : Set Plane} (d : InitialData C) {x : Plane} (hx : x ∈ C) :
                                                                                  d.skelMap x = d.u x
                                                                                  source
                                                                                  theorem Schoenflies.InitialData.skelInv_of_mem {C : Set Plane} (d : InitialData C) {y : Plane} (hy : y ∈ modelCurve) :
                                                                                  d.skelInv y = d.w y
                                                                                  source
                                                                                  theorem Schoenflies.InitialData.skelMap_cross {C : Set Plane} (d : InitialData C) {t : ℝ} (ht : t ∈ unitInterval) :
                                                                                  d.skelMap (d.cross t) = tgtChord d.xa d.xb t

                                                                                  The skeleton map matches parameters on the crosscut.

                                                                                  source
                                                                                  theorem Schoenflies.InitialData.tgtChord_mem_modelCurve_iff {C : Set Plane} (d : InitialData C) {t : ℝ} (ht : t ∈ unitInterval) :
                                                                                  tgtChord d.xa d.xb t ∈ modelCurve ↔ t = 0 ∨ t = 1
                                                                                  source
                                                                                  theorem Schoenflies.InitialData.injOn_tgtChord {C : Set Plane} (d : InitialData C) :
                                                                                  Set.InjOn (tgtChord d.xa d.xb) unitInterval
                                                                                  source
                                                                                  theorem Schoenflies.InitialData.skelInv_tgtChord {C : Set Plane} (d : InitialData C) {t : ℝ} (ht : t ∈ unitInterval) :
                                                                                  d.skelInv (tgtChord d.xa d.xb t) = d.cross t

                                                                                  Continuity and inversion #

                                                                                  source
                                                                                  theorem Schoenflies.InitialData.continuousOn_skelMap {C : Set Plane} (d : InitialData C) :
                                                                                  ContinuousOn d.skelMap d.sourceRealization.skeletonSet
                                                                                  source
                                                                                  theorem Schoenflies.InitialData.continuousOn_skelInv {C : Set Plane} (d : InitialData C) :
                                                                                  ContinuousOn d.skelInv d.targetRealization.skeletonSet
                                                                                  source
                                                                                  theorem Schoenflies.InitialData.leftInvOn_skel {C : Set Plane} (d : InitialData C) :
                                                                                  Set.LeftInvOn d.skelInv d.skelMap d.sourceRealization.skeletonSet
                                                                                  source
                                                                                  theorem Schoenflies.InitialData.rightInvOn_skel {C : Set Plane} (d : InitialData C) :
                                                                                  Set.RightInvOn d.skelInv d.skelMap d.targetRealization.skeletonSet
                                                                                  source
                                                                                  noncomputable def Schoenflies.InitialData.skeletonHomeo {C : Set Plane} (d : InitialData C) :
                                                                                  CellStructure.SkeletonHomeo d.sourceRealization d.targetRealization

                                                                                  The skeleton homeomorphism g of def:matched-pair. It is u on the outer cycle (clause 2), and on the crosscut it is the chosen homeomorphism P → [u(a), u(b)] matching endpoints (clause 3); clause 1 is definitional here, both realizations being realizations of the one initialStructure.

                                                                                  Equations
                                                                                  • d.skeletonHomeo = { toFun := d.skelMap, invFun := d.skelInv, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯, leftInvOn := ⋯, rightInvOn := ⋯, pos_apply := ⋯, edgeArc_image := ⋯ }
                                                                                  Instances For
                                                                                    source
                                                                                    @[simp]
                                                                                    theorem Schoenflies.InitialData.skeletonHomeo_toFun {C : Set Plane} (d : InitialData C) :
                                                                                    d.skeletonHomeo.toFun = d.skelMap
                                                                                    source
                                                                                    theorem Schoenflies.InitialData.skeletonHomeo_eq_u {C : Set Plane} (d : InitialData C) {x : Plane} (hx : x ∈ C) :
                                                                                    d.skeletonHomeo.toFun x = d.u x

                                                                                    Clause 2 of def:matched-pair: g = u on C.

                                                                                    source
                                                                                    theorem Schoenflies.InitialData.skeletonHomeo_cross {C : Set Plane} (d : InitialData C) {t : ℝ} (ht : t ∈ unitInterval) :
                                                                                    d.skeletonHomeo.toFun (d.cross t) = tgtChord d.xa d.xb t

                                                                                    Clause 3 of def:matched-pair for the crosscut: the chosen homeomorphism P → [u(a), u(b)] matches the two parametrizations, hence the endpoints.

                                                                                    The two 2-cells really are the two sides of the crosscut #

                                                                                    thm:general-crosscut applied on each side. On the source side the collar hypothesis HasArcCollars (inside C) P is carried, since P is an arbitrary polygonal crosscut; on the target side the chord is straight, so Schoenflies.hasArcCollars_segment discharges it outright.

                                                                                    source
                                                                                    theorem Schoenflies.InitialData.isCrosscut {C : Set Plane} (d : InitialData C) :
                                                                                    IsCrosscut C d.crossSet d.a d.b

                                                                                    P is a crosscut of D — the configuration thm:general-crosscut consumes.

                                                                                    source
                                                                                    theorem Schoenflies.InitialData.isCutPair {C : Set Plane} (d : InitialData C) :
                                                                                    IsCutPair C d.a d.b (d.src.arcOf false) (d.src.arcOf true)

                                                                                    A₁, A₂ are the two arcs of C from a to b. They are the geometric unions of the two boundary edge-paths B₁, B₂ of the abstract structure.

                                                                                    source
                                                                                    theorem Schoenflies.InitialData.sourceRealization_cell_face {C : Set Plane} (d : InitialData C) (k : Bool) :
                                                                                    d.sourceRealization.cell (InitialCell.face k) = inside (d.src.arcOf k ∪ d.crossSet)
                                                                                    source
                                                                                    theorem Schoenflies.InitialData.source_cells_cover {C : Set Plane} (d : InitialData C) (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) (hcollars : HasArcCollars (inside C) d.crossSet) :
                                                                                    inside C \ d.crossSet = d.sourceRealization.cell (InitialCell.face false) ∪ d.sourceRealization.cell (InitialCell.face true)

                                                                                    The two source 2-cells exhaust D ∖ P — thm:general-crosscut, first sentence.

                                                                                    source
                                                                                    theorem Schoenflies.InitialData.source_cell_isComponent {C : Set Plane} (d : InitialData C) (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) (k : Bool) (z : Plane) :
                                                                                    z ∈ d.sourceRealization.cell (InitialCell.face k) → connectedComponentIn (inside C \ d.crossSet) z = d.sourceRealization.cell (InitialCell.face k)

                                                                                    Each source 2-cell is a component of D ∖ P.

                                                                                    source
                                                                                    theorem Schoenflies.InitialData.source_closure_cell_inter {C : Set Plane} (d : InitialData C) (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) (k : Bool) :
                                                                                    closure (d.sourceRealization.cell (InitialCell.face k)) ∩ C = d.src.arcOf k

                                                                                    The labelling of the two source 2-cells: the closure of Rₖ meets C exactly in Aₖ. This is what makes k ↦ face k the correspondence lem:crosscut-side-correspondence asks for.

                                                                                    source
                                                                                    theorem Schoenflies.InitialData.source_cells_ne {C : Set Plane} (d : InitialData C) (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) :
                                                                                    d.sourceRealization.cell (InitialCell.face false) ≠ d.sourceRealization.cell (InitialCell.face true)

                                                                                    The target side #

                                                                                    source
                                                                                    theorem Schoenflies.InitialData.openSquare_subset_inside_modelCurve :
                                                                                    Plane.openSquare 0 1 ⊆ inside modelCurve

                                                                                    The open square is the bounded region of the model curve: it is open, convex and bounded, and its frontier is contained in S.

                                                                                    source
                                                                                    theorem Schoenflies.InitialData.isCrosscutTarget {C : Set Plane} (d : InitialData C) :
                                                                                    IsCrosscut modelCurve d.tgt.chordSet (Plane.mk d.xa 1) (Plane.mk d.xb (-1))

                                                                                    The straight chord is a crosscut of the open square.

                                                                                    source
                                                                                    theorem Schoenflies.InitialData.isCutPairTarget {C : Set Plane} (d : InitialData C) :
                                                                                    IsCutPair modelCurve (Plane.mk d.xa 1) (Plane.mk d.xb (-1)) (d.tgt.arcOf false) (d.tgt.arcOf true)

                                                                                    u(A₁), u(A₂) are the two arcs of S from u(a) to u(b).

                                                                                    source
                                                                                    theorem Schoenflies.InitialData.hasArcCollarsTarget {C : Set Plane} (d : InitialData C) :
                                                                                    HasArcCollars (inside modelCurve) d.tgt.chordSet

                                                                                    The collar hypothesis is not needed on the target side: the chord is a segment.

                                                                                    source
                                                                                    theorem Schoenflies.InitialData.targetRealization_cell_face {C : Set Plane} (d : InitialData C) (k : Bool) :
                                                                                    d.targetRealization.cell (InitialCell.face k) = inside (d.tgt.arcOf k ∪ d.tgt.chordSet)
                                                                                    source
                                                                                    theorem Schoenflies.InitialData.target_cells_cover {C : Set Plane} (d : InitialData C) (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) :
                                                                                    inside modelCurve \ d.tgt.chordSet = d.targetRealization.cell (InitialCell.face false) ∪ d.targetRealization.cell (InitialCell.face true)

                                                                                    The two target 2-cells exhaust Q° ∖ [u(a), u(b)].

                                                                                    source
                                                                                    theorem Schoenflies.InitialData.target_closure_cell_inter {C : Set Plane} (d : InitialData C) (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) (k : Bool) :
                                                                                    closure (d.targetRealization.cell (InitialCell.face k)) ∩ modelCurve = d.tgt.arcOf k

                                                                                    The labelling of the two target 2-cells.

                                                                                    prop:initial-pair: an initial matched pair exists #

                                                                                    The two open corner arcs the blueprint chooses a and b from are the relative interiors of two opposite sides of the square, pulled back by u. They are relatively open in C and nonempty, so the countable dense set of strongly accessible points of prop:countable-strong-access meets both; lem:tangent-cone and lem:accessible-endpoints then supply the polygonal crosscut.

                                                                                    source
                                                                                    def Schoenflies.openTop :
                                                                                    Set Plane

                                                                                    The relative interior of the top side of the square.

                                                                                    Equations
                                                                                    Instances For
                                                                                      source
                                                                                      def Schoenflies.openBottom :
                                                                                      Set Plane

                                                                                      The relative interior of the bottom side — the side opposite the top one.

                                                                                      Equations
                                                                                      Instances For
                                                                                        source
                                                                                        theorem Schoenflies.isOpen_topBand :
                                                                                        IsOpen {p : Plane | |p.ofLp 0| < 1 ∧ 0 < p.ofLp 1}
                                                                                        source
                                                                                        theorem Schoenflies.isOpen_bottomBand :
                                                                                        IsOpen {p : Plane | |p.ofLp 0| < 1 ∧ p.ofLp 1 < 0}
                                                                                        source
                                                                                        theorem Schoenflies.mem_openTop {p : Plane} :
                                                                                        p ∈ openTop ↔ p.ofLp 1 = 1 ∧ |p.ofLp 0| < 1
                                                                                        source
                                                                                        theorem Schoenflies.mem_openBottom {p : Plane} :
                                                                                        p ∈ openBottom ↔ p.ofLp 1 = -1 ∧ |p.ofLp 0| < 1
                                                                                        source
                                                                                        theorem Schoenflies.openTop_nonempty :
                                                                                        openTop.Nonempty
                                                                                        source
                                                                                        theorem Schoenflies.openBottom_nonempty :
                                                                                        openBottom.Nonempty
                                                                                        source
                                                                                        theorem Schoenflies.exists_mem_inter_of_dense {C A U W : Set Plane} (hAC : A ⊆ C) (hdense : C ⊆ closure A) (hW : IsOpen W) (hU : U = W ∩ C) (hne : U.Nonempty) :
                                                                                        (A ∩ U).Nonempty

                                                                                        A dense subset of C meets every nonempty relatively open subset of C.

                                                                                        source
                                                                                        theorem Schoenflies.exists_initialData {C : Set Plane} (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) (hC : IsJordanCurve C) :
                                                                                        Nonempty (InitialData C)

                                                                                        prop:initial-pair. Every Jordan curve carries an initial matched pair: a common abstract cell structure with an admissible realization in C ∪ D — C subdivided at the u-preimages of the four corners and at two strongly accessible points a, b of nonadjacent corner arcs, together with a polygonal crosscut of D from a to b — and an admissible realization in Q, namely S correspondingly subdivided together with the straight chord [u(a), u(b)].

                                                                                        harc is thm:arc-complement, the standing hypothesis of thm:jordan in this library.

                                                                                        source
                                                                                        theorem Schoenflies.initial_pair {C : Set Plane} (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) (hC : IsJordanCurve C) :
                                                                                        ∃ (d : InitialData C), d.sourceRealization.graph.IsTwoConnected ∧ d.targetRealization.graph.IsTwoConnected ∧ d.sourceRealization.outerSet = C ∧ d.targetRealization.outerSet = modelCurve ∧ IsConnected d.sourceRealization.nonboundary ∧ IsConnected d.targetRealization.nonboundary ∧ IsPolygonal d.crossSet ∧ d.tgt.chordSet = segment ℝ (d.u d.a) (d.u d.b) ∧ ∀ x ∈ C, d.skeletonHomeo.toFun x = d.u x

                                                                                        prop:initial-pair, assembled. There is a matched pair whose source realization is C subdivided at the u-preimages of the four corners of Q and at two further points a, b of the countable dense strongly accessible set lying in two nonadjacent corner arcs, together with one polygonal crosscut of D from a to b, and whose target realization is S correspondingly subdivided together with the straight chord [u(a), u(b)].

                                                                                        Both realizations realize the one Schoenflies.initialStructure, so clause 1 of def:matched-pair is definitional; clause 2 is the last conjunct; clause 3 is InitialData.skeletonHomeo together with InitialData.skeletonHomeo_cross. Admissibility (def:admissible-graph) is the first six conjuncts.

                                                                                        Everything here is available separately, as a function of the InitialData produced: this bundle exists so that the blueprint statement appears once, in one place. def:generated- structure builds every later stage from InitialData.sourceRealization, InitialData.targetRealization and InitialData.skeletonHomeo, and needs them as data, not as the content of an existential.