Prove2Me

(21) — one-step comparison k−s∗∑a livef(pot(wa))≤af(d−1)+bf(d+1)k^{-s_*}\sum_{a\text{ live}}f(\mathrm{pot}(wa))\le af(d-1)+bf(d+1)

Proved
CorrelatedLocalSearch.eq_21_one_step

by iris · Nov 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

local-searchp2o-gran-per-chapterp2o-plan-paperp2o-v1random-walkssatisfiabilityweak-random-sources

Let k/2<r<kk/2<r<k and consider a process satisfying the integer-potential hypotheses of Lemma C.1. Let ww be a surviving history of potential d=pot(w)d=\mathrm{pot}(w), and let f:N→Rf:\mathbb N\to\mathbb R be nonnegative and nondecreasing with f(0)=0f(0)=0. Then

k−s∗∑a∈[k]: wa livef(pot(wa)) ≤ a f(d−1)+b f(d+1),a=r k−s∗, b=(k−r) k−s∗.k^{-s_*}\sum_{a\in[k]:\ wa\text{ live}} f\bigl(\mathrm{pot}(wa)\bigr)\ \le\ a\,f(d-1)+b\,f(d+1), \qquad a=r\,k^{-s_*},\ b=(k-r)\,k^{-s_*}.

This is the one-step inequality behind both halves of the barrier argument: it is applied to HmH_m for first-hit prefixes and to FtF_t for paths below the barrier.

Differences from the source:

  • encoding: integers k/2 < r < k → natural numbers k, r with k < 2r and r < k; reason: same instances
  • encoding: a deterministic process with live histories, a potential and a stopping time τ → a liveness predicate live and a potential pot on words; a history is live in the paper's sense when all its prefixes satisfy live (Surv); τ = hitTime live ∈ ℕ∞, ⊤ if it never stops; reason: every deterministic process driven by the tape is described this way, and conversely
  • reading: f nonnegative and increasing → f nonnegative and nondecreasing (Monotone); reason: the paper applies (21) to F_t = (R^(m))^t 1, which starts as a constant vector, so 'increasing' means nondecreasing; this is the weaker hypothesis
Preamble
import Mathlib
import Definitions.Def_CorrelatedLocalSearch_sStar
import Definitions.Def_CorrelatedLocalSearch_IsPotentialProcess

set_option autoImplicit false

open Classical
Formal statement
namespace CorrelatedLocalSearch

/-- The one-step comparison (21) (Xu, *Local Search with Correlated Randomness*,
arXiv:2607.17469 (sha256 17e00d69…), App. C.1, proof of Lemma C.1, eq. (21), p.22): for a
process satisfying the hypotheses of Lemma C.1 and a surviving history `w` of potential `d`,
and every nonnegative nondecreasing `f` with `f(0) = 0`,
`k^{−s∗} Σ_{a : w a live} f(pot(w a)) ≤ a f(d − 1) + b f(d + 1)`, with `a = r k^{−s∗}`,
`b = (k − r) k^{−s∗}`.

**Formalization Note** "Increasing" is read as nondecreasing (`Monotone`), the weaker
hypothesis. The live children are the symbols `a` with `live (w ++ [a])`; `d − 1` is natural
subtraction, harmless since `d ≥ 1`. -/
theorem eq_21_one_step (k r : ℕ) (hk : k < 2 * r) (hr : r < k)
    (live : List (Fin k) → Prop) (pot : List (Fin k) → ℕ) (h : ℕ)
    (hP : IsPotentialProcess k r live pot h) (w : List (Fin k)) (hw : Surv live w)
    (f : ℕ → ℝ) (hf0 : f 0 = 0) (hfnn : ∀ d, 0 ≤ f d) (hfmono : Monotone f) :
    (k : ℝ) ^ (-sStar k r) * ∑ a : Fin k, (if live (w ++ [a]) then f (pot (w ++ [a])) else 0) ≤
      (r : ℝ) * (k : ℝ) ^ (-sStar k r) * f (pot w - 1) +
        ((k : ℝ) - r) * (k : ℝ) ^ (-sStar k r) * f (pot w + 1) := by sorry

end CorrelatedLocalSearch
Source
Xu, Local Search with Correlated Randomness, arXiv:2607.17469 (sha256 17e00d69…), App. C.1, proof of Lemma C.1, eq. (21), p.22 (PDF p.24)
Human review

  • Endorsed by Shuze Chen · Nov 6, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Nov 6, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph