RibbonSurvival.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Actual surviving-component assertions for access rays and the splice. Containment of the past in the initial rectangle implies that every point above or beside it belongs to the unbounded surviving component.

theorem OAI.SLEExactGauge.survives_of_unbounded_free_curve line 16
def OAI.SLEExactGauge.upwardRay line 28
theorem OAI.SLEExactGauge.upwardRay_continuous line 30
theorem OAI.SLEExactGauge.upwardRay_unbounded line 33
theorem OAI.SLEExactGauge.outside_initial_rectangle_survives line 44
theorem OAI.SLEExactGauge.continuationTube_subset_survivingDomain line 69
Source documentation
The open continuation tube avoids the actual filled hull whenever the past lies in the containing rectangle; no filled-hull containment is assumed.
```
theorem continuationTube_subset_survivingDomain
    (γ : ℝ≥0 → ℂ) (T : ℝ≥0) (B : ℝ)
    (hpast : γ '' Icc 0 T ⊆ GuideSplice.closedInitialRectangle B)
    (F : ℂ → ℂ) (a : ℂ) (r : ℝ) (O : Set ℂ) :
    GuideSplice.continuationTube F a r B O ⊆ survivingDomain γ T := by
…
```
Mentions: OAI.SLEExactGauge.GuideSplice.closedInitialRectangle, OAI.SLEExactGauge.GuideSplice.continuationTube, OAI.SLEExactGauge.survivingDomain