Lax Lean Archive

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

Correctness of the complete weighted approximation algorithm

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

    Clip negative weights, round them to copy multiplicities, and compute the unweighted approximation on the canonically numbered independent blow-up. Projection and removal of nonpositive-weight vertices give the requested weighted approximation. Empty and nonpositive instances return the empty set.

    Concept map
    104 concepts; 1 descendant hidden
    100%
    Soundness of exact rational LP certificatesCertificates of infeasibilityLinear programs and their dualsExact polynomial-time linear programmingon a word RAMExact rational solution certificatesBinary-size encoding of rational linearprogramsCertificates of unboundednessTreewidthExplicit integer budgets for the round-or-cutalgorithmTreewidth transfer through analmost-embeddingBalanced closed parts certify a balancedseparatorSublinear bag bounds survive independentblow-upsIndependent blow-up classes are hereditaryLifting a tree decomposition through abounded blow-upDeleting high-degree vertices in anindependent blow-upIndependent sets lift and project through ablow-upProtected balls for the rounded ellipsoidmethodInteger coefficients of recursive separatingcutsValid separating inequalities fromindependent-set boundsComputing the recursive answer-or-cutdecisionComputing balanced light separators fromregistered flow-cut outputsConditioning graph routes on uniformendpointsConditioning preserves bounded costs andtotal massJoint distributions for the entropy-decreaseargumentA small conditioning set gives low edge costBags meeting a connected vertex setTree-decomposition transfer throughconnected vertex representationsA computable catalog and index for momentcoordinatesA width obstruction from sparse costs andbounded route loadsCoupled route sampling with shared verteximagesA good coupled sample with bounded totalroute sizeRepeated cuts yield a balanced lightseparatorInfinity-distance projection LP and itsseparating dualEdge-sublinear separators implyedge-sublinear decomposition bagsTreewidth loss under edge deletionStrongly edge-sublinear separatorsEntropy and adjacency massEntropy lies between zero and the logarithmof the orderHigh edge cost forces a strict entropydecreaseEdge mass bounds the average entropydecreaseExhaustive search for small independent-settargetsFinite product sampling and coordinatemarginalsThe split flow-cut certificate must give acheap separationHereditary graph classesConditioning with a quantitative momentlower boundExact rational search above the conditioningmoment floorRecursive rounding after discarding lightpartsRestricting an induced almost-embedding toits route unionIndependent blow-ups and projectionA class width bound obstructs induced routesamplingFew edges in the graph induced by shortroutesAlmost-embedding transfer with isolatedsource verticesBalanced light separators from the registeredflow-cut solverThe independent-set relaxation and its exacthullThe moment relaxation as an explicitrational linear programComputed rounding oracle near the momentrelaxationSparse bounded-load route distributions areimpossibleCollision and length bounds forindependently sampled pathsRemoving nonpositive weightsInteger power bounds on class decompositionbagsThe bounded projected round-or-cut searchExact rational search for a conditioning setRational cut normals preserve protectedcubes after scalingRational LP certificates for distanceprojectionDepth and approximation loss of balancedrecursionCorrectness of the complete recursiveunweighted algorithmCombining recursive answers in round-or-cutDecoding the actual registered LP solveroutputCumulative separator cost over disjointdiscarded shoresA bounded rounded ellipsoid search withanswer-or-cut repliesRounding loses at most one weight unit pervertexGraph-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 lengthThe components left by deleting a separatorTree decompositions from recursive balancedseparatorsControlled-size subcubic source graphs oflinear treewidthProjecting split paths and preservingendpoint loadsQuantitative gaps for recursive componentcutsDescending target search in SolveVertex splitting for the directed flow–cutalgorithmScaling weights to integer multiplicitiesCorrectness of the complete weightedapproximation algorithmMaximum-weight independent set and itsencodingProjecting an unweighted approximationgives a weighted approximationPolynomial 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.RecursiveAlgorithm
    2import Lax263307.BlowUpBagBounds
    3import Lax263307.PositiveWeights
    4import Lax263307.WeightedProjection
    5import Mathlib.Algebra.BigOperators.Fin
    6
    7/-!
    8---
    9title: Correctness of the complete weighted approximation algorithm
    10type: theorem
    11---
    12Clip negative weights, round them to copy multiplicities, and compute the
    13unweighted approximation on the canonically numbered independent blow-up.
    14Projection and removal of nonpositive-weight vertices give the requested
    15weighted approximation. Empty and nonpositive instances return the empty set.
    16
    17# Formalization notes
    18
    19The algorithm is a computable function using the fixed registered LP and
    20flow solvers. The copy labeling is the computable finite-sigma equivalence.
    21This closes functional correctness for signed rational weights, including
    22the recursive search. It does not yet assert a complete RAM execution or
    23its quasipolynomial time and word-length bounds.
    24-/
    25
    26namespace Lax263307.WeightedAlgorithm
    27
    28open WeightRounding IndependentBlowUp PositiveWeights
    29
    30def labeling {n : ℕ} (copies : Fin n → ℕ) : Fin (∑ v, copies v) ≃ Vertex copies :=
    31 finSigmaFinEquiv.symm
    32
    33def numbered {n : ℕ} (G : SimpleGraph (Fin n)) (copies : Fin n → ℕ) :
    34 SimpleGraph (Fin (∑ v, copies v)) := (graph G copies).comap (labeling copies)
    35
    36instance {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (copies : Fin n → ℕ) :
    37 DecidableRel (numbered G copies).Adj := fun _ _ => inferInstanceAs (Decidable (G.Adj _ _))
    38
    39def solve {n : ℕ} (lp flow : List ℕ → List ℕ) (a K B : ℕ)
    40 (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (w : Fin n → ℚ) (ε : ℚ) : Finset (Fin n) :=
    41 let w' := positiveWeights w
    42 if n = 0 ∨ maximumWeight w' ≤ 0 then ∅
    43 else
    44 let copies' := copies w' ε
    45 let I := RecursiveAlgorithm.independentSet lp flow a K B (numbered G copies') (ε/2)
    46 discardNonpositive w (project (I.image (labeling copies')))
    47
    48open GraphClasses EdgeSublinearSeparators WeightedIndependentSet
    49
    50axiom exists_solver (C : GraphClass) (hereditary : IsHereditary C)
    51 (separators : HasStronglyEdgeSublinearSeparators C) :
    52 ∃ (lp flow : List ℕ → List ℕ) (a K B : ℕ),
    53 Lax759944.RamPolytime.RamPolytime lp ∧ Lax759944.RamPolytime.RamPolytime flow ∧
    54 0 < a ∧ 0 < K ∧ 0 < B ∧
    55 ∀ (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj], G ∈ C n →
    56 ∀ (w : Fin n → ℚ) (ε : ℚ), 0 < ε → ε < 1 → IsApproximation G w ε (solve lp flow a K B G w ε)
    57
    58end Lax263307.WeightedAlgorithm
    59
    Show Proof
    Formalization notes

    The algorithm is a computable function using the fixed registered LP and flow solvers. The copy labeling is the computable finite-sigma equivalence. This closes functional correctness for signed rational weights, including the recursive search. It does not yet assert a complete RAM execution or its quasipolynomial time and word-length bounds.

    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…