SerpentineAttachments.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Clearance below the array and the unique attachment to its first column. These facts separate the low connector from the array.

lemma OAI.SLEExactGauge.Serpentine.array_normal_im_lower line 13
theorem OAI.SLEExactGauge.Serpentine.array_downward_attachment line 48
Source documentation
The downward extension of the first column meets the array only at its initial cross-section, with identical normal coordinate.
```
theorem array_downward_attachment {m : ℕ} (hm : 0 < m) {z : ℂ}
    (hz : 0 ≤ z.re ∧ |z.im| ≤ 1) {y a : ℝ} (hy : y ≤ -(100 * (m : ℝ)))
    (ha : |a| ≤ 1)
    (he : normalRibbon (arraySpine m (2 * m)) (arrayTangent m (2 * m)) z =
      columnPoint 0 (100 * m) m 0 y a) :
    z.re = 0 ∧ y = -(100 * (m : ℝ)) ∧ z.im = a := by
…
```
Mentions: OAI.SLEExactGauge.Serpentine.normalRibbon, OAI.SLEExactGauge.Serpentine.arraySpine, OAI.SLEExactGauge.Serpentine.arrayTangent, OAI.SLEExactGauge.Serpentine.columnPoint