Lax Lean Archive

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

The split flow-cut certificate must give a cheap separation

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

    In a hereditary class with a power bag bound, sufficiently large target and sparsity parameters rule out the high-flow branch of the directed split certificate. If γk≤ℓn2\gamma k\le\ell n^2, its projected route loads would meet the forbidden bounded-load distribution hypotheses. The returned cut therefore projects to two nonempty covering shores with no cross edge and separator cost at most 4ρ∣A∣∣B∣/γ4\rho|A||B|/\gamma.

    Concept map
    45 concepts; 7 descendants hidden
    100%
    TreewidthTreewidth transfer through analmost-embeddingConditioning graph routes on uniformendpointsBags meeting a connected vertex setTree-decomposition transfer throughconnected vertex representationsA width obstruction from sparse costs andbounded route loadsCoupled route sampling with shared verteximagesA good coupled sample with bounded totalroute sizeTreewidth loss under edge deletionEntropy and adjacency massFinite product sampling and coordinatemarginalsThe split flow-cut certificate must give acheap separationHereditary graph classesRestricting an induced almost-embedding toits route unionA class width bound obstructs induced routesamplingFew edges in the graph induced by shortroutesAlmost-embedding transfer with isolatedsource verticesSparse bounded-load route distributions areimpossibleCollision and length bounds forindependently sampled pathsInteger power bounds on class decompositionbagsGraph-route distributions from high-valuesplit flowsDiscarding long almost-embedding routesUniform endpoint normalization of finitepath flowsAn induced almost-embedding from a goodroute sampleChoosing a collision-free outcome withbounded total path lengthControlled-size subcubic source graphs oflinear treewidthProjecting split paths and preservingendpoint loadsVertex splitting for the directed flow–cutalgorithmPolynomial order bound from the sampledwidth inequalityConcurrent fractional flowExact flow–cut output certificatesProduct multicommodity networks andsparsest cutsDeterministic directed uniform flow–cutalgorithmRational flow instances and certificatesBinary encoding of finite wordsPolynomial-time computation by a wordRAMThe word RAMThe Constructor Meets the Requested OrderEdge Expansion and Subcubic GraphsThe Explicit Family Has Linear TreewidthSelecting and Encoding the ConstructedGraphsRotation Map of the Fixed Powered SeedDeterministic Search for a Fixed ExpanderSeedThe Explicit Graphs Are SubcubicExplicit Zig-Zag Family and PathReplacement
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax263307.NoBoundedLoadRoutes
    2import Lax263307.RouteDistributions
    3import Lax263307.VertexSplitting
    4
    5/-!
    6---
    7title: The split flow-cut certificate must give a cheap separation
    8type: theorem
    9---
    10In a hereditary class with a power bag bound, sufficiently large target and
    11sparsity parameters rule out the high-flow branch of the directed split
    12certificate. If γk≤ℓn2\gamma k\le\ell n^2, its projected route loads would
    13meet the forbidden bounded-load distribution hypotheses. The returned cut
    14therefore projects to two nonempty covering shores with no cross edge and
    15separator cost at most 4ρ∣A∣∣B∣/γ4\rho|A||B|/\gamma.
    16
    17# Formalization notes
    18
    19The shores are the actual minus/plus port projections of the certificate's
    20cut. This is the certificate analysis needed by the repeated-cut procedure;
    21the registered RAM solver and the wrapper cost are handled separately.
    22The power bag premise is still to be derived from the main separator premise.
    23
    24# Attribution
    25
    26Bonnet–Chang, Lemma 7 with its high-flow branch excluded by Lemma 11.
    27-/
    28
    29namespace Lax263307.ForcedSeparation
    30
    31open scoped NNReal NNRat
    32open Lax263307.GraphClasses Lax263307.PowerBagBounds Lax263307.VertexSplitting
    33open Lax455465.ProductNetwork Lax455465.ConcurrentFlow
    34
    35axiom certificate_separation (C : GraphClass) (hereditary : IsHereditary C)
    36 (a A : ℕ) (a_positive : 0 < a) (A_positive : 0 < A) (class_bound : HasPowerBagBound C a A) :
    37 ∃ K : ℕ, 0 < K ∧ ∀ (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj],
    38 G ∈ C n → 0 < n → ∀ (x : Fin n → ℚ≥0) (large : ℚ≥0)
    39 (certificate : Lax455465.FlowCutCertificate.Certificate (2 * n)) (ρ γ k p : ℝ) (ℓ : ℕ),
    40 0 < ℓ → 0 ≤ ρ → 0 < γ → 0 < k → 0 < p →
    41 γ * k ≤ (ℓ : ℝ) * (n : ℝ) ^ 2 → (∀ v, (x v : ℝ) ≤ 1) →
    42 (∑ v, (x v : ℝ)) ≤ k →
    43 Lax263307.Entropy.edgeCost G (fun v => (x v : ℝ)) ≤ k ^ 2 / p →
    44 (K : ℝ) * ((ℓ : ℝ) + 1) ^ (4 * a + 2) ≤ k →
    45 (2 * K : ℝ) * ((ℓ : ℝ) + 1) ^ (4 * a + 2) ≤ p →
    46 AdmissibleCut (splitInstance G x large).weights certificate.cut →
    47 IsArcConcurrentFlow .directed (splitInstance G x large).network
    48 (splitInstance G x large).weights (certificate.flow.value : ℝ≥0) certificate.flow.flow →
    49 (ratioCost (splitInstance G x large).network (splitInstance G x large).weights certificate.cut : ℝ) ≤
    50 ρ * (certificate.flow.value : ℝ) →
    51 ρ * (2 * n : ℕ) ^ 2 / γ < (large : ℝ) →
    52 (leftShore certificate.cut).Nonempty ∧ (rightShore certificate.cut).Nonempty ∧
    53 leftShore certificate.cut ∪ rightShore certificate.cut = Finset.univ ∧
    54 (∀ u ∈ leftShore certificate.cut \ rightShore certificate.cut,
    55 ∀ v ∈ rightShore certificate.cut \ leftShore certificate.cut, ¬G.Adj u v) ∧
    56 (∑ v ∈ leftShore certificate.cut ∩ rightShore certificate.cut, (x v : ℝ)) ≤
    57 4 * ρ * (leftShore certificate.cut).card * (rightShore certificate.cut).card / γ
    58
    59end Lax263307.ForcedSeparation
    60
    Show Proof
    Formalization notes

    The shores are the actual minus/plus port projections of the certificate's cut. This is the certificate analysis needed by the repeated-cut procedure; the registered RAM solver and the wrapper cost are handled separately. The power bag premise is still to be derived from the main separator premise.

    Attribution

    Bonnet–Chang, Lemma 7 with its high-flow branch excluded by Lemma 11.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…