Lax Lean Archive

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

Depth and approximation loss of balanced recursion

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

    A recursive call on a balanced component has at most ⌊2n/3⌋\lfloor2n/3\rfloor vertices. The number of nontrivial calls on a branch is therefore logarithmic in the original graph order. A factor 1−δ1-\delta lost at each of at most λ\lambda levels retains at least 1−λδ1-\lambda\delta of a certified upper bound.

    Concept map
    3 concepts; 10 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 approximation_transfer proven

    2 balanced_decrease proven

    3 logarithmic_bound proven

    Lean source view on GitHub

    1import Lax263307.WeightedIndependentSet
    2import Mathlib.Data.Nat.Log
    3
    4/-!
    5---
    6title: Depth and approximation loss of balanced recursion
    7type: theorem
    8---
    9A recursive call on a balanced component has at most ⌊2n/3⌋\lfloor2n/3\rfloor
    10vertices. The number of nontrivial calls on a branch is therefore logarithmic
    11in the original graph order. A factor 1−δ1-\delta lost at each of at most
    12λ\lambda levels retains at least 1−λδ1-\lambda\delta of a certified upper bound.
    13
    14# Formalization notes
    15
    16The integer depth function avoids numerical evaluation of logarithms with
    17base 3/23/2. Empty graphs and singletons have depth zero. The explicit upper
    18bound uses twice the binary logarithm; this constant change does not affect
    19the QPTAS bound.
    20
    21# Attribution
    22
    23Bonnet–Chang, the recursion-depth argument in Lemma 14 and Bernoulli's
    24inequality in Theorem 15.
    25-/
    26
    27namespace Lax263307.RecursionDepth
    28
    29/-- Number of balanced reductions needed to reach order at most one. -/
    30def depth (n : ℕ) : ℕ :=
    31 if n ≤ 1 then 0 else 1 + depth (2 * n / 3)
    32termination_by n
    33decreasing_by omega
    34
    35/-- A balanced recursive call consumes one level. -/
    36axiom balanced_decrease (n m : ℕ) (nontrivial : 1 < n) (balanced : 3 * m ≤ 2 * n) :
    37 depth m + 1 ≤ depth n
    38
    39/-- At most two reductions are needed per binary-logarithm level. -/
    40axiom logarithmic_bound (n : ℕ) : depth n ≤ 2 * (Nat.log2 n + 1)
    41
    42/-- A certified independence upper bound turns the accumulated loss into approximation. -/
    43axiom approximation_transfer {n : ℕ} (G : SimpleGraph (Fin n))
    44 (I : Finset (Fin n)) (u levels : ℕ) (δ ε : ℚ)
    45 (independent : G.IsIndepSet (I : Set (Fin n)))
    46 (upper_bound : ∀ J : Finset (Fin n), G.IsIndepSet (J : Set (Fin n)) → J.card ≤ u)
    47 (δ_nonnegative : 0 ≤ δ) (δ_small : δ ≤ 1)
    48 (ε_small : ε ≤ 1) (loss : (levels : ℚ) * δ ≤ ε)
    49 (size : (1 - δ) ^ levels * (u : ℚ) ≤ I.card) :
    50 WeightedIndependentSet.IsApproximation G (fun _ => 1) ε I
    51
    52end Lax263307.RecursionDepth
    53
    Show ProofShow ProofShow Proof
    Formalization notes

    The integer depth function avoids numerical evaluation of logarithms with base 3/23/2. Empty graphs and singletons have depth zero. The explicit upper bound uses twice the binary logarithm; this constant change does not affect the QPTAS bound.

    Attribution

    Bonnet–Chang, the recursion-depth argument in Lemma 14 and Bernoulli's inequality in Theorem 15.

    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…