theorem LevelMethodHistory.gap_le_kappa_mul_optimalValue_of_termination_rule (history : LevelMethodHistory) {κ : ℝ} (k : ℕ) (htermination : history.approximateOptimalValue k ≥ (1 - κ) * history.optimalValue k) : history.gap k ≤ κ * history.optimalValue k

Proposition 3.55 (1): if the relative termination rule fhat(history, k) ≥ (1 - κ) fstar(history, k) holds at a selected full step, then the owner gap δ[history](k) = fstar(history, k) - fhat(history, k) is bounded by κ fstar(history, k).