ExperimentClearance.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The dense experiment need not classify the filled hull of its obstacle. A free upward corridor puts the marked-point ball in the actual unbounded surviving component and gives its conformal-radius cutoff directly.

def OAI.SLEExactGauge.upwardShadow line 17
Source documentation
The upward shadow of a ball, with a slightly larger rectangular base.
```
def upwardShadow (w : ℂ) (r : ℝ) : Set ℂ :=
…
```
lemma OAI.SLEExactGauge.upwardRay_mem_shadow line 20
lemma OAI.SLEExactGauge.marked_ball_survives_of_free_upwardShadow line 33
lemma OAI.SLEExactGauge.fullRadius_lower_of_surviving_ball line 52

theorem OAI.SLEExactGauge.experiment_radius_lower_from_shadow line 64

Source documentation

Uniform free clearance gives the actual radius bound throughout every successful prefix. Filled-hull containment is unnecessary.

theorem experiment_radius_lower_from_shadow
    {U : ℝ≥0 → ℝ} {γ : ℝ≥0 → ℂ} {G F : ℝ≥0 → ℂ → ℂ}
    (hU : Continuous U) (hw : IsCapacityTwoWitness U γ G F)
    (T : ℝ≥0) (w : ℂ) {r : ℝ} (hr : 0 < r) (hheight : r ≤ w.im)
    (hfree : Disjoint (γ '' Icc 0 T) (upwardShadow w r)) :
    ∀ t : ℝ≥0, t ≤ T → w ∈ survivingDomain γ t ∧ r ≤ fullRadius G t w := by
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.upwardShadow, OAI.SLEExactGauge.survivingDomain, OAI.SLEExactGauge.fullRadius

lemma OAI.SLEExactGauge.completion_before_radiusLevelTime_of_prefix_lower line 76