Recurrence bridge for the upper bound #
This file connects the probabilistic high-demand construction to the deterministic product recursion. It is still parameterized by the numerical annulus estimates; once those are instantiated, this theorem is the formal recursion step used in the upper bound.
Ordinary upper-bound target for optimal pebbling of hypercubes: for each
dimension n, there is a solvable distribution on Q_n of size at most
costBound n.
Equations
- PebblingLean.Hypercube.HasHypercubePebblingUpperBound costBound = ∀ (n : ℕ), PebblingLean.Pebbling.HasSolvableAtMostSize (PebblingLean.Hypercube.graph n) 1 (costBound n)
Instances For
Forget the strengthened high-demand invariant and retain only the ordinary one-pebble solvability upper bound.
Abstract strong-induction wrapper for recursive high-demand constructions.
The actual upper bound will instantiate costBound and minPile with the
chosen recursive dimension split and parameter estimates.
Base-case helper: the trivial distribution with one pebble on every vertex
solves demand 1, and can be weakened to any larger cost bound and any
minimum-pile lower bound at most 1.
Base-case helper with large occupied piles: putting S pebbles on every
vertex gives ordinary solvability when S ≥ 1, while retaining any requested
minimum-pile lower bound at most S.
One formal recursion step from the optimized chord high-demand construction.
The probabilistic construction supplies a Tbase-solvable distribution on
Q_m of size at most N * 2^rOut, with occupied piles of size at least
2^rOut. If Q_a can solve demand N * 2^rOut at cost 2^rOut * K, then
the product step gives a solvable distribution on Q_(a+m) of cost
(N * 2^rOut) * K.
Recursive high-demand step with an optimized-chord fiber construction.
An existing high-demand construction on Q_m supplies the demands. The
optimized-chord construction on Q_a solves the largest possible demand
costBound, with fiber cost bounded by S * K; occupied-pile compression then
gives a high-demand distribution on Q_(a+m) with cost costBound * K and new
minimum pile size 2^rOut.
Same recursive high-demand step, with the new pile-size invariant weakened
to any specified lower bound below 2^rOut.
Variable-demand version of the optimized-chord product step.
For every occupied pile size t ≥ S in the recursive Q_m distribution, the
optimized-chord construction supplies a t-solvable fiber in Q_a of cost
t*K. This is the recurrence used in the paper: costs add as
∑_z E z * K = |E|*K, rather than paying for a worst-case demand in every
occupied fiber.
Abstract recursive split schedule for the upper bound.
For every large dimension n, the schedule chooses a split
Q_n ≃ Q_{splitA n} □ Q_{splitM n}. The inductive hypothesis supplies the
base high-demand distribution on Q_{splitM n}; the optimized-chord annulus
construction supplies the fiber distribution on Q_{splitA n} for demand
costBound (splitM n). The hypotheses here are exactly the numerical
conditions that remain after all graph-theoretic, probabilistic, and product
bookkeeping has been formalized.
Paper-accurate recursive split schedule with variable fiber demand.
The fixed-demand schedule above asks the Q_a fiber construction to solve the
maximum possible pile size in every occupied fiber. The paper instead applies
the high-demand lemma separately to each occupied pile size t; this theorem
packages that sharper recurrence.
Same recursive split schedule, with the finite base range discharged by the constant one-pebble-per-vertex distribution.
Same recursive split schedule, with finite base cases discharged by the constant distribution having exactly the requested minimum pile size on every vertex. This is the base-case form used by the paper recursion, where the large-pile invariant is maintained even below the cutoff dimension.
Variable-demand recursive split schedule, with finite base cases discharged by the constant distribution having the requested minimum pile size on every vertex.
Ordinary upper-bound form of the recursive split schedule with constant base cases.
Ordinary upper-bound form of the recursive split schedule with large-pile constant base cases.
Ordinary upper-bound form of the variable-demand recursive split schedule with large-pile constant base cases.