Delivery interpretation of annulus contributions

The probabilistic upper bound counts, for each target, the quantity 2^(rOut - dist center target) contributed by a stack of size 2^rOut at an annulus center. This file proves that the counted quantity is not just bookkeeping: it is actually deliverable by pebbling moves.

def PebblingLean.Hypercube.stackListDistribution {n : ℕ} (rOut : ℕ) : List (HypercubeVertex n) → Pebbling (HypercubeVertex n)

A deterministic distribution formed by placing one stack of size 2^rOut at each center in a list. Repeated centers add stacks.

Equations

• PebblingLean.Hypercube.stackListDistribution rOut [] = fun (x : PebblingLean.HypercubeVertex n) => 0
• PebblingLean.Hypercube.stackListDistribution rOut (center :: centers) = PebblingLean.Pebbling.single center (2 ^ rOut) + PebblingLean.Hypercube.stackListDistribution rOut centers

def PebblingLean.Hypercube.IsGoodCenterList (n rIn rOut T : ℕ) (centers : List (HypercubeVertex n)) : Prop

A center list is good for demand T if every target receives annulus contribution at least T. The probabilistic estimates will prove existence of such lists.

Equations

• PebblingLean.Hypercube.IsGoodCenterList n rIn rOut T centers = ∀ (target : PebblingLean.HypercubeVertex n), T ≤ PebblingLean.Hypercube.annulusTotalContribution rIn rOut target centers

theorem PebblingLean.Hypercube.size_stackListDistribution {n rOut : ℕ} (centers : List (HypercubeVertex n)) : (stackListDistribution rOut centers).size = centers.length * 2 ^ rOut

theorem PebblingLean.Hypercube.minOccupiedPileSize_stackListDistribution {n rOut : ℕ} (centers : List (HypercubeVertex n)) : (stackListDistribution rOut centers).MinOccupiedPileSize (2 ^ rOut)

Every occupied pile in a stack-list distribution has at least one full stack. Repeated centers only increase the pile size.

theorem PebblingLean.Hypercube.canReachAtLeast_annulusContribution_single {n rIn rOut : ℕ} {target center : HypercubeVertex n} (hmem : center ∈ annulus n rIn rOut target) : Pebbling.CanReachAtLeast (graph n) (Pebbling.single center (2 ^ rOut)) target (annulusContribution rIn rOut target center)

A stack of size 2^rOut at an annulus center can directly deliver the annulus contribution assigned to that center.

theorem PebblingLean.Hypercube.canReachAtLeast_annulusTotalContribution_stackList {n rIn rOut : ℕ} (target : HypercubeVertex n) (centers : List (HypercubeVertex n)) : Pebbling.CanReachAtLeast (graph n) (stackListDistribution rOut centers) target (annulusTotalContribution rIn rOut target centers)

The deterministic delivery interpretation of X_t: the stack list can deliver at least the total annulus contribution to the fixed target.

theorem PebblingLean.Hypercube.solvableAtLeast_stackListDistribution_of_good {n rIn rOut T : ℕ} {centers : List (HypercubeVertex n)} (hgood : IsGoodCenterList n rIn rOut T centers) : Pebbling.SolvableAtLeast (graph n) (stackListDistribution rOut centers) T

Deterministic probabilistic-method interface: once a center list is good for every target, the corresponding stack distribution is T-solvable.

theorem PebblingLean.Hypercube.hasSolvableAtMostSize_of_goodCenterList {n rIn rOut T : ℕ} {centers : List (HypercubeVertex n)} (hgood : IsGoodCenterList n rIn rOut T centers) : Pebbling.HasSolvableAtMostSize (graph n) T (centers.length * 2 ^ rOut)

Costed form of the deterministic interface for the high-demand lemma.

theorem PebblingLean.Hypercube.hasHighDemandDistribution_of_goodCenterList {n rIn rOut T : ℕ} {centers : List (HypercubeVertex n)} (hgood : IsGoodCenterList n rIn rOut T centers) : HasHighDemandDistribution n T (centers.length * 2 ^ rOut) (2 ^ rOut)

High-demand form of the deterministic interface: a good center list gives a T-solvable distribution with controlled size and occupied piles of size at least 2^rOut.