Lax Lean Archive

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

Integer coefficients of recursive separating cuts

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

    The cut for a part CC and bound uu is

    ∑v∈CzA∪{v}−uzA≤0.\sum_{v\in C}z_{A\cup\{v\}}-u z_A\le0.

    After repeated coordinates are collected, every coefficient is an integer with absolute value at most nn, provided u≤nu\le n. This is the coefficient bound required for the oracle's rational arithmetic.

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

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

    1 coefficient_bound proven

    2 evaluation_identity proven

    Lean source view on GitHub

    1import Lax263307.ComponentCuts
    2import Mathlib.Data.Fintype.Powerset
    3
    4/-!
    5---
    6title: Integer coefficients of recursive separating cuts
    7type: theorem
    8---
    9The cut for a part CC and bound uu is
    10∑v∈CzA∪{v}−uzA≤0.\sum_{v\in C}z_{A\cup\{v\}}-u z_A\le0.
    11After repeated coordinates are collected, every coefficient is an integer
    12with absolute value at most nn, provided u≤nu\le n. This is the coefficient
    13bound required for the oracle's rational arithmetic.
    14
    15# Attribution
    16
    17Bonnet–Chang, Lemma 13 and Section 5.3.
    18-/
    19
    20namespace Lax263307.ComponentCutEncoding
    21
    22open LinearRelaxation
    23
    24/-- The coefficient at one coordinate, after collecting all repeated terms. -/
    25def coefficient {n r : ℕ} (A C : Finset (Fin n)) (u : ℕ)
    26 (B : Coordinate n r) : ℤ :=
    27 (∑ v ∈ C, if insert v A = B.val then 1 else 0) -
    28 if A = B.val then (u : ℤ) else 0
    29
    30/-- Evaluate the coefficient vector in the real coordinate space. -/
    31noncomputable def evaluate {n r : ℕ} (a : Coordinate n r → ℤ)
    32 (z : MomentVector n r) : ℝ := ∑ B, (a B : ℝ) * z B
    33
    34/-- The collected coefficient vector represents exactly the intended cut. -/
    35axiom evaluation_identity {n r : ℕ} (A C : Finset (Fin n)) (u : ℕ)
    36 (size : A.card ≤ r) (z : MomentVector n r) :
    37 evaluate (coefficient A C u) z =
    38 (∑ v ∈ C, value z (insert v A)) - (u : ℝ) * value z A
    39
    40/-- Each coefficient has magnitude at most the graph order. -/
    41axiom coefficient_bound {n r : ℕ} (A C : Finset (Fin n)) (u : ℕ)
    42 (bound : u ≤ n) (B : Coordinate n r) :
    43 |coefficient A C u B| ≤ (n : ℤ)
    44
    45end Lax263307.ComponentCutEncoding
    46
    Show ProofShow Proof

    Attribution

    Bonnet–Chang, Lemma 13 and Section 5.3.

    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…