Documentation

LeanPool.PebblingLean.Paper

Paper-facing formulation #

This file contains wrappers whose statements follow the exposition in the paper. The proof-producing modules use relational predicates and explicit integer cost bounds; here we package those results as statements about a noncomputable optimal pebbling number optimalPebblingNumber n and the explicit constant CLean.

source
def PebblingLean.Hypercube.Paper.N0 :
ℕ

The finite cutoff used by the fully explicit Lean upper bound.

Equations
Instances For
    source
    theorem PebblingLean.Hypercube.Paper.N0_eq :
    N0 = 36329454321664
    source
    theorem PebblingLean.Hypercube.Paper.N0_pos :
    0 < N0
    source
    noncomputable def PebblingLean.Hypercube.Paper.CLean :
    ℝ

    The explicit constant certified by the Lean proof.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem PebblingLean.Hypercube.Paper.CLean_nonneg :
      0 ≤ CLean
      source
      theorem PebblingLean.Hypercube.Paper.CLean_eq_paper_formula :
      CLean = Real.exp (4 / ↑N0 ^ 2) * ∑ j ∈ Finset.range N0, 2 ^ (j / 5) * (3 / 2) ^ j

      The same constant in the displayed form used in the paper.

      source
      theorem PebblingLean.Hypercube.Paper.one_le_CLean_sum :
      1 ≤ ∑ j ∈ Finset.range N0, 2 ^ (j / 5) * (3 / 2) ^ j
      source
      theorem PebblingLean.Hypercube.Paper.CLean_pos :
      0 < CLean
      source
      theorem PebblingLean.Hypercube.Paper.exists_solvable_size (n : ℕ) :
      ∃ (k : ℕ), Pebbling.HasSolvableSize (graph n) k

      There is always at least one solvable distribution on Q_n: put one pebble on every vertex.

      source
      noncomputable def PebblingLean.Hypercube.Paper.optimalPebblingNumber (n : ℕ) :
      ℕ

      A noncomputable version of the optimal pebbling number o(Q_n). The paper works with this number; the main proof modules avoid choosing it by using the relational predicate IsOptimalNumber.

      Equations
      Instances For
        source
        theorem PebblingLean.Hypercube.Paper.optimalPebblingNumber_hasSolvableSize (n : ℕ) :
        Pebbling.HasSolvableSize (graph n) (optimalPebblingNumber n)
        source
        theorem PebblingLean.Hypercube.Paper.isOptimalNumber_optimalPebblingNumber (n : ℕ) :
        Pebbling.IsOptimalNumber (graph n) (optimalPebblingNumber n)
        source
        theorem PebblingLean.Hypercube.Paper.lower_bound (n : ℕ) :
        (4 / 3) ^ n ≤ ↑(optimalPebblingNumber n)

        Paper lower bound: o(Q_n) ≥ (4/3)^n.

        source
        theorem PebblingLean.Hypercube.Paper.lower_bound_real (n : ℕ) :
        (4 / 3) ^ n ≤ ↑(optimalPebblingNumber n)

        Real-valued form of the paper lower bound.

        source
        theorem PebblingLean.Hypercube.Paper.upper_bound (n : ℕ) :
        ↑(optimalPebblingNumber n) ≤ CLean * (4 / 3) ^ n

        Paper upper bound with the explicit Lean constant.

        source
        theorem PebblingLean.Hypercube.Paper.bounds (n : ℕ) :
        (4 / 3) ^ n ≤ ↑(optimalPebblingNumber n) ∧ ↑(optimalPebblingNumber n) ≤ CLean * (4 / 3) ^ n

        The two inequalities in the final theorem, stated directly for optimalPebblingNumber.

        source
        theorem PebblingLean.Hypercube.Paper.optimalPebblingNumber_theta :
        ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), (4 / 3) ^ n ≤ ↑(optimalPebblingNumber n) ∧ ↑(optimalPebblingNumber n) ≤ C * (4 / 3) ^ n

        Paper conclusion: the optimal pebbling number of the hypercube has order (4/3)^n. This is stated as an explicit two-sided big-Theta witness.