1. CLRS-Lean
  2. CLRS Fourth Edition
  3. Chapter 15. Greedy Algorithms
  4. 15.4. Offline caching
  5. Optimality Proof
  6. Optimality — Trace Coupling
Imports
import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A6_Iteration

Section 15.4 trace-coupling proof

The optimality proof proceeds through legal cache traces, exact one-page cache differences, a recursive ordered/credited suffix coupling, one-step exchange, and finite iteration.

Proof layers: