16.3. The Potential Method

This fourth-edition reader facade presents the potential method independently from the aggregate and accounting methods.

Main results

CLRS.Chapter17.amortizedCost adds the change in potential to an operation's actual cost.
CLRS.Chapter17.potential_totalCost_eq_totalAmortized_sub_delta proves the exact telescoping identity for a finite trace.
CLRS.Chapter17.potential_totalCost_le_totalAmortized derives the standard upper bound when the endpoint potential does not decrease.

Status: proved for the finite-trace potential framework.

Definitions and proofs

CLRSLean.FourthEdition.Chapter_16.Section_16_1_Amortized_Framework

Prefix sum of integer-valued costs for the first n operations.

def prefixCostR (cost : Nat -> Int) : Nat -> Int
  | 0 => 0
  | n + 1 => prefixCostR cost n + cost n

A potential-method trace with integer actual costs and potentials.

structure PotentialTrace where
  actual : Nat -> Int
  potential : Nat -> Int

Amortized cost of operation i under a potential function.

def amortizedCost (tr : PotentialTrace) (i : Nat) : Int :=
  tr.actual i + tr.potential (i + 1) - tr.potential i

Exact potential-method identity: total actual cost equals total amortized cost minus the net potential increase.

theorem potential_totalCost_eq_totalAmortized_sub_delta
    (tr : PotentialTrace) (n : Nat) :
    prefixCostR tr.actual n =
      prefixCostR (amortizedCost tr) n - (tr.potential n - tr.potential 0) := by
  induction n with
  | zero =>
      simp [prefixCostR]
  | succ n ih =>
      simp [prefixCostR, amortizedCost, ih]
      ring

Potential-method upper bound: if the endpoint potential has not decreased, total actual cost is at most total amortized cost.


theorem potential_totalCost_le_totalAmortized
    (tr : PotentialTrace) (n : Nat)
    (hpot : tr.potential 0 <= tr.potential n) :
    prefixCostR tr.actual n <= prefixCostR (amortizedCost tr) n := by
  have h := potential_totalCost_eq_totalAmortized_sub_delta tr n
  rw [h]
  omega