ParameterGaps.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Companion §03, coarse epoch parameter gaps. These explicit constants prove the manuscript's uniform logarithmic comparison without a compactness/minimum oracle. Hypotheses are the exact held-size and non-dominance inequalities.

theorem OAI.UniformKServer.ParameterGaps.regular_log line 15
Source documentation
The regular size-log comparison, with an absolute explicit constant.
```
theorem regular_log {x : ℝ} (hx : (50:ℝ)/43 ≤ x) :
    (1+Real.log x)/50 ≤ Real.log (1+(9:ℝ)/11*((99:ℝ)/100*x-1)) := by
…
```
theorem OAI.UniformKServer.ParameterGaps.ratio_from_sizes line 35
Source documentation
Convert exact active accuracy and superadditivity to the size ratio. The side sum may omit inactive children, whose sizes remain nonnegative.
```
theorem ratio_from_sizes {M m a side : ℝ} (hm : 0 < m) (ha : 0 < a)
    (hacc : (9:ℝ)/10*m ≤ a) (hside : 0 ≤ side)
    (hM : m+(10:ℝ)/11*side ≤ M) :
    1+(9:ℝ)/11*(side/a) ≤ M/m := by
…
```

theorem OAI.UniformKServer.ParameterGaps.regular_epoch line 49

Source documentation

A regular active child in an epoch.

theorem regular_epoch {A a M m : ℝ} (ha : 0 < a)
    (hsmall : a ≤ (86:ℝ)/100*A)
    (hratio : 1+(9:ℝ)/11*((99:ℝ)/100*A/a-1) ≤ M/m) :
    (1+Real.log (A/a))/50 ≤ Real.log (M/m) := by
…

theorem OAI.UniformKServer.ParameterGaps.dominant_log line 62
Source documentation
The same comparison for the marked child. The constant 1/2 is a conservative consequence of the source's side/reference comparisons.
```
theorem dominant_log {u r : ℝ} (hu : 0 ≤ u) (hu₁ : u ≤ 1/4)
    (hr : 1+u/2 ≤ r) : u/3 ≤ Real.log r := by
…
```

theorem OAI.UniformKServer.ParameterGaps.dominant_ratio line 76

Source documentation

With δ_s=10⁻³, the marked side-reference gives the concrete ratio used in dominant_log. No additive lower bound on u is needed.

theorem dominant_ratio {A a side U r : ℝ} (hA : 0 < A) (ha : 0 < a)
    (hside : 0 ≤ side) (haA : a ≤ (101:ℝ)/100*A)
    (hU : U ≤ (1001:ℝ)/1000*side)
    (hr : 1+(9:ℝ)/11*(side/a) ≤ r) :
    1+(U/A)/2 ≤ r := by
…

def OAI.UniformKServer.ParameterGaps.beta line 94
Source documentation
Clipped β parameters are unclipped on active vertices.
```
def beta (c ell k cut M : ℝ) : ℝ := 3 + c / ell * Real.log (k/max M cut)
```
theorem OAI.UniformKServer.ParameterGaps.beta_gap line 96