SerpentineStepCount.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Integer unit-step alignment inside the actual straight passes of the serpentine array. A full unit middle strip is retained in each selected step; rounding the column entry times does not lose the quadratic count.

def OAI.SLEExactGauge.Serpentine.columnEntry line 17
Source documentation
Column entry times in ribbon-width units: straight length 200m, then a semicircle of radius 50. The connector contributes A.
```
def columnEntry (A : ℝ) (m j : ℕ) : ℝ :=
…
```
def OAI.SLEExactGauge.Serpentine.retainedStep line 20
lemma OAI.SLEExactGauge.Serpentine.columnEntry_nonneg line 22
lemma OAI.SLEExactGauge.Serpentine.retainedStep_bounds line 27
theorem OAI.SLEExactGauge.Serpentine.retained_middle_in_straight line 42
Source documentation
The complete closed middle interval of each chosen integer step lies strictly in its corresponding straight pass.
```
theorem retained_middle_in_straight {A : ℝ} (hA : 0 ≤ A) {m j i : ℕ}
    (hi : i < m) :
    Icc ((retainedStep A m j i : ℝ) + 1 / 3)
      ((retainedStep A m j i : ℝ) + 2 / 3) ⊆
      Ioo (columnEntry A m j) (columnEntry A m j + 200 * m) := by
…
```
Mentions: OAI.SLEExactGauge.Serpentine.retainedStep, OAI.SLEExactGauge.Serpentine.columnEntry
lemma OAI.SLEExactGauge.Serpentine.columnEntry_separation line 52
lemma OAI.SLEExactGauge.Serpentine.retainedStep_strict_column line 60
theorem OAI.SLEExactGauge.Serpentine.retainedStep_injective line 70
def OAI.SLEExactGauge.Serpentine.retainedSteps line 89
theorem OAI.SLEExactGauge.Serpentine.retainedSteps_card line 92
def OAI.SLEExactGauge.Serpentine.completionStep line 98
Source documentation
Rounded completion of all 2m+1 passes, before extending vertically.
```
def completionStep (A : ℝ) (m : ℕ) : ℕ :=
…
```
theorem OAI.SLEExactGauge.Serpentine.completionStep_quadratic_bound line 101