Lax Lean Archive

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

Computed rounding oracle near the moment relaxation

Lax263307.NearOracle · concepts/Lax263307/NearOracle.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 algorithm searches for a heavy conditioning set, computes separators using the registered flow-cut solver, and queries the resulting parts. Its actual output is either an independent set or a valid component cut with a uniform gap and a bounded coefficient sum.

    Concept map
    83 concepts; 4 descendants hidden
    100%
    Certificates of infeasibilityLinear programs and their dualsExact 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 lightseparatorEdge-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 decompositionbagsExact rational search for a conditioning setDepth and approximation loss of balancedrecursionCombining recursive answers in round-or-cutCumulative 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.ComputedSeparators
    2import Lax263307.ComputedRounding
    3import Lax263307.HeavyRationalConditioning
    4import Lax263307.AlgorithmParameters
    5
    6/-!
    7---
    8title: Computed rounding oracle near the moment relaxation
    9type: theorem
    10---
    11The algorithm searches for a heavy conditioning set, computes separators
    12using the registered flow-cut solver, and queries the resulting parts.
    13Its actual output is either an independent set or a valid component cut
    14with a uniform gap and a bounded coefficient sum.
    15
    16# Formalization notes
    17
    18The child-query hypothesis is the induction hypothesis for the recursive
    19algorithm. All selections in the oracle are computable. Its implementation
    20and execution bounds in the registered RAM model are separate obligations.
    21-/
    22
    23namespace Lax263307.NearOracle
    24
    25open scoped NNRat
    26open LinearRelaxation RationalConditioning
    27
    28def costs {n r : ℕ} (y : RationalVector n r) (A : Finset (Fin n)) (v : Fin n) : ℚ≥0 :=
    29 ⟨max 0 (rationalValue y (insert v A) / rationalValue y A), le_max_left _ _⟩
    30
    31def order (q : ℕ) : List (Option (Fin q)) := none :: (List.finRange q).map some
    32
    33inductive Result (n : ℕ)
    34 | found (vertices : Finset (Fin n))
    35 | cut (conditioning vertices : Finset (Fin n)) (bound : ℕ)
    36 | reject
    37
    38def run {n : ℕ} (flow : List ℕ → List ℕ) (a K B D : ℕ)
    39 (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (k : ℕ)
    40 (y : RationalVector n (AlgorithmParameters.level a K B n D))
    41 (child : Finset (Fin n) → ℕ → Option (Finset (Fin n))) : Result n :=
    42 let p := AlgorithmParameters.sparsity a K B n D
    43 match HeavyRationalConditioning.findHeavyConditioning G k p y with
    44 | none => .reject
    45 | some A =>
    46 let x := costs y A
    47 let cs := ComputedSeparators.cuts
    48 (ComputedSeparators.step flow G x B (AlgorithmParameters.load B n D) k) n Finset.univ
    49 let parts := ComputedSeparators.pieces cs
    50 let c : Option (Fin cs.length) → ℚ := fun i => ∑ v ∈ parts i, (x v : ℚ)
    51 match ComputedRounding.collect (order cs.length) parts (1 / D) k c
    52 (fun i t => child (parts i) t) with
    53 | .found I => .found I
    54 | .cut C u => .cut A C u
    55
    56def ChildCorrect {n : ℕ} (G : SimpleGraph (Fin n)) (D h : ℕ)
    57 (child : Finset (Fin n) → ℕ → Option (Finset (Fin n))) : Prop :=
    58 ∀ C : Finset (Fin n), 3 * C.card ≤ 2 * n → ∀ t : ℕ,
    59 match child C t with
    60 | some I => I ⊆ C ∧ G.IsIndepSet (I : Set (Fin n)) ∧
    61 (1 - 4 * (1 / (D : ℝ))) ^ h * (t : ℝ) ≤ I.card
    62 | none => IsIndependenceBound G C (t - 1)
    63
    64def Correct {n r : ℕ} (G : SimpleGraph (Fin n)) (k h D : ℕ) (η : ℝ)
    65 (x : MomentVector n r) : Result n → Prop
    66 | .found I => G.IsIndepSet (I : Set (Fin n)) ∧
    67 (1 - 4 * (1 / (D : ℝ))) ^ (h + 1) * (k : ℝ) ≤ I.card
    68 | .cut A C u => A.card ≤ r ∧ u ≤ n ∧ IsIndependenceBound G C u ∧
    69 (∀ z ∈ independentSetHull G k r,
    70 ComponentCutEncoding.evaluate (ComponentCutEncoding.coefficient A C u) z ≤ 0) ∧
    71 η * (1 / (D : ℝ)) ^ 2 / (16 * n) ≤
    72 ComponentCutEncoding.evaluate (ComponentCutEncoding.coefficient A C u) x ∧
    73 (∑ T : Coordinate n r, |(ComponentCutEncoding.coefficient A C u T : ℝ)|) ≤ 2 * n
    74 | .reject => False
    75
    76open GraphClasses PowerBagBounds AlgorithmParameters
    77
    78axiom exists_oracle (C : GraphClass) (hereditary : IsHereditary C)
    79 (a A : ℕ) (ha : 0 < a) (hA : 0 < A) (class_bound : HasPowerBagBound C a A) :
    80 ∃ (flow : List ℕ → List ℕ) (K B : ℕ), Lax759944.RamPolytime.RamPolytime flow ∧
    81 0 < K ∧ 0 < B ∧ ∀ (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj],
    82 G ∈ C n → 0 < n → ∀ (D k h : ℕ), 4 ≤ D → cutoff a K B n D < k →
    83 ∀ (y : RationalVector n (level a K B n D)),
    84 IsFeasible G k (level a K B n D) (realVector y) →
    85 ∀ (x : MomentVector n (level a K B n D)),
    86 (∀ T, |x T - realVector y T| ≤ (momentFloor a K B n D : ℝ) *
    87 (1 / (D : ℝ)) ^ 2 / (32 * (n : ℝ) ^ 2)) →
    88 ∀ (child : Finset (Fin n) → ℕ → Option (Finset (Fin n))), ChildCorrect G D h child →
    89 Correct G k h D (momentFloor a K B n D) x (run flow a K B D G k y child)
    90
    91end Lax263307.NearOracle
    92
    Show Proof
    Formalization notes

    The child-query hypothesis is the induction hypothesis for the recursive algorithm. All selections in the oracle are computable. Its implementation and execution bounds in the registered RAM model are separate obligations.

    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…