Lax Lean Archive

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

Correctness of the complete recursive unweighted algorithm

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

    An explicit recursive function uses exhaustive search for small targets and bounded projected round-or-cut search for larger targets. Child calls operate on canonically labeled balanced parts. Descending target search returns an independent set with the requested approximation ratio.

    Concept map
    93 concepts; 2 descendants 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 balancedseparatorProtected 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 unionA 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 pathsInteger 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 repliesGraph-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–cutalgorithmMaximum-weight independent set and itsencodingPolynomial 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.ProjectedOracle
    2import Lax263307.ExhaustiveTargets
    3import Lax263307.RecursionDepth
    4import Lax263307.TargetSearch
    5
    6/-!
    7---
    8title: Correctness of the complete recursive unweighted algorithm
    9type: theorem
    10---
    11An explicit recursive function uses exhaustive search for small targets and
    12bounded projected round-or-cut search for larger targets. Child calls operate
    13on canonically labeled balanced parts. Descending target search returns an
    14independent set with the requested approximation ratio.
    15
    16# Formalization notes
    17
    18The depth budget terminates every call. Induction discharges the child-query
    19hypothesis of the projected oracle, including sound rejection. The accuracy
    20denominator is 4(depth(n)+1)ceil(1/epsilon). This proves correctness of the
    21computable function; a finite RAM implementation and its uniform complexity
    22bound are still needed for the main theorem.
    23-/
    24
    25namespace Lax263307.RecursiveAlgorithm
    26
    27open ComputedSeparators AlgorithmParameters
    28
    29def attempt (lp flow : List ℕ → List ℕ) (a K B D : ℕ) (fuel : ℕ)
    30 {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (k : ℕ) : Option (Finset (Fin n)) :=
    31 if k ≤ cutoff a K B n D ∨ n ≤ 1 then ExhaustiveTargets.findIndependentSet G k
    32 else if n < k then none
    33 else match fuel with
    34 | 0 => none
    35 | fuel + 1 => ProjectedOracle.search lp flow a K B D G k
    36 (fun C t => (attempt lp flow a K B D fuel (restriction G C) t).map
    37 (fun I => I.image (label C)))
    38termination_by fuel
    39
    40def solve {n : ℕ} (lp flow : List ℕ → List ℕ) (a K B D : ℕ)
    41 (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] : Finset (Fin n) × ℕ :=
    42 TargetSearch.search (attempt lp flow a K B D (RecursionDepth.depth n) G) n
    43
    44def Correct {n : ℕ} (G : SimpleGraph (Fin n)) (k fuel D : ℕ) : Option (Finset (Fin n)) → Prop
    45 | some I => G.IsIndepSet (I : Set (Fin n)) ∧ (1 - 4*(1/(D:ℝ)))^fuel * (k:ℝ) ≤ I.card
    46 | none => ∀ J : Finset (Fin n), G.IsIndepSet (J : Set (Fin n)) → J.card < k
    47
    48def accuracyDenominator (n : ℕ) (ε : ℚ) : ℕ :=
    49 4 * (RecursionDepth.depth n + 1) * ⌈ε⁻¹⌉₊
    50
    51def independentSet {n : ℕ} (lp flow : List ℕ → List ℕ) (a K B : ℕ)
    52 (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (ε : ℚ) : Finset (Fin n) :=
    53 (solve lp flow a K B (accuracyDenominator n ε) G).1
    54
    55open GraphClasses PowerBagBounds
    56
    57axiom exists_solver (C : GraphClass) (hereditary : IsHereditary C)
    58 (a A : ℕ) (ha : 0 < a) (hA : 0 < A) (class_bound : HasPowerBagBound C a A) :
    59 ∃ (lp flow : List ℕ → List ℕ) (K B : ℕ),
    60 Lax759944.RamPolytime.RamPolytime lp ∧ Lax759944.RamPolytime.RamPolytime flow ∧
    61 0 < K ∧ 0 < B ∧ ∀ (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj],
    62 G ∈ C n → ∀ ε : ℚ, 0 < ε → ε < 1 →
    63 Lax263307.WeightedIndependentSet.IsApproximation G (fun _ => 1) ε
    64 (independentSet lp flow a K B G ε)
    65
    66end Lax263307.RecursiveAlgorithm
    67
    Show Proof
    Formalization notes

    The depth budget terminates every call. Induction discharges the child-query hypothesis of the projected oracle, including sound rejection. The accuracy denominator is 4(depth(n)+1)ceil(1/epsilon). This proves correctness of the computable function; a finite RAM implementation and its uniform complexity bound are still needed for the main theorem.

    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…