Papers With

← All papers
First page of The Exact Growth Rate of Space-Optimal Reversible Pebbling on Chains

The Exact Growth Rate of Space-Optimal Reversible Pebbling on Chains

Tetsuo Yokoyama

cs.CC Sep 14, 2026 · v1 math.CO
formalization combinatorics ai-agents
Read PDF arXiv abstract Code
TL;DR
Main theorems on the exact growth rate of reversible pebbling were formalized and verified in Lean 4 by an AI agent, with a public repository.
Abstract
We determine the exact time exponent of space-optimal reversible pebbling on chains as $1.331742379256310\ldots$. The growth rate of space-optimal reach exists as a limit and admits a variational formula. The same exponent governs complete computations at minimal space, uniformly in the chain length.
Problem

The exact time exponent of space-optimal reversible pebbling on chains was open. Known bounds left a gap between Knill's lower bound of about n^1.2938 and the n^{log2 3} cost of Bennett's strategy.

Approach

Knill's recursion is analyzed through normalized forward differences of the cost function. Their counting functions satisfy a dual pair of comparison inequalities, and power-law supersolutions and subsolutions give matching bounds expressed through a variational formula. Theorems 1.1–1.3 were verified in Lean 4 without additional hypotheses, using a formalization built from the manuscript by an AI agent.

Results

The growth constant is c = 2^{1+κ*}, where κ* ≈ 0.33174237925631, so the time exponent is log2 c ≈ 1.331742379256310. Bennett's strategy is therefore not time-optimal. The same exponent governs complete computations at minimal space.