Lax Lean Archive

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

A fixed RAM program constructs the rounded blow-up

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

    One finite RAM program reads the original weighted graph, clips negative weights, computes rounded copy counts, and constructs the adjacency matrix of the canonically numbered independent blow-up. Its output starts with the blow-up order and then gives the adjacency matrix in row-major order.

    Concept map
    105 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 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 programA fixed RAM program constructs therounded blow-upComputed 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.WeightedAlgorithm
    2import Lax808846.Ram
    3
    4/-!
    5---
    6title: A fixed RAM program constructs the rounded blow-up
    7type: theorem
    8---
    9One finite RAM program reads the original weighted graph, clips negative
    10weights, computes rounded copy counts, and constructs the adjacency matrix
    11of the canonically numbered independent blow-up. Its output starts with the
    12blow-up order and then gives the adjacency matrix in row-major order.
    13
    14# Formalization notes
    15
    16The execution proof includes the actual unprefixed input reader, maximum
    17scan, natural-number quotient for copy counts, owner-array construction,
    18and every adjacency lookup. Copy owners agree exactly with the computable
    19finite-sigma labeling used by the weighted algorithm. Time and sufficient
    20word width are quadratic in the original order, blow-up order, and input
    21rational height. This is the preprocessing program; the complete recursive
    22RAM solver and its global quasipolynomial bound remain separate obligations.
    23-/
    24
    25namespace Lax263307.NativeBlowUp
    26
    27open WeightRounding WeightedIndependentSet WeightedAlgorithm
    28
    29def encode {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] : List ℕ :=
    30 n :: (List.ofFn fun u => List.ofFn fun v => if G.Adj u v then 1 else 0).flatten
    31
    32axiom exists_program : ∃ p : Lax808846.Ram.Program, ∃ c : ℕ, 0<c ∧
    33 ∀ (n h : ℕ), 1≤h → ∀ (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    34 (w : Fin n → ℚ) (ε : ℚ), 0<ε →
    35 (∀ i,(w i).num.natAbs≤2^h ∧ (w i).den≤2^h) →
    36 ε.num.natAbs≤2^h → ε.den≤2^h →
    37 let cs := copies (fun v => max (w v) 0) ε
    38 let N := ∑ v,cs v
    39 ∀ width : ℕ,c*(n+N+h+1)^2≤width →
    40 ∃ t≤c*(n+N+h+1)^2,Lax808846.Ram.RunsTo width p (encodeInput G w ε)
    41 (encode (numbered G cs)) t
    42
    43end Lax263307.NativeBlowUp
    44
    Show Proof
    Formalization notes

    The execution proof includes the actual unprefixed input reader, maximum scan, natural-number quotient for copy counts, owner-array construction, and every adjacency lookup. Copy owners agree exactly with the computable finite-sigma labeling used by the weighted algorithm. Time and sufficient word width are quadratic in the original order, blow-up order, and input rational height. This is the preprocessing program; the complete recursive RAM solver and its global quasipolynomial bound remain separate obligations.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…