Lax Lean Archive

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

Independent-set encodings satisfy the relaxation

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

    Every independent set II of size kk gives a feasible point of Rr(G,k)R_r(G,k) by setting yA=1[A⊆I]y_A=\mathbf1[A\subseteq I]. Consequently Pr(G,k)⊆Rr(G,k)P_r(G,k)\subseteq R_r(G,k).

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

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

    1 hull_feasible proven

    2 indicator_feasible proven

    Lean source view on GitHub

    1import Lax263307.LinearRelaxation
    2
    3/-!
    4---
    5title: Independent-set encodings satisfy the relaxation
    6type: theorem
    7---
    8Every independent set II of size kk gives a feasible point of Rr(G,k)R_r(G,k)
    9by setting yA=1[A⊆I]y_A=\mathbf1[A\subseteq I]. Consequently
    10Pr(G,k)⊆Rr(G,k)P_r(G,k)\subseteq R_r(G,k).
    11
    12# Attribution
    13
    14Bonnet–Chang, Section 4, equation (13), and Section 5.1, equation (20).
    15-/
    16
    17namespace Lax263307.RelaxationFeasibility
    18
    19open LinearRelaxation
    20
    21/-- All indicator encodings satisfy the five families of constraints. -/
    22axiom indicator_feasible {n : ℕ} (G : SimpleGraph (Fin n)) (k r : ℕ)
    23 (I : Finset (Fin n)) (independent : G.IsIndepSet (I : Set (Fin n)))
    24 (cardinality : I.card = k) : IsFeasible G k r (indicator r I)
    25
    26/-- The exact independent-set hull is contained in the relaxation. -/
    27axiom hull_feasible {n : ℕ} (G : SimpleGraph (Fin n)) (k r : ℕ)
    28 (y : MomentVector n r) (member : y ∈ independentSetHull G k r) :
    29 IsFeasible G k r y
    30
    31end Lax263307.RelaxationFeasibility
    32
    Show ProofShow Proof

    Attribution

    Bonnet–Chang, Section 4, equation (13), and Section 5.1, equation (20).

    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…