CoverSchedule.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The common deterministic physical mesh and geometric clock radii in the explicit-gauge cover. The cutoff depends on the multiplicity and radius, never on the stopped state or spatial center.

def OAI.SLEExactGauge.coverRadius line 15
theorem OAI.SLEExactGauge.coverRadius_pos line 17
theorem OAI.SLEExactGauge.coverRadius_antitone line 19
theorem OAI.SLEExactGauge.coverRadius_tendsto_zero line 25
theorem OAI.SLEExactGauge.coverRadius_third_tendsto_zero line 34
theorem OAI.SLEExactGauge.coverRadius_window_upper line 42
theorem OAI.SLEExactGauge.coverRadius_next_below_dense_cutoff line 48
Source documentation
The one-unit angle test and the dense experiment both finish before the next scheduled radius.
```
theorem coverRadius_next_below_dense_cutoff
    {T C₁ : ℝ} (hC₁ : 0 < C₁) (hgap : 1 + Real.log C₁ < T) (j : ℕ) :
    coverRadius T (j + 1) < Real.exp (-1) * coverRadius T j / C₁ := by
…
```
Mentions: OAI.SLEExactGauge.coverRadius

theorem OAI.SLEExactGauge.exists_cover_physical_mesh line 62

Source documentation

One sequence works at every test and every center. It has strict slack below all dense-visit cutoffs, even though those cutoffs vary with m_n.

theorem exists_cover_physical_mesh
    (T c : ℝ) (δ : ℕ → ℝ) (hδ : ∀ m, 0 < δ m) :
    ∃ v : ℕ → ℝ, (∀ n, 0 < v n) ∧
      Tendsto v atTop (𝓝 0) ∧ (∀ n, v (n + 1) ≤ v n / 2) ∧
      (∀ n, v n ≤ (2 : ℝ) ^ (-(n : ℝ))) ∧
      ∀ n j, j ∈ coverTestWindow n →
        v n < Real.exp (-1) * coverRadius T j * δ (coverMultiplicity c n) := by
…

Mentions: OAI.SLEExactGauge.coverTestWindow, OAI.SLEExactGauge.coverRadius, OAI.SLEExactGauge.coverMultiplicity

theorem OAI.SLEExactGauge.cover_diameter_tendsto_zero line 87
Source documentation
A common diameter bound for the selected enlarged disks and the fine grid cells tends to zero.
```
theorem cover_diameter_tendsto_zero {T : ℝ} (hT : 0 < T) (A B : ℝ) :
    Tendsto (fun n => ENNReal.ofReal
      (max (A * coverRadius T (n / 3)) (B * coverRadius T n))) atTop (𝓝 0) := by
…
```
Mentions: OAI.SLEExactGauge.coverRadius