WaypointCrosscutSides.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The two actual physical waypoint tubes start on opposite local sides of any correctly straightened access guide. The local side assertion is derived from openness; it is not a ribbon-angle input.

theorem OAI.SLEExactGauge.RibbonCoordinates.waypoint_quarter_ball_side line 17
theorem OAI.SLEExactGauge.RibbonCoordinates.physical_quarter_tube_coordinate line 46

theorem OAI.SLEExactGauge.RibbonCoordinates.physical_waypoint_tubes_opposite_sides line 68

Source documentation

Any local straightening of the access guide fixes one orientation for the entire pair of physical quarter-time tube neighborhoods.

theorem physical_waypoint_tubes_opposite_sides
    (hopen : PublishedPlanarDiskOpenness)
    (P : ℂ → ℂ) (hP : ContinuousOn P closedRibbon) (hi : InjOn P closedRibbon)
    (K : ℝ≥0) (hK : 0 < (K : ℝ)) {k : ℝ} (hk : 1 ≤ k)
    (hlower : ∀ v ∈ crossingPatch k, ∀ w ∈ crossingPatch k,
      dist v w ≤ K * dist (P v) (P w))
    (f : ℂ → ℂ) (j : ℂ → ℝ)
    (hf : ContinuousOn f (ball ((k + 1 / 2 : ℝ) : ℂ) (1 / 4)))
    (hfi : InjOn f (ball ((k + 1 / 2 : ℝ) : ℂ) (1 / 4)))
    (hzero : ∀ z ∈ ball ((k + 1 / 2 : ℝ) : ℂ) (1 / 4),
      (f z).re = 0 ↔ z.im = 0)
    (hrel : ∀ z ∈ ball ((k + 1 / 2 : ℝ) : ℂ) (1 / 4), j (P z) = (f z).re) :
…

Mentions: OAI.SLEExactGauge.PublishedPlanarDiskOpenness, OAI.SLEExactGauge.RibbonCoordinates.closedRibbon, OAI.SLEExactGauge.RibbonCoordinates.crossingPatch