{"id":"palomar/PALOMAR-2026-09-30-000014","url":"https://github.com/geoconuk/lean-misc-math/tree/95624a5e96f93b05b744843f9fcd762503be1d85","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-30-000014-v1.json","repo":"https://github.com/geoconuk/lean-misc-math","tags":["cs.CC","cs.DS","msc:68Q17","msc:68Q25","msc:05C57","msc:65T50","msc:65Y20","lean","complexity","pebble-games"],"score":0,"title":"Hong and Kung's red-blue pebble game: the partition lemma and I/O lower bounds for the FFT and matrix multiplication","trust":"high","domain":"cs.CC","source":"palomar","authors":["George A. Constantinides"],"reviews":0,"subject":"cs.CC","summary":"The red-blue pebble game of Hong Jia-Wei and H. T. Kung (STOC 1981) models a computation on a directed acyclic graph run with S words of fast memory and unlimited slow memory: a red pebble on a vertex is its value held in fast memory, a blue pebble its value held in slow memory, and each load or store costs one I/O operation. This formalisation defines the game, complete calculations and the minimum I/O time Q, and proves three families of results from the paper, with explicit constants and, where the paper states one, in its asymptotic form. Q is 0 by convention where no complete…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-09-30","reactions":{},"formalized":true,"formalizes":[{"title":"I/O Complexity: The Red-Blue Pebble Game","identifier":"doi:10.1145/800076.802486","relationship":"adapts"}]}