Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Quasipolynomial bounds for the computed algorithm budgets

Lax263307.ParameterResources · concepts/Lax263307/ParameterResources.lean · lax-263307

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    For fixed class constants, the graph order, accuracy denominator, load, edge sparsity, conditioning level, moment dimension, protected-radius precision, ellipsoid iteration count, and small-target enumeration bound all fit one quasipolynomial bound in D times the binary-logarithm scale.

    Concept map
    26 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax263307.AlgorithmParameters
    2
    3/-!
    4---
    5title: Quasipolynomial bounds for the computed algorithm budgets
    6type: theorem
    7---
    8For fixed class constants, the graph order, accuracy denominator, load,
    9edge sparsity, conditioning level, moment dimension, protected-radius
    10precision, ellipsoid iteration count, and small-target enumeration bound
    11all fit one quasipolynomial bound in D times the binary-logarithm scale.
    12
    13# Formalization notes
    14
    15The proof supplies fixed positive natural constants before n and D.
    16It bounds the actual integer formulas used by the algorithm, including
    17its conservative precision choice. Polynomial work in these resources
    18and amplification through logarithmic recursion still need their RAM
    19correctness and running-time proofs.
    20-/
    21
    22namespace Lax263307.ParameterResources
    23
    24open AlgorithmParameters
    25
    26def resource (a K B n D : ℕ) : ℕ :=
    27 n + D + load B n D + sparsity a K B n D + level a K B n D +
    28 Lax263307.MomentLP.dimension n (level a K B n D) + radiusDenominator a K B n D +
    29 precision a K B n D + iterations a K B n D + (n + 1) ^ cutoff a K B n D
    30
    31axiom resource_bound (a K B : ℕ) (hK : 0 < K) :
    32 ∃ C d : ℕ, 0 < C ∧ 0 < d ∧ ∀ n D : ℕ, 0 < n → 0 < D →
    33 resource a K B n D ≤ 2 ^ (C * (D * logarithm n) ^ d)
    34
    35end Lax263307.ParameterResources
    36
    Show Proof
    Formalization notes

    The proof supplies fixed positive natural constants before n and D. It bounds the actual integer formulas used by the algorithm, including its conservative precision choice. Polynomial work in these resources and amplification through logarithmic recursion still need their RAM correctness and running-time proofs.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…