Lax Lean Archive

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

Explicit integer budgets for the round-or-cut algorithm

Lax263307.AlgorithmParameters · concepts/Lax263307/AlgorithmParameters.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

    Fixed class constants and an integer accuracy denominator determine the load, edge sparsity, conditioning level, and small-target cutoff. The conditioning moment floor supplies a uniform protected radius. A larger integer precision budget makes that dyadic radius small enough using only natural arithmetic and powers of two.

    Concept map
    25 concepts; 6 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

    1 budgets proven

    2 conditioning_floor proven

    3 protected_radius proven

    Lean source view on GitHub

    1import Lax263307.MomentLP
    2import Lax263307.HeavyConditioning
    3import Lax263307.RoundedOracleSearch
    4import Mathlib.Data.Nat.Log
    5
    6/-!
    7---
    8title: Explicit integer budgets for the round-or-cut algorithm
    9type: theorem
    10---
    11Fixed class constants and an integer accuracy denominator determine the
    12load, edge sparsity, conditioning level, and small-target cutoff.
    13The conditioning moment floor supplies a uniform protected radius.
    14A larger integer precision budget makes that dyadic radius small enough
    15using only natural arithmetic and powers of two.
    16
    17# Formalization notes
    18
    19The precision budget is the protected-radius denominator plus two.
    20That denominator is quasipolynomial in the input order and accuracy, so
    21this conservative choice also gives a quasipolynomial iteration budget.
    22The resource estimate and concrete RAM execution are separate obligations.
    23-/
    24
    25namespace Lax263307.AlgorithmParameters
    26
    27def logarithm (n : ℕ) : ℕ := Nat.log2 (2 * n) + 1
    28def load (B n D : ℕ) : ℕ := 12 * B * D * logarithm n
    29def targetThreshold (a K B n D : ℕ) : ℕ := K * (load B n D + 1) ^ (4 * a + 2)
    30def sparsity (a K B n D : ℕ) : ℕ := 2 * targetThreshold a K B n D
    31def level (a K B n D : ℕ) : ℕ := sparsity a K B n D * (Nat.log2 n + 1)
    32def cutoff (a K B n D : ℕ) : ℕ := max (targetThreshold a K B n D) (level a K B n D)
    33def floorDenominator (a K B n D : ℕ) : ℕ :=
    34 2 * n * sparsity a K B n D * (Nat.log2 n + 1)
    35def momentFloor (a K B n D : ℕ) : ℚ :=
    36 1 / (floorDenominator a K B n D : ℚ) ^ level a K B n D
    37def radiusDenominator (a K B n D : ℕ) : ℕ :=
    38 256 * MomentLP.dimension n (level a K B n D) * n ^ 2 * D ^ 2 *
    39 floorDenominator a K B n D ^ level a K B n D
    40def precision (a K B n D : ℕ) : ℕ := radiusDenominator a K B n D + 2
    41def iterations (a K B n D : ℕ) : ℕ :=
    42 RoundedOracleSearch.steps (MomentLP.dimension n (level a K B n D)) (precision a K B n D)
    43
    44axiom budgets {a K B n D k : ℕ} (hK : 0 < K) (hB : 0 < B)
    45 (hD : 4 ≤ D) (large : cutoff a K B n D < k) :
    46 0 < load B n D ∧ 0 < sparsity a K B n D ∧ 0 < level a K B n D ∧
    47 0 < (1 / (D : ℝ)) ∧ (1 / (D : ℝ)) ≤ 1 / 4 ∧
    48 12 * (B : ℝ) * ((Nat.log2 (2 * n) : ℝ) + 1) ≤
    49 (1 / (D : ℝ)) * load B n D ∧
    50 (sparsity a K B n D : ℝ) * ((Nat.log2 n : ℝ) + 1) ≤ level a K B n D ∧
    51 (K : ℝ) * ((load B n D : ℝ) + 1) ^ (4 * a + 2) ≤ k ∧
    52 (2 * K : ℝ) * ((load B n D : ℝ) + 1) ^ (4 * a + 2) ≤ sparsity a K B n D
    53
    54axiom conditioning_floor (a K B n D : ℕ) :
    55 (momentFloor a K B n D : ℝ) =
    56 HeavyConditioning.probabilityFloor n (sparsity a K B n D) ^ level a K B n D
    57
    58axiom protected_radius {a K B n D : ℕ} (hK : 0 < K) (hn : 0 < n) (hD : 0 < D) :
    59 2 ≤ precision a K B n D ∧
    60 ((2 : ℝ) ^ precision a K B n D)⁻¹ ≤
    61 (momentFloor a K B n D : ℝ) /
    62 (256 * (MomentLP.dimension n (level a K B n D) : ℝ) * (n : ℝ) ^ 2 * (D : ℝ) ^ 2)
    63
    64end Lax263307.AlgorithmParameters
    65
    Show ProofShow ProofShow Proof
    Formalization notes

    The precision budget is the protected-radius denominator plus two. That denominator is quasipolynomial in the input order and accuracy, so this conservative choice also gives a quasipolynomial iteration budget. The resource estimate and concrete RAM execution are separate obligations.

    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…