Lax Lean Archive

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

QPTAS for Max Weight Independent Set in Graphs with Strongly Edge-Sublinear Separators

lax-263307·formalized by Édouard Bonnet @EdouardBonnet·created ·GitHub @9459f3f·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this submission may be incorrect.

No flags have been submitted.

    Community review

    Flag this submission

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    Abstract

    A hereditary graph class has strongly edge-sublinear separators if its mm-edge graphs admit balanced separators of size O(mb)O(m^b) for some 0≤b<10\le b<1. Maximum-weight independent set admits a deterministic quasipolynomial-time approximation scheme on every such class. Given rational vertex weights and rational 0<ε<10<\varepsilon<1, the scheme returns an independent set of weight at least (1−ε)(1-\varepsilon) times the optimum in time exp⁡((ε−1log⁡(n+2))O(1))+(ℓ+1)O(1)\exp((\varepsilon^{-1}\log(n+2))^{O(1)})+(\ell+1)^{O(1)}, where ℓ\ell is the binary encoding length of the weights and accuracy and the constants depend only on the class. No separator is required as part of the input.

    Concepts

    Concept map
    115 concepts
    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 unionThe exact hull is nonempty precisely atfeasible targetsIndependent 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 exacthullQPTAS for maximum-weight independent setThe moment relaxation as an explicitrational linear programA fixed RAM program constructs therounded blow-upA fixed RAM program for themoment-coordinate catalogA fixed RAM program for exact small-targetsearchA fixed RAM program constructing thecomplete moment LPA uniform RAM program for the roundedellipsoid updateNative RAM execution of theweight-to-multiplicity reductionComputed rounding oracle near the momentrelaxationSparse bounded-load route distributions areimpossibleQuasipolynomial bounds for the computedalgorithm budgetsCollision and length bounds forindependently sampled pathsRemoving nonpositive weightsInteger power bounds on class decompositionbagsThe bounded projected round-or-cut searchDeterministic quasipolynomial-timeapproximation schemesExact 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 solveroutputIndependent-set encodings satisfy therelaxationCumulative 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 submissionOther submissionA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    Proofs

    Proof networkview on GitHub

    100%
    AlgorithmParameters123BlowUpBagBounds12BlowUpClasses12BlowUpDeletion123BlowUpIndependentSets12345BufferedEllipsoid1234ComponentCutEncoding12ComponentCuts12ConditionalRoutes123CoordinateCatalog12345CoupledRouteSampling1234CoupledSamplingBounds123CutTraces12DistanceProjection123456EdgeBagBounds12ExhaustiveTargets123FiniteProductSampling12HeavyConditioning12HeavyRecursiveRounding123InducedEmbeddingWidth123MomentLP123456PathSampling1234PositiveWeights12RationalConditioning123RationalCutBuffer12345678RationalProjection12RecursionDepth123RecursiveRounding12RelaxationFeasibility12RoundedOracleSearch1234RoundingBounds123RouteDistributions12RoutePruning12RoutingNormalization12SamplingOutcomes12SeparatorDecompositions12SplitPathProjection123StrongComponentGaps12345VertexSplitting12345Lax109476.CertificateExistenceLax109476.CertificateSoundnessLax109476.FarkasLemmaLax109476.FarkasSoundnessLax109476.FourierMotzkinLax109476.OptimalDualMultipliersLax109476.PolynomialTimeSolverLax109476.PrimalAttainmentLax109476.RationalFeasibilityLax109476.RecessionExistenceLax109476.RecessionSoundnessLax109476.StrongDualityLax109476.WeakDualityAlmostEmbeddingsBalancedPartitionsBlowUpDecompositionsComputedRoundingComputedSeparatorsConditionedCostsConditioningDistributionConditioningExistenceConnectedBagsConnectedRepresentationsCostSamplingObstructionEdgeDeletionWidthEntropyBoundsEntropyDecreaseEntropyGapForcedSeparationHeavyRationalConditioningHostRestrictionHullNonemptyInducedRouteEdgesIsolatedEmbeddingTransferLightSeparatorsMainTheoremNativeBlowUpNativeCatalogNativeExhaustiveNativeMomentLPNativeRoundedStepNativeWeightReductionNearOracleNoBoundedLoadRoutesParameterResourcesPowerBagBoundsProjectedOracleRecursiveAlgorithmRegisteredLPRepeatedCutAccountingSampledAlmostEmbeddingsSourceGraphsTargetSearchWeightedAlgorithmWeightedProjectionWidthGrowthLax455465.ArcToPathLax455465.RamDirectedSparsestCutLax455465.RamDirectedUniformFlowCutLax455465.RamProductFlowCutLax920634.ConstructionSizeLax920634.ExpansionTreewidthLax920634.ExplicitExpansionLax920634.ExplicitTreewidthLax920634.PathExpansionLax920634.SeedCorrectnessLax920634.SubcubicConstruction
    assumptions conclusionProven claimStatement 1, 2, … of a claim with several statementsClaim from this submission / another submissionProof — open large view for details
    Proof list

    Lean sources for these proofs: proofs/ on GitHub

    Proof code is not displayed; the archive records each proof's checked relationship between claims.

    Related submissions

    Submission map

    100%
    This submissionOther submissionA → B: B's concepts build on AA → B: only B's proofs build on A

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-263307,
  author = {Édouard Bonnet},
  title = {QPTAS for Max Weight Independent Set in Graphs with Strongly Edge-Sublinear Separators},
  year = {2026},
  howpublished = {Lax Archive, lax-263307},
  url = {https://laxarchive.org/lax-263307/},
  note = {draft},
}

    References

    1. Édouard Bonnet and Yeonsu Chang. QPTAS for Max Weight Independent Set in Graphs with Strongly Edge-Sublinear Separators. 2026. Manuscript, local PDF snapshot of 12 October 2026, Theorem 2.

    Discussion

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

    Loading discussion…