SerpentineShadow.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The displaced array and its vertical attachments avoid an explicit upward shadow from the marked point. This gives the free upward route used to control the conformal radius of every completed prefix.

lemma OAI.SLEExactGauge.Serpentine.center_horizontal_distance line 14
lemma OAI.SLEExactGauge.Serpentine.disk_horizontal_separation line 20
lemma OAI.SLEExactGauge.Serpentine.column_avoids_upward_shadow line 35
lemma OAI.SLEExactGauge.Serpentine.turn_inside_displaced_disk line 44
lemma OAI.SLEExactGauge.Serpentine.turn_avoids_upward_shadow line 53

lemma OAI.SLEExactGauge.Serpentine.low_connector_avoids_upward_shadow line 62

Source documentation

The low part of the connector lies below the shadow.

lemma low_connector_avoids_upward_shadow {s : ℝ} (hs : 0 < s) (w z : ℂ)
    (hw : s ≤ w.im) (hz : z.im ≤ s / 2) :
    ¬ (|z.re - w.re| < s / 100 ∧ w.im - s / 100 < z.im) := by
…

lemma OAI.SLEExactGauge.Serpentine.attachment_avoids_upward_shadow line 70
Source documentation
The vertical attachment over either outer column stays horizontally separated, regardless of its height.
```
lemma attachment_avoids_upward_shadow {s : ℝ} (hs : 0 < s) (w z : ℂ)
    {x : ℝ} (hx : |x| ≤ halfHeight s)
    (hz : |z.re - ((center s w).re + x)| ≤ s / 1000) :
    ¬ (|z.re - w.re| < s / 100 ∧ w.im - s / 100 < z.im) := by
…
```
Mentions: OAI.SLEExactGauge.Serpentine.halfHeight, OAI.SLEExactGauge.Serpentine.center