Loss bookkeeping for the recursive upper bound

The probabilistic and product arguments produce a recursive construction. After normalizing by (4/3)^n, the remaining analytic issue is to show that the multiplicative losses accumulated along the dimension recursion stay bounded.

This file formalizes that bookkeeping abstractly. It does not choose the final parameters yet; instead, it proves the deterministic theorem that a bounded finite loss sum gives a uniform normalized-cost bound.

def PebblingLean.Hypercube.LossRecurrence.iterate (next : ℕ → ℕ) : ℕ → ℕ → ℕ

The k-fold iterate of a dimension-reduction map, written recursively so the recurrence proofs can unfold cleanly.

Equations

• PebblingLean.Hypercube.LossRecurrence.iterate next 0 x✝ = x✝
• PebblingLean.Hypercube.LossRecurrence.iterate next k.succ x✝ = PebblingLean.Hypercube.LossRecurrence.iterate next k (next x✝)

def PebblingLean.Hypercube.LossRecurrence.ActiveFor (next : ℕ → ℕ) (n0 : ℕ) : ℕ → ℕ → Prop

ActiveFor next n0 k n means that the first k dimensions encountered from n are still in the recursive range n0 ≤ dimension.

Equations

• PebblingLean.Hypercube.LossRecurrence.ActiveFor next n0 0 x✝ = True
• PebblingLean.Hypercube.LossRecurrence.ActiveFor next n0 k.succ x✝ = (n0 ≤ x✝ ∧ PebblingLean.Hypercube.LossRecurrence.ActiveFor next n0 k (next x✝))

def PebblingLean.Hypercube.LossRecurrence.lossProduct (next : ℕ → ℕ) (loss : ℕ → ℝ) : ℕ → ℕ → ℝ

Product of the multiplicative losses accumulated over k recursive steps.

Equations

• PebblingLean.Hypercube.LossRecurrence.lossProduct next loss 0 x✝ = 1
• PebblingLean.Hypercube.LossRecurrence.lossProduct next loss k.succ x✝ = (1 + loss x✝) * PebblingLean.Hypercube.LossRecurrence.lossProduct next loss k (next x✝)

def PebblingLean.Hypercube.LossRecurrence.lossSum (next : ℕ → ℕ) (loss : ℕ → ℝ) : ℕ → ℕ → ℝ

Sum of the additive losses accumulated over k recursive steps.

Equations

• PebblingLean.Hypercube.LossRecurrence.lossSum next loss 0 x✝ = 0
• PebblingLean.Hypercube.LossRecurrence.lossSum next loss k.succ x✝ = loss x✝ + PebblingLean.Hypercube.LossRecurrence.lossSum next loss k (next x✝)

theorem PebblingLean.Hypercube.LossRecurrence.lossProduct_nonneg {next : ℕ → ℕ} {loss : ℕ → ℝ} (hloss : ∀ (n : ℕ), 0 ≤ loss n) (k n : ℕ) : 0 ≤ lossProduct next loss k n

theorem PebblingLean.Hypercube.LossRecurrence.cost_le_lossProduct {next : ℕ → ℕ} {loss R : ℕ → ℝ} {n0 : ℕ} (hloss : ∀ (n : ℕ), 0 ≤ loss n) (hstep : ∀ (n : ℕ), n0 ≤ n → R n ≤ (1 + loss n) * R (next n)) (k n : ℕ) (hactive : ActiveFor next n0 k n) : R n ≤ lossProduct next loss k n * R (iterate next k n)

Iterating a normalized recurrence gives a finite product of the losses times the terminal normalized cost.

theorem PebblingLean.Hypercube.LossRecurrence.cost_le_lossProduct_mul_base {next : ℕ → ℕ} {loss R : ℕ → ℝ} {n0 k n : ℕ} {B : ℝ} (hloss : ∀ (n : ℕ), 0 ≤ loss n) (hstep : ∀ (n : ℕ), n0 ≤ n → R n ≤ (1 + loss n) * R (next n)) (hactive : ActiveFor next n0 k n) (hbase : R (iterate next k n) ≤ B) : R n ≤ lossProduct next loss k n * B

Version of cost_le_lossProduct with the terminal cost bounded by a specified base constant.

theorem PebblingLean.Hypercube.LossRecurrence.lossProduct_le_exp_lossSum {next : ℕ → ℕ} {loss : ℕ → ℝ} (hloss : ∀ (n : ℕ), 0 ≤ loss n) (k n : ℕ) : lossProduct next loss k n ≤ Real.exp (lossSum next loss k n)

A finite product of factors 1 + loss is bounded by the exponential of the corresponding finite sum.

theorem PebblingLean.Hypercube.LossRecurrence.cost_le_exp_lossSum_mul_base {next : ℕ → ℕ} {loss R : ℕ → ℝ} {n0 k n : ℕ} {B : ℝ} (hloss : ∀ (n : ℕ), 0 ≤ loss n) (hB : 0 ≤ B) (hstep : ∀ (n : ℕ), n0 ≤ n → R n ≤ (1 + loss n) * R (next n)) (hactive : ActiveFor next n0 k n) (hbase : R (iterate next k n) ≤ B) : R n ≤ Real.exp (lossSum next loss k n) * B

Exponential version of the finite recurrence bound.

theorem PebblingLean.Hypercube.LossRecurrence.cost_le_exp_lossBound_mul_base {next : ℕ → ℕ} {loss R : ℕ → ℝ} {n0 k n : ℕ} {B L : ℝ} (hloss : ∀ (n : ℕ), 0 ≤ loss n) (hB : 0 ≤ B) (hstep : ∀ (n : ℕ), n0 ≤ n → R n ≤ (1 + loss n) * R (next n)) (hactive : ActiveFor next n0 k n) (hbase : R (iterate next k n) ≤ B) (hsum : lossSum next loss k n ≤ L) : R n ≤ Real.exp L * B

If the accumulated additive loss is at most L, the normalized cost is bounded by exp L times the terminal base bound.

theorem PebblingLean.Hypercube.LossRecurrence.exists_terminal_iterate_of_decreasing {next : ℕ → ℕ} {n0 : ℕ} (hnext : ∀ (n : ℕ), n0 ≤ n → next n < n) (n : ℕ) : ∃ (k : ℕ), ActiveFor next n0 k n ∧ iterate next k n < n0

A strictly decreasing dimension map always reaches the finite base range after finitely many recursive steps.

def PebblingLean.Hypercube.LossRecurrence.geomSum (q : ℝ) (k : ℕ) : ℝ

The finite geometric sum 1 + q + ... + q^(k-1).

Equations

• PebblingLean.Hypercube.LossRecurrence.geomSum q k = ∑ i ∈ Finset.range k, q ^ i

theorem PebblingLean.Hypercube.LossRecurrence.geomSum_le_two_of_le_half {q : ℝ} (hq_nonneg : 0 ≤ q) (hq_half : q ≤ 1 / 2) (k : ℕ) : geomSum q k ≤ 2

theorem PebblingLean.Hypercube.LossRecurrence.first_loss_le_pow_mul_bound {next : ℕ → ℕ} {loss : ℕ → ℝ} {n0 : ℕ} {q M : ℝ} (hq_nonneg : 0 ≤ q) (hdecay : ∀ (n : ℕ), n0 ≤ n → n0 ≤ next n → loss n ≤ q * loss (next n)) (hbound : ∀ (n : ℕ), n0 ≤ n → loss n ≤ M) (k n : ℕ) (hactive : ActiveFor next n0 (k + 1) n) : loss n ≤ q ^ k * M

If every active loss is at most q times the next active loss, and active losses are bounded by M, then the first loss in a path of length k+1 is at most q^k M.

theorem PebblingLean.Hypercube.LossRecurrence.lossSum_le_geomSum_mul_bound {next : ℕ → ℕ} {loss : ℕ → ℝ} {n0 : ℕ} {q M : ℝ} (hq_nonneg : 0 ≤ q) (hdecay : ∀ (n : ℕ), n0 ≤ n → n0 ≤ next n → loss n ≤ q * loss (next n)) (hbound : ∀ (n : ℕ), n0 ≤ n → loss n ≤ M) (k n : ℕ) (hactive : ActiveFor next n0 k n) : lossSum next loss k n ≤ geomSum q k * M

Geometric domination of a finite loss sum along an active recursive path.

theorem PebblingLean.Hypercube.LossRecurrence.cost_uniform_bound_of_geometric_loss {next : ℕ → ℕ} {loss R : ℕ → ℝ} {n0 : ℕ} {B q M G : ℝ} (hloss : ∀ (n : ℕ), 0 ≤ loss n) (hB : 0 ≤ B) (hM : 0 ≤ M) (hq_nonneg : 0 ≤ q) (hnext : ∀ (n : ℕ), n0 ≤ n → next n < n) (hstep : ∀ (n : ℕ), n0 ≤ n → R n ≤ (1 + loss n) * R (next n)) (hbase : ∀ n < n0, R n ≤ B) (hdecay : ∀ (n : ℕ), n0 ≤ n → n0 ≤ next n → loss n ≤ q * loss (next n)) (hbound : ∀ (n : ℕ), n0 ≤ n → loss n ≤ M) (hgeom : ∀ (k : ℕ), geomSum q k ≤ G) (n : ℕ) : R n ≤ Real.exp (G * M) * B

Uniform normalized-cost bound when the loss sequence decays geometrically along recursive paths.

theorem PebblingLean.Hypercube.LossRecurrence.cost_uniform_bound_of_geometric_loss_le_two {next : ℕ → ℕ} {loss R : ℕ → ℝ} {n0 : ℕ} {B q M : ℝ} (hloss : ∀ (n : ℕ), 0 ≤ loss n) (hB : 0 ≤ B) (hM : 0 ≤ M) (hq_nonneg : 0 ≤ q) (hq_half : q ≤ 1 / 2) (hnext : ∀ (n : ℕ), n0 ≤ n → next n < n) (hstep : ∀ (n : ℕ), n0 ≤ n → R n ≤ (1 + loss n) * R (next n)) (hbase : ∀ n < n0, R n ≤ B) (hdecay : ∀ (n : ℕ), n0 ≤ n → n0 ≤ next n → loss n ≤ q * loss (next n)) (hbound : ∀ (n : ℕ), n0 ≤ n → loss n ≤ M) (n : ℕ) : R n ≤ Real.exp (2 * M) * B

Convenient geometric-loss bound for ratio at most 1/2, giving total loss at most 2M. The paper's recursion has a much smaller ratio (1/16) after increasing the base threshold, so this intentionally uses a relaxed constant.

theorem PebblingLean.Hypercube.LossRecurrence.cost_uniform_bound_of_terminal_lossBound {next : ℕ → ℕ} {loss R : ℕ → ℝ} {n0 : ℕ} {B L : ℝ} (hloss : ∀ (n : ℕ), 0 ≤ loss n) (hB : 0 ≤ B) (hstep : ∀ (n : ℕ), n0 ≤ n → R n ≤ (1 + loss n) * R (next n)) (hbase : ∀ n < n0, R n ≤ B) (hterminal : ∀ (n : ℕ), ∃ (k : ℕ), ActiveFor next n0 k n ∧ iterate next k n < n0 ∧ lossSum next loss k n ≤ L) (n : ℕ) : R n ≤ Real.exp L * B

Uniform normalized-cost bound from an explicit terminal path and a bound on the loss accumulated along that path.

theorem PebblingLean.Hypercube.LossRecurrence.cost_uniform_bound_of_decreasing_lossBound {next : ℕ → ℕ} {loss R : ℕ → ℝ} {n0 : ℕ} {B L : ℝ} (hloss : ∀ (n : ℕ), 0 ≤ loss n) (hB : 0 ≤ B) (hnext : ∀ (n : ℕ), n0 ≤ n → next n < n) (hstep : ∀ (n : ℕ), n0 ≤ n → R n ≤ (1 + loss n) * R (next n)) (hbase : ∀ n < n0, R n ≤ B) (hlossSum : ∀ (n k : ℕ), ActiveFor next n0 k n → iterate next k n < n0 → lossSum next loss k n ≤ L) (n : ℕ) : R n ≤ Real.exp L * B

Uniform normalized-cost bound for a decreasing dimension map, assuming a separate estimate on every terminal loss sum.

noncomputable def PebblingLean.Hypercube.normalizedCost (costBound : ℕ → ℕ) (n : ℕ) : ℝ

Normalized integer cost bound, divided by (4/3)^n.

Equations

• PebblingLean.Hypercube.normalizedCost costBound n = ↑(costBound n) / (4 / 3) ^ n

theorem PebblingLean.Hypercube.normalizedCost_nonneg (costBound : ℕ → ℕ) (n : ℕ) : 0 ≤ normalizedCost costBound n

noncomputable def PebblingLean.Hypercube.finiteBaseNormalizedBound (costBound : ℕ → ℕ) (n0 : ℕ) : ℝ

A concrete finite bound for the normalized costs below a cutoff. This is not optimized; it is just a convenient way to discharge finite base cases.

Equations

• PebblingLean.Hypercube.finiteBaseNormalizedBound costBound n0 = ∑ n ∈ Finset.range n0, PebblingLean.Hypercube.normalizedCost costBound n

theorem PebblingLean.Hypercube.finiteBaseNormalizedBound_nonneg (costBound : ℕ → ℕ) (n0 : ℕ) : 0 ≤ finiteBaseNormalizedBound costBound n0

theorem PebblingLean.Hypercube.normalizedCost_le_finiteBaseNormalizedBound_of_lt (costBound : ℕ → ℕ) {n0 n : ℕ} (hn : n < n0) : normalizedCost costBound n ≤ finiteBaseNormalizedBound costBound n0

def PebblingLean.Hypercube.HasRealHypercubePebblingUpperBound (C : ℝ) : Prop

Real-valued asymptotic upper-bound statement: for every dimension n, there is an ordinary solvable distribution whose size is at most C * (4/3)^n.

Equations

• PebblingLean.Hypercube.HasRealHypercubePebblingUpperBound C = ∀ (n : ℕ), ∃ (k : ℕ), PebblingLean.Pebbling.HasSolvableAtMostSize (PebblingLean.Hypercube.graph n) 1 k ∧ ↑k ≤ C * (4 / 3) ^ n

theorem PebblingLean.Hypercube.costBound_le_of_normalizedCost_le {costBound : ℕ → ℕ} {C : ℝ} (hnorm : ∀ (n : ℕ), normalizedCost costBound n ≤ C) (n : ℕ) : ↑(costBound n) ≤ C * (4 / 3) ^ n

theorem PebblingLean.Hypercube.hasRealHypercubePebblingUpperBound_of_normalizedCost {costBound : ℕ → ℕ} {C : ℝ} (hupper : HasHypercubePebblingUpperBound costBound) (hnorm : ∀ (n : ℕ), normalizedCost costBound n ≤ C) : HasRealHypercubePebblingUpperBound C

Convert an integer-valued cost-bound construction plus a real normalized cost estimate into the real asymptotic upper-bound statement.

theorem PebblingLean.Hypercube.hasRealHypercubePebblingUpperBound_of_geometric_normalizedCost_loss {costBound next : ℕ → ℕ} {loss : ℕ → ℝ} {n0 : ℕ} {B q M : ℝ} (hupper : HasHypercubePebblingUpperBound costBound) (hloss : ∀ (n : ℕ), 0 ≤ loss n) (hB : 0 ≤ B) (hM : 0 ≤ M) (hq_nonneg : 0 ≤ q) (hq_half : q ≤ 1 / 2) (hnext : ∀ (n : ℕ), n0 ≤ n → next n < n) (hstep : ∀ (n : ℕ), n0 ≤ n → normalizedCost costBound n ≤ (1 + loss n) * normalizedCost costBound (next n)) (hbase : ∀ n < n0, normalizedCost costBound n ≤ B) (hdecay : ∀ (n : ℕ), n0 ≤ n → n0 ≤ next n → loss n ≤ q * loss (next n)) (hbound : ∀ (n : ℕ), n0 ≤ n → loss n ≤ M) : HasRealHypercubePebblingUpperBound (Real.exp (2 * M) * B)

Final abstract bridge from the geometric normalized-cost recurrence to the real asymptotic upper-bound statement. After the numerical parameter choices prove the hypotheses here, this is the formal end of the upper-bound proof.