OAI/Combinatorics/PlanarL1/Stem.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarL1.Topology.segment_split line 12
2. lemma OAI.PlanarL1.Topology.convex_frontier_segment_at line 43
3. lemma OAI.PlanarL1.Topology.ExteriorPorts.spoke_intersection line 62
4. lemma OAI.PlanarL1.Topology.ExteriorPorts.spoke_disjoint line 72
5. def OAI.PlanarL1.Topology.ExteriorPorts.restrict line 80
6. lemma OAI.PlanarL1.Topology.ExteriorPorts.obstacles_closed line 88
7. lemma OAI.PlanarL1.Topology.SegmentChain.piece_subset_trace line 97
8. lemma OAI.PlanarL1.Topology.SegmentChain.first_segment_subset line 102
9. lemma OAI.PlanarL1.Topology.SegmentChain.cut_not_start line 105
10. lemma OAI.PlanarL1.Topology.SegmentChain.cut_not_next line 113
11. lemma OAI.PlanarL1.Topology.SegmentChain.cut_avoids_start line 123
12. lemma OAI.PlanarL1.Topology.SegmentChain.exit_frontier line 142

    Source documentation

    A literal cut of the first polygonal piece at the boundary of a convex neighborhood. All of the residual path is outside, except for that port.

    lemma exit_frontier (hP : P.IsSimple) {T : Set ℂ} (hT : Convex ℝ T) (hop : IsOpen T)
        (hx : x∈T) (htail : Disjoint (closure T) P.tail.trace) :
        ∃ q : ℂ, ∃ hq : q∈segment ℝ x (P.vertex 1),
          q∈frontier T ∧ q≠P.vertex 1 ∧ q≠x ∧
          (∀ z∈(P.cutFirst q hq).trace, z∈closure T → z=q) := by
    …

    Mentions: OAI.PlanarL1.Topology.SegmentChain.trace

13. structure OAI.PlanarL1.Topology.DiskCore line 184

    Source documentation

    A literal finite polyline core in a bounded convex disk, with specified leaf ports on its boundary. These data are constructed by the surgeries.

    structure DiskCore (G : SimpleGraph V) (B : Set V) where
    …

14. def OAI.PlanarL1.Topology.DiskCore.restrict line 199
15. lemma OAI.PlanarL1.Topology.DiskCore.spoke_subset line 202
16. lemma OAI.PlanarL1.Topology.DiskCore.align line 207

    Source documentation

    Align the first residual piece with a new disk center, without consuming any bend. A thin capsule avoids every other stem and the fixed obstacle.

    lemma align [Finite V] {target : V → ℂ}
        (E : ExteriorPorts C.drawing.point target B C.disk)
        (hleaf : ∀ w∈B, ∀ u u', G.Adj w u → G.Adj w u' → u=u')
        {v : V} (hv : v∈B) {K : Set ℂ} (hK : IsClosed K)
        (hCK : Disjoint (closure C.disk) K)
        {n : ℕ} (P : SegmentChain (E.region v) (C.drawing.point v) (target v) (n+1))
        (hP : P.IsSimple) :
        ∃ C' : DiskCore G B,
        ∃ E' : ExteriorPorts C'.drawing.point target B C'.disk,
        ∃ P' : SegmentChain (E'.region v) (C'.drawing.point v) (target v) (n+1),
          P'.IsSimple ∧ C'.drawing.point v∈segment ℝ C'.center (P'.vertex 1) ∧
          Disjoint (closure C'.disk) K ∧
    …

    Mentions: OAI.PlanarL1.Topology.ExteriorPorts, OAI.PlanarL1.Topology.SegmentChain, OAI.PlanarL1.Topology.DiskCore

17. lemma OAI.PlanarL1.Topology.DiskCore.finish_stem line 298
18. lemma OAI.PlanarL1.Topology.DiskCore.bend_stem line 357

    Source documentation

    Consuming one radial piece and cutting the next strictly decreases the number of residual polygonal pieces. All other external stems remain disjoint.

    lemma bend_stem (E : ExteriorPorts C.drawing.point target B C.disk)
        (hleaf : ∀ w∈B, ∀ u u', G.Adj w u → G.Adj w u' → u=u')
        {v : V} (hv : v∈B) {K : Set ℂ} (hK : IsClosed K)
        (hCK : Disjoint (closure C.disk) K)
        (hEK : ∀ z∈E.region v, z∈K → z=target v)
        {n : ℕ} (P : SegmentChain (E.region v) (C.drawing.point v) (target v) (n+1+1))
        (hP : P.IsSimple) (hrad : C.drawing.point v∈segment ℝ C.center (P.vertex 1)) :
        ∃ C' : DiskCore G B,
        ∃ E' : ExteriorPorts C'.drawing.point target B C'.disk,
        ∃ P' : SegmentChain (E'.region v) (C'.drawing.point v) (target v) (n+1),
          P'.IsSimple ∧ C'.drawing.point v∈segment ℝ C'.center (P'.vertex 1) ∧
          Disjoint (closure C'.disk) K ∧
    …

    Mentions: OAI.PlanarL1.Topology.ExteriorPorts, OAI.PlanarL1.Topology.SegmentChain, OAI.PlanarL1.Topology.DiskCore

19. lemma OAI.PlanarL1.Topology.DiskCore.absorb_radial line 479

    Source documentation

    A radial initial piece plus the finitely many bends of a simple polygonal stem can be swallowed while the other stems remain genuine exterior routes.

    lemma absorb_radial (E : ExteriorPorts C.drawing.point target B C.disk)
        (hleaf : ∀ w∈B, ∀ u u', G.Adj w u → G.Adj w u' → u=u')
        {v : V} (hv : v∈B) {K : Set ℂ} (hK : IsClosed K)
        (hCK : Disjoint (closure C.disk) K) (hEK : Disjoint (E.region v) K)
        {n : ℕ} (P : SegmentChain (E.region v) (C.drawing.point v) (target v) (n+1))
        (hP : P.IsSimple) (hrad : C.drawing.point v∈segment ℝ C.center (P.vertex 1)) :
        ∃ C' : DiskCore G (B \ {v}),
        ∃ E' : ExteriorPorts C'.drawing.point target (B \ {v}) C'.disk,
          C'.drawing.point v=target v ∧ C'.drawing.point v∈C'.disk ∧
          Disjoint (closure C'.disk) K ∧
          (∀ w∈B \ {v}, ∀ z∈E'.region w, z∈K → z∈E.region w) := by
    …

    Mentions: OAI.PlanarL1.Topology.ExteriorPorts, OAI.PlanarL1.Topology.SegmentChain, OAI.PlanarL1.Topology.DiskCore

20. lemma OAI.PlanarL1.Topology.DiskCore.absorb_stem line 509

    Source documentation

    Absorb an arbitrary finite polygonal exterior stem into the disk. The selected leaf reaches its actual exterior target, which becomes interior; other ports and their external connections survive, without introducing new intersections with any fixed closed obstacle disjoint from the route.

    lemma absorb_stem (E : ExteriorPorts C.drawing.point target B C.disk)
        (hleaf : ∀ w∈B, ∀ u u', G.Adj w u → G.Adj w u' → u=u')
        {v : V} (hv : v∈B) {K : Set ℂ} (hK : IsClosed K)
        (hCK : Disjoint (closure C.disk) K) (hEK : Disjoint (E.region v) K) :
        ∃ C' : DiskCore G (B \ {v}),
        ∃ E' : ExteriorPorts C'.drawing.point target (B \ {v}) C'.disk,
          C'.drawing.point v=target v ∧ C'.drawing.point v∈C'.disk ∧
          Disjoint (closure C'.disk) K ∧
          (∀ w∈B \ {v}, ∀ z∈E'.region w, z∈K → z∈E.region w) := by
    …

    Mentions: OAI.PlanarL1.Topology.ExteriorPorts, OAI.PlanarL1.Topology.DiskCore

21. lemma OAI.PlanarL1.Topology.DiskCore.prepare_radial line 547

    Source documentation

    Before the last radial piece is swallowed, all of a closed external barrier, including the target vertex itself, can remain outside the disk.

    lemma prepare_radial (E : ExteriorPorts C.drawing.point target B C.disk)
        (hleaf : ∀ w∈B, ∀ u u', G.Adj w u → G.Adj w u' → u=u')
        {v : V} (hv : v∈B) {K : Set ℂ} (hK : IsClosed K)
        (hCK : Disjoint (closure C.disk) K)
        (hEK : ∀ z∈E.region v, z∈K → z=target v)
        {n : ℕ} (P : SegmentChain (E.region v) (C.drawing.point v) (target v) (n+1))
        (hP : P.IsSimple) (hrad : C.drawing.point v∈segment ℝ C.center (P.vertex 1)) :
        ∃ C' : DiskCore G B,
        ∃ E' : ExteriorPorts C'.drawing.point target B C'.disk,
          segment ℝ (C'.drawing.point v) (target v) ⊆ E'.region v ∧
          C'.drawing.point v∈segment ℝ C'.center (target v) ∧
          Disjoint (closure C'.disk) K ∧
    …

    Mentions: OAI.PlanarL1.Topology.ExteriorPorts, OAI.PlanarL1.Topology.SegmentChain, OAI.PlanarL1.Topology.DiskCore

22. lemma OAI.PlanarL1.Topology.DiskCore.prepare_stem line 574