Lax Lean Archive

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

Integer power bounds on class decomposition bags

Lax263307.PowerBagBounds · concepts/Lax263307/PowerBagBounds.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 uniform bound ∣B∣a≤A(m+1)a−1|B|^a\le A(m+1)^{a-1} gives the monotone bag-size function W(m)=⌊A(m+1)a−1a⌋W(m)=\lfloor\sqrt[a]{A(m+1)^{a-1}}\rfloor. For a,A>0a,A>0, this function is at least one and obeys the same power bound. Integer powers suffice for the sampled width contradiction once separators yield such a class bound.

    Concept map
    32 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax263307.InducedEmbeddingWidth
    2import Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
    3
    4/-!
    5---
    6title: Integer power bounds on class decomposition bags
    7type: theorem
    8---
    9A uniform bound ∣B∣a≤A(m+1)a−1|B|^a\le A(m+1)^{a-1} gives the monotone bag-size function
    10W(m)=⌊A(m+1)a−1a⌋W(m)=\lfloor\sqrt[a]{A(m+1)^{a-1}}\rfloor. For a,A>0a,A>0, this function
    11is at least one and obeys the same power bound. Integer powers suffice for
    12the sampled width contradiction once separators yield such a class bound.
    13
    14# Attribution
    15
    16An integer form of the sublinear width bound used in Bonnet–Chang's Lemma 11.
    17-/
    18
    19namespace Lax263307.PowerBagBounds
    20
    21open Lax263307.GraphClasses Lax263307.InducedEmbeddingWidth Lax228581.Treewidth
    22
    23def HasPowerBagBound (C : GraphClass) (a A : ℕ) : Prop :=
    24 ∀ n (G : SimpleGraph (Fin n)), G ∈ C n → ∃ D : TreeDecomposition G,
    25 ∀ i, (D.bag i).card ^ a ≤ A * (G.edgeSet.ncard + 1) ^ (a - 1)
    26
    27def bagBound (a A m : ℕ) : ℕ := Nat.nthRoot a (A * (m + 1) ^ (a - 1))
    28
    29axiom root_bag_bound (C : GraphClass) (a A : ℕ) (a_positive : 0 < a) (A_positive : 0 < A)
    30 (class_bound : HasPowerBagBound C a A) :
    31 Monotone (bagBound a A) ∧ HasBagBound C (bagBound a A) ∧
    32 (∀ m, 1 ≤ bagBound a A m) ∧
    33 (∀ m, (bagBound a A m) ^ a ≤ A * (m + 1) ^ (a - 1))
    34
    35end Lax263307.PowerBagBounds
    36
    Show Proof

    Attribution

    An integer form of the sublinear width bound used in Bonnet–Chang's Lemma 11.

    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…