Lax Lean Archive

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

The bounded projected round-or-cut search

Lax263307.ProjectedOracle · concepts/Lax263307/ProjectedOracle.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 actual registered LP certificate decides whether to reject, separate by a projection cut, or call the computed near-relaxation oracle. Both cut branches preserve the same explicit dyadic cube about every scaled independent-set encoding. The bounded rounded ellipsoid loop therefore returns an approximate independent set or a valid upper bound strictly below the requested positive target.

    Concept map
    90 concepts; 3 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 entropydecreaseFinite 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 balancedrecursionCombining 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 componentcutsVertex 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.NearOracle
    2import Lax263307.RegisteredLP
    3import Lax263307.RationalProjection
    4import Lax263307.RationalCutBuffer
    5
    6/-!
    7---
    8title: The bounded projected round-or-cut search
    9type: theorem
    10---
    11The actual registered LP certificate decides whether to reject, separate
    12by a projection cut, or call the computed near-relaxation oracle.
    13Both cut branches preserve the same explicit dyadic cube about every
    14scaled independent-set encoding. The bounded rounded ellipsoid loop
    15therefore returns an approximate independent set or a valid upper bound
    16strictly below the requested positive target.
    17
    18# Formalization notes
    19
    20The only recursive hypothesis concerns answers on balanced child parts.
    21The LP and flow functions are fixed for the class and have the registered
    22RAM polynomial-time guarantees. The surrounding computable search still
    23needs its own finite RAM implementation and time bound.
    24-/
    25
    26namespace Lax263307.ProjectedOracle
    27
    28open LinearRelaxation AlgorithmParameters
    29
    30def tolerance (a K B n D : ℕ) : ℚ := momentFloor a K B n D / (32 * (n : ℚ)^2 * (D : ℚ)^2)
    31
    32def raw {N : ℕ} (center : Fin N → ℚ) : Fin N → ℚ := fun i => 4 * (N : ℚ) * center i
    33
    34def run {n : ℕ} (lp flow : List ℕ → List ℕ) (a K B D : ℕ)
    35 (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (k : ℕ)
    36 (child : Finset (Fin n) → ℕ → Option (Finset (Fin n)))
    37 (center : MomentLP.Index n (level a K B n D) → ℚ) :
    38 RoundedOracleSearch.Reply (MomentLP.dimension n (level a K B n D)) (Finset (Fin n)) :=
    39 let P := MomentLP.program G k (level a K B n D)
    40 match RationalProjection.classify P (tolerance a K B n D)
    41 (RegisteredLP.certificate lp (DistanceProjection.distanceProgram P (raw center))) with
    42 | .reject => .reject
    43 | .far normal _ => .cut (RationalCutBuffer.integerNormal normal)
    44 | .near y =>
    45 match NearOracle.run flow a K B D G k (MomentLP.decode y) child with
    46 | .reject => .reject
    47 | .found I => .found I
    48 | .cut A C u => .cut (RationalCutBuffer.integerNormal
    49 (RoundedOracleSearch.rationalNormal (MomentLP.encode (ComponentCutEncoding.coefficient A C u))))
    50
    51def Good {n : ℕ} (G : SimpleGraph (Fin n)) (k h D : ℕ) (I : Finset (Fin n)) : Prop :=
    52 G.IsIndepSet (I : Set (Fin n)) ∧ (1 - 4 * (1 / (D : ℝ))) ^ (h+1) * (k : ℝ) ≤ I.card
    53
    54def Correct {n : ℕ} (G : SimpleGraph (Fin n)) (k h a K B D : ℕ)
    55 (center : MomentLP.Index n (level a K B n D) → ℚ) :
    56 RoundedOracleSearch.Reply (MomentLP.dimension n (level a K B n D)) (Finset (Fin n)) → Prop
    57 | .found I => Good G k h D I
    58 | .reject => independentSetHull G k (level a K B n D) = ∅
    59 | .cut normal => (∃ i, normal i ≠ 0) ∧
    60 ∀ z ∈ independentSetHull G k (level a K B n D),
    61 ∀ e : MomentLP.Index n (level a K B n D) → ℝ,
    62 (∀ i, |e i| ≤ ((2 : ℝ) ^ precision a K B n D)⁻¹) →
    63 (fun i => (normal i : ℝ)) ⬝ᵥ
    64 (BufferedEllipsoid.scale (MomentLP.encode z) + e - (fun i => (center i : ℝ))) ≤ 0
    65
    66def search {n : ℕ} (lp flow : List ℕ → List ℕ) (a K B D : ℕ)
    67 (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (k : ℕ)
    68 (child : Finset (Fin n) → ℕ → Option (Finset (Fin n))) : Option (Finset (Fin n)) :=
    69 RoundedOracleSearch.search (fun _ center => run lp flow a K B D G k child center)
    70 (precision a K B n D)
    71
    72def SearchCorrect {n : ℕ} (G : SimpleGraph (Fin n)) (k h D : ℕ) : Option (Finset (Fin n)) → Prop
    73 | some I => Good G k h D I
    74 | none => IsIndependenceBound G Finset.univ (k-1)
    75
    76open GraphClasses PowerBagBounds
    77
    78axiom exists_search (C : GraphClass) (hereditary : IsHereditary C)
    79 (a A : ℕ) (ha : 0 < a) (hA : 0 < A) (class_bound : HasPowerBagBound C a A) :
    80 ∃ (lp flow : List ℕ → List ℕ) (K B : ℕ),
    81 Lax759944.RamPolytime.RamPolytime lp ∧ Lax759944.RamPolytime.RamPolytime flow ∧
    82 0 < K ∧ 0 < B ∧ ∀ (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj],
    83 G ∈ C n → 0 < n → ∀ (D k h : ℕ), 4 ≤ D → cutoff a K B n D < k →
    84 ∀ (child : Finset (Fin n) → ℕ → Option (Finset (Fin n))),
    85 Lax263307.NearOracle.ChildCorrect G D h child →
    86 SearchCorrect G k h D (search lp flow a K B D G k child)
    87
    88end Lax263307.ProjectedOracle
    89
    Show Proof
    Formalization notes

    The only recursive hypothesis concerns answers on balanced child parts. The LP and flow functions are fixed for the class and have the registered RAM polynomial-time guarantees. The surrounding computable search still needs its own finite RAM implementation and time bound.

    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…