MovingFinalGap.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The polynomial bulk scale leaves a strict final overlap margin

theorem OAI.Ostmann.eventually_polynomial_scale_log_margin line 13
Source documentation
At the manuscript's scale z = k^4, every fixed logarithmic cost is smaller than any fixed positive multiple of log (2^k).
```
theorem eventually_polynomial_scale_log_margin (B C δ : ℝ) (hδ : 0 < δ) :
    ∀ᶠ k : ℕ in atTop,
      B + C * Real.log ((k : ℝ) ^ 4) < δ * Real.log ((2 : ℝ) ^ k) := by
…
```

theorem OAI.Ostmann.eventually_moving_final_gap line 31

Source documentation

The 3/4 bad-arrangement saving dominates the 2/5 cutoff exponent, with the full base-gap and fixed logarithmic costs of (9.8).

theorem eventually_moving_final_gap (Bs BD Bz C B : ℝ) :
    ∀ᶠ k : ℕ in atTop,
      BD + 2 * Bs + (Bz + 16) * Real.log ((k : ℝ) ^ 4) + C + 2 * B + 2 <
        (7 / 20 : ℝ) * Real.log ((2 : ℝ) ^ k) := by
…