Concrete parameter layer for the upper bound #
This file starts instantiating the abstract recurrence with the parameter choices used in the paper:
- the recursive dimension drop
m = ceil(K sqrt(n log n)); - the larger factor
a = n - m; - the pile-size invariant
2^(n/5); - the loss
n^{-2}; - the annulus centered near
a/3, with widthceil(A sqrt(a log(2 n^2))).
The genuinely analytic inputs are still explicit hypotheses: binomial annulus mean estimates, the Bernstein/union-bound exponent estimate for these concrete parameters, and the finite collection of threshold inequalities. The theorem at the bottom proves that these hypotheses imply the real asymptotic upper bound.
Dimension of the large factor.
Equations
Instances For
The technical occupied-pile invariant used in the recursion.
Equations
- PebblingLean.Hypercube.PaperParameters.minPile n = 2 ^ (n / 5)
Instances For
The recursive loss used in the paper, n^{-2}. At n = 0 this is 0
under Lean's totalized inverse convention, but all recurrence uses are above a
positive base cutoff.
Equations
Instances For
Integer multiplier for the fiber cost. This is the ceiling of the
normalized target multiplier (1+n^{-2})(4/3)^a.
Equations
Instances For
The recursive integer cost bound generated by the paper's schedule.
Below the finite cutoff n0 we use the constant distribution with
minPile n pebbles at every vertex. Above the cutoff we recurse to
splitM K n and multiply by the integer fiber multiplier. The fallback branch
is never used once the threshold hypothesis 4 splitM K n ≤ n is available,
but it keeps the definition total.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Annulus half-width for the high-demand construction on the Q_a factor,
with the paper's choice delta = n^{-2} giving log(2/delta)=log(2 n^2).
Equations
Instances For
The real expression inside the annulus-width ceiling.
Equations
- PebblingLean.Hypercube.PaperParameters.annulusWidthCore A K n = A * √(↑(PebblingLean.Hypercube.PaperParameters.splitA K n) * Real.log (2 * ↑n ^ 2))
Instances For
Inner radius of the annulus in the large factor.
Equations
Instances For
Outer radius of the annulus in the large factor.
Equations
Instances For
The integer annulus width dominates its real core because it is a ceiling.
The annulus diameter is at most twice the half-width parameter.
Demand-dependent number of random annulus centers used in the high-demand
construction. The factor 1 + loss n / 2 leaves the other half of the
loss n budget to pay for the ceiling.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The gap in the high-demand lemma when the target demand is the current
recursive cost and delta = n^{-2}.
Equations
- PebblingLean.Hypercube.PaperParameters.demandGap K costBound n = PebblingLean.Hypercube.PaperParameters.loss n * ↑(costBound (PebblingLean.Hypercube.PaperParameters.splitM K n)) / 4
Instances For
Demand-dependent gap used by the paper's variable-demand product step:
for demand t, the high-demand construction aims for a surplus
delta*t/4, with delta = n^{-2} at the ambient recursive dimension.
Equations
Instances For
If the next recursive dimension is at most one quarter of the current
dimension, then the loss drops geometrically. We use the relaxed ratio 1/2;
the proof gives much more.
To prove the real split estimate, it is enough to bound the expression inside the ceiling with one unit of ceiling overhead.
A simpler sufficient condition for the ceiling-core split estimate.
For large n, proving K^2 log n ≤ n/64 is enough to force
K sqrt(n log n)+1 ≤ n/4.
Lower companion to nat_div_real_le_div, with one unit of floor slack.
If the annulus half-width fits inside the center radius, then the inner
radius is at most a/3-w in real notation.
A coarse upper estimate sufficient for the center-width condition
3(core+1)≤a.
The coarse square budget for core≥9 propagates from a lower bound on
a and log(2n^2)≥log n.
The sample-count ceiling still fits inside the integer fiber multiplier once the annulus stack size is at most the reserved half-loss budget.
The concrete sample count gives the required mean surplus once the annulus
mean captures at least a (1-delta/8) fraction of the ideal weighted mean.
Here delta = loss n = n^{-2}.
To verify the stack-size threshold for all allowed demands, it is enough
to verify it at the smallest allowed demand minPile(splitM n).
Multiplication-form sufficient condition for the stack-size threshold.
Since loss n = n^{-2}, this says the product
minPile(m)(4/3)^a has room for 2 n^2 copies of the annulus stack size.
Logarithmic sufficient condition for the multiplication-form stack
threshold. This rewrites
2 n^2 2^rOut ≤ 2^(m/5) (4/3)^a as a comparison of logarithms.
Logarithmic sufficient condition for the multiplication-form Bernstein
width threshold. This is the log form of
128 * 2^(2w) * ((a+1)log 2) ≤ loss(n)^2 * 2^(m/5).
The Bernstein-width log budget can be proved using the real width core with one unit of ceiling overhead.
The stack log budget can be proved using the real width core with one unit of ceiling overhead in the outer radius.
Coarse sufficient condition for the Bernstein-width core log budget. This
is the form where every remaining term is expressed using only n, K, and
A, up to the standard sqrt(3n log n) envelope.
Coarse sufficient condition for the stack core log budget.
The positive linear margin in the stack estimate.
Instances For
Strict positivity of the stack margin:
log(4/3)-log(2)/3 = (1/3)log(32/27).
A convenient certified lower bound for the stack margin.
Corrected coarse sufficient condition for the stack core log budget. It
keeps the paired linear margin
a*(log(4/3)-log 2/3) before using a≥3n/4.
Coefficient form of the width coarse estimate. The only growing term on
the right is now sqrt(n log n) with coefficient
(K/5-2A sqrt 3) log 2.
Coefficient form of the corrected stack-margin estimate.
A simple constant-domination sufficient condition for the width sqrt
margin. The stronger but convenient assumption 15A√3≤K leaves a positive
coefficient K/15 for the residual logarithmic terms.
Once K≥5A√3, the stack sqrt coefficient is nonnegative, so the linear
margin alone can pay for the remaining logarithmic terms.
A small numerical bound used to simplify logarithmic width budgets.
Split form of the residual stack budget: one inequality pays for
2 log n, and the other pays for the constant 3 log 2.
Explicit large-n sufficient condition for the split estimate
K^2 log n≤n/64. It is intentionally coarse, but isolates this residual
analytic input behind a single quadratic threshold.
A convenient way to pay the simplified width budget: use half of the
available sqrt(n log n) term for the constant and half for 5 log n.
A width constant budget checked at the cutoff propagates to all larger dimensions.
Large-n sufficient conditions for the residual stack budget. The first
condition pays for 2 log n; the second pays for 3 log 2.
If the stack constant budget holds at the cutoff, then it holds for every larger dimension because the linear margin is nonnegative.
Squared sufficient condition for the stack square-root budget. With
c = log(4/3)-log(2)/3, the condition 16 log n≤n c^2 implies
4 sqrt(n log n)≤n c.
Simplified Bernstein/union-bound logarithmic condition. If the sampled
mean is at most 2t, then the more legible lower bound
delta^2 t/(128 B_0) implies the logarithmic condition used by the
probabilistic-method finish.
The sampled annulus mean is at most 2t once the annulus mean is bounded
by the full weighted mean and the sample-count ceiling is paid for by the
stack-size threshold.
Since the simplified Bernstein exponent is linear in the demand t, it
is enough to check it at the smallest allowed demand.
It is enough to prove the minimum-demand Bernstein threshold with
2^(2w), where w is the annulus half-width, since
rOut-rIn ≤ 2w.
Multiplication-form sufficient condition for the Bernstein width threshold. This avoids carrying a division in the remaining asymptotic estimate.
A lower bound for the Binomial(n,1/3) mass of the annulus window is
exactly the annulus-mean lower bound used by the upper-bound recurrence.
Normalized recurrence for the recursively defined integer cost bound after absorbing the multiplier ceiling into a doubled loss term.
Raw-cost form of the normalized recurrence step. This is the algebraic
translation of
|D_n| ≤ (1+n^{-2}) |D_m| (4/3)^a.
The concrete parameter theorem. The hypotheses are the remaining
numerical estimates for the paper's chosen schedule. Everything after those
estimates is now formal: the high-demand construction, product recursion, base
cases, normalized loss control, and final real C(4/3)^n upper bound.
Concrete parameter theorem using the paper-facing variable-demand product
recurrence. For every recursive dimension n and every actual occupied pile
size t ≥ minPile(splitM n), the probabilistic construction on the large
factor solves demand t with cost t * costMultiplier n.
This is the recurrence matching the proof in the paper. The remaining hypotheses are the concrete annulus mean, Bernstein/union-bound, fiber-cost, integer cost, and normalized-cost estimates.
Same as hasRealUpperBound_of_parameter_conditions, but with the
normalized recurrence supplied in the raw multiplicative form used in the
paper.
Specialization of the concrete parameter theorem to the recursively
defined integer cost bound. The finite base cost and the integer product
recurrence are discharged by recursiveCostBound_base_cost and
recursiveCostBound_step_cost; the remaining hypotheses are the genuine
analytic estimates for the chosen annulus, sample count, and ceiling overhead
in the real normalized recurrence.
Variable-demand version of
hasRealUpperBound_of_raw_cost_parameter_conditions.
Variable-demand specialization to the recursively defined integer cost bound. This is the closest formal wrapper to the paper's recursive construction currently in the project.
Recursive-cost variable-demand theorem with the concrete sample count
sampleCountForDemand. The fiber-cost arithmetic is reduced to the threshold
inequality saying the annulus stack size fits inside the reserved half-loss
budget.
Fully integer-recursive concrete-sample wrapper with ceiling overhead
absorbed into the loss bookkeeping. Compared with
hasRealUpperBound_of_recursiveCostBound_concreteSample_conditions, this
replaces the exact real recurrence hypothesis by the concrete threshold
1 ≤ n^{-2}(4/3)^a, and consequently uses the harmless doubled loss
1+2n^{-2} in the final recurrence.
Same as
hasRealUpperBound_of_recursiveCostBound_concreteSample_ceiling_conditions,
with the finite base constant chosen automatically as the sum of normalized
costs below the cutoff.
Concrete-sample finite-base wrapper with the mean and stack hypotheses
reduced to their natural paper forms. The annulus mean hypothesis says the
chosen annulus captures a (1-delta/8) fraction of the ideal weighted mean,
and the stack-size threshold only has to be checked for the smallest recursive
pile size.
Further reduced wrapper: the Bernstein/union-bound logarithmic hypothesis
is replaced by the paper-style pair of estimates E X_t ≤ 2t and
(a+1)log 2 ≤ delta^2 t/(128 B_0).
Wrapper with both annulus mean estimates exposed directly: a lower bound capturing most of the ideal weighted mean, and the trivial upper bound by the full weighted mean. The only remaining probabilistic exponent input is the simple Bernstein/union-bound threshold.
Current most reduced concrete upper-bound wrapper. For the chosen paper
parameters it remains to prove, for all sufficiently large n, the concrete
dimension split, annulus lower/upper estimates, the minimum-demand Bernstein
threshold, stack-size threshold, pile-radius threshold, and ceiling slack.
Current most reduced concrete upper-bound wrapper with the annulus upper
estimate proved internally. The remaining annulus input is only the lower-tail
capture estimate saying the chosen annulus keeps a (1-delta/8) fraction of
the full weighted mean.
Version of the reduced wrapper using the coarser but simpler Bernstein
denominator 2^(2w), where w = annulusWidth A K n.
Reduced wrapper with the annulus lower estimate stated as the concrete
binomial-window probability estimate for a Binomial(splitA n, 1/3) random
variable. This isolates the remaining Chernoff-style estimate needed for the
annulus capture step.
Tail-probability form of the reduced upper-bound wrapper. The annulus
capture estimate is reduced to proving that the two Binomial(a,1/3) tails
outside [rIn,rOut] have total mass at most delta/8.
Chernoff-parameter form of the reduced upper-bound wrapper. It remains to choose nonnegative parameters for the two binomial tails and verify the displayed explicit exponential bound.
Same Chernoff-parameter wrapper, but with separate budgets for the left
and right tails. This is the form one usually proves: each tail is at most
delta/16, so their sum is at most delta/8.
Same reduced wrapper with the ceiling slack replaced by the growth
condition (4/3)^a ≥ n^2.
Same reduced wrapper with the Bernstein width threshold stated in the
multiplication form better suited for large-n estimates.
Current reduced wrapper with all three deterministic threshold hypotheses in multiplication/growth form:
- the Chernoff tails each have budget
loss/16; - the Bernstein width threshold has no division;
- the stack threshold is
2 n^2 2^rOut ≤ minPile(m)(4/3)^a; - ceiling slack is
(4/3)^a ≥ n^2.
A coarse second-order exponential upper bound on [0,1]. The constant
13/18 comes from the third-order Taylor bound in mathlib and is deliberately
not optimized.
A canonical nonnegative Chernoff parameter of order width/a. The
constant is deliberately exposed in the definition; future analytic estimates
may replace this wrapper if a sharper constant is more convenient.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If 3w≤a, then the standard Chernoff parameter
λ=3w/(a+1) is at most one.
Left-tail standard-lambda log estimate for the annulus window.
Right-tail standard-lambda log estimate for the annulus window. The
assumption 9≤w absorbs the one-unit floor slack in rOut.
Multiplication-form version of the current reduced wrapper. The remaining real estimates are now stated without division:
16 * leftChernoffTerm ≤ loss;16 * rightChernoffTerm ≤ loss;- the multiplication-form Bernstein width threshold;
- the multiplication-form stack threshold;
(4/3)^a ≥ n^2for ceiling slack.
Same strongest wrapper, but with the split estimate supplied in real form
splitM n ≤ n/4 and the ceiling slack supplied in the coarser form
n^2 ≤ (4/3)^(n/2).
Canonical-lambda version of the reduced wrapper. This fixes both
Chernoff parameters to 3w/(a+1), leaving only the resulting two explicit
tail estimates and the deterministic growth thresholds.
Standard-lambda wrapper with the ceiling slack fully discharged by the
explicit elementary threshold n0≥58.
Same standard-lambda wrapper, with the split estimate reduced to the
ceiling-core inequality K sqrt(n log n)+1 ≤ n/4.
Same as
hasRealUpperBound_of_recursiveCostBound_coreSplit_standardLambda_noCeilSlack_finiteBase,
but discharging split-core nonnegativity from K≥0.
Exponent-form version of the current reduced wrapper. The two Chernoff tail estimates are now split into:
- a bound of each named Chernoff term by
exp(-E_n); - the log budget
log 16 + 2 log n ≤ E_n.
Same tail-exponent wrapper, but with the dimension split reduced to the
clean log-linear estimate K^2 log n ≤ n/64.
Version with both the split and stack-size thresholds stated in logarithmic form. The remaining multiplicative threshold is the Bernstein width estimate.
Current most log-reduced wrapper. The split, Bernstein-width threshold, and stack-size threshold are all stated as logarithmic estimates; the Chernoff terms are stated through an explicit tail exponent.
Same log-threshold wrapper with the annulus-width ceiling isolated. The
width and stack hypotheses use the real core
A sqrt(a log(2n^2)) + 1, which is the form expected for the remaining
large-n analytic estimates.
Coarsest current large-n wrapper. The width and stack side conditions
now use only the envelope sqrt(3n log n) and the lower estimate
splitM/5 ≥ K sqrt(n log n)/5 - 1; the exact integer floors and ceilings are
handled internally.
Same coarse wrapper, with the Chernoff hypotheses stated directly as
logarithmic exponent estimates for the standard parameter
annulusChernoffLambda.
Variant of the coarse logarithmic wrapper where the tail budget is supplied
as the simpler estimate 6 log n ≤ E_n.
Current strongest wrapper. This uses the corrected stack margin
log(4/3)-log(2)/3, rather than the overly coarse replacement of a/3 by
n/3.
Sqrt-coefficient version of the current strongest wrapper. The remaining
width and stack estimates are now stated with explicit coefficients multiplying
sqrt(n log n).
Constant-domination version of the sqrt-margin wrapper. It uses
15A√3≤K to reduce the width estimate to a residual
(K/15)log(2)sqrt(n log n) budget, and reduces the stack estimate to the
linear margin budget.
Strongest large-n wrapper in the current development. Compared with
hasRealUpperBound_of_Kdom_logBudgets_logChernoff_sixLog_finiteBase, this
replaces the raw width logarithm by the cleaner bound
log 128+4log 2+5log n, and splits the stack logarithmic budget into its
growing and constant pieces.
Large-n budget wrapper. This version exposes the residual deterministic
analysis in the form intended for the final threshold check:
K log 2≥150letssqrt(n log n)pay for the5 log npart of the simplified width budget;- one width condition pays for the remaining constant;
- the stack margin is split into
sqrt(n log n)and constant lower bounds.
Same large-n wrapper, but the split budget is discharged by the explicit
quadratic cutoff (128K^2)^2≤n0, and the stack constant budget is discharged
by checking it once at n0.
Log-linear stack-budget wrapper. The stack square-root side condition is
replaced by 16 log n≤n c^2, where
c=log(4/3)-log(2)/3.
Cutoff-budget wrapper. The split, width constant, and stack constant deterministic side conditions are all checked at the cutoff. The only remaining quantified deterministic budget is the log-linear stack estimate.
Deterministic-cutoff version of the current upper-bound wrapper. At this level the non-Chernoff side conditions are all finite cutoff inequalities: split, width constant, stack log-linear, and stack constant.
Chernoff-reduced version of the deterministic-cutoff wrapper. The raw
left/right logarithmic Chernoff hypotheses are replaced by the standard
annulus-width exponent condition for λ=3w/(a+1).
Chernoff wrapper with the natural choice E_n = 6 log n. The two
structural Chernoff side conditions rIn≤a/3-w and λ≤1 are both discharged
from the single annulus condition 3w≤a.
Same Chernoff-six-log wrapper, with the exponent condition stated as the
squared-width lower bound 12(a+1)log n≤w^2.
Core-width version of the final Chernoff wrapper. The remaining Chernoff
side conditions are now stated using the real expression
A sqrt(a log(2n^2)) inside the width ceiling:
3(core+1)≤amakes the actual integer width satisfy3w≤a;core≥9gives the right-tail floor-slack condition;12(a+1)log n≤core^2gives the six-log Chernoff exponent.
Final analytic-budget wrapper before choosing explicit numerical constants. The non-Chernoff deterministic thresholds remain finite cutoff checks, while the annulus Chernoff hypotheses are reduced to:
- a coarse upper bound making the annulus width fit inside
a/3; - one cutoff check implying
core≥9thereafter; - the constant inequality
A^2≥16, which gives the six-log Chernoff exponent.
A quadratic cutoff sufficient for the coarse annulus-width fit
3(A sqrt(3n log n)+1)≤3n/4. This is the same split estimate with
the coefficient A sqrt 3.
Cutoff-only annulus analytic wrapper. Compared with
hasRealUpperBound_of_Kdom_finalAnalyticBudgets_finiteBase, the remaining
coarse width-fit hypothesis has also been collapsed to one quadratic cutoff
condition at n0.
Explicit-constant version with A=4 and K=217. All structural
constant inequalities are discharged; what remains is a finite list of cutoff
checks at n0.
Explicit-constant version with the width-fit cutoff discharged from the split cutoff.
Fully explicit upper-bound theorem with A=4, K=217, conditional only
on the split cutoff.
A concrete cutoff large enough for the explicit constants A=4,
K=217. It is exactly (128 * 217^2)^2.
Equations
- PebblingLean.Hypercube.PaperParameters.explicitCutoff = 36329454321664
Instances For
Fully explicit paper-parameter upper bound. The constant is not optimized;
it is the finite-base normalized constant generated by the recursive schedule
with A=4, K=217, and n0 = 36,329,454,321,664.
Any relationally optimal pebbling number is bounded above by the explicit constant generated by the formal upper-bound construction.
Final packaged asymptotic bounds for any k certified as the optimal
pebbling number of Q_n: the formal lower bound and the explicit real upper
bound.