LeanPool.GoemansFlow.Counterexample

Path completeness. For each commodity i, the arc-lists forming a walk from the source s to the terminal t_i are exactly the two listed paths. This is derived from the arc list — via the enumeration walksFrom together with the topological rank bounding every walk by 4 arcs — and not assumed.

source

theorem GoemansFlow.routing_paths_nodup (p : Fin 3 → List Arc) (h : IsRouting p) (i : Fin 3) :

(p i).Nodup

Every routing in the counterexample uses arc-simple paths.

source

theorem GoemansFlow.routing_load_eq_sum (p : Fin 3 → List Arc) (h : IsRouting p) (a : Arc) :

unsplittableLoad demand p a = ∑ i : Fin 3, if a ∈ p i then demand i else 0

The traversal-counting load agrees with upstream's membership formula on every routing.

source

Conversely, all six really are walks.

source

def GoemansFlow.vertexSequence (x : Vertex) (l : List Arc) :

List Vertex

The vertex sequence visited by a walk.

Equations

GoemansFlow.vertexSequence x l = x :: List.map GoemansFlow.head l

Instances For

source

Each of the six s-t_i walks is a simple path (no repeated vertex), so restricting Conjecture 1.3 to simple paths would not help.

source

def GoemansFlow.loadThree (q0 q1 q2 : List Arc) (a : Arc) :

ℤ

The load written as a function of the three chosen paths.

Equations

GoemansFlow.loadThree q0 q1 q2 a = List.count a q0 • GoemansFlow.demand 0 + List.count a q1 • GoemansFlow.demand 1 + List.count a q2 • GoemansFlow.demand 2

Instances For

source

def GoemansFlow.routingCostThree (q0 q1 q2 : List Arc) :

ℤ

Routing cost expressed in terms of the three chosen paths.

Equations

GoemansFlow.routingCostThree q0 q1 q2 = ∑ a : GoemansFlow.Arc, GoemansFlow.arcCost a * GoemansFlow.loadThree q0 q1 q2 a

Instances For

source

theorem GoemansFlow.unsplittableLoad_eq (p : Fin 3 → List Arc) (a : Arc) :

unsplittableLoad demand p a = loadThree (p 0) (p 1) (p 2) a

source

theorem GoemansFlow.routingCost_eq (p : Fin 3 → List Arc) :

routingCost p = routingCostThree (p 0) (p 1) (p 2)

source

theorem GoemansFlow.enum_check (q0 : List Arc) :

q0 ∈ [expensivePathOne , zeroCostPathOne ] → ∀ q1 ∈ [expensivePathTwo , zeroCostPathTwo ], ∀ q2 ∈ [expensivePathThree , zeroCostPathThree ], (∀ (a : Arc), loadThree q0 q1 q2 a ≤ fractionalFlow a + maximumDemand) → 60 ≤ routingCostThree q0 q1 q2

The eight-case kernel check. Over the eight combinations of path choices, every capacity-good one costs at least 60.

source

theorem GoemansFlow.min_cost_capacity_good (p : Fin 3 → List Arc) (hr : IsRouting p) (hc : CapacityGood p) :

60 ≤ routingCost p

Layer A (main). Every unsplittable routing of the three demands along arbitrary walks out of s whose arc loads stay within x(a) + d_max costs at least 60 — strictly more than the fractional cost 58.

source

def GoemansFlow.allExpensiveRoute :

Fin 3 → List Arc

Route every commodity on its "expensive" path.

Equations

GoemansFlow.allExpensiveRoute = GoemansFlow.expensivePath

Instances For

source

def GoemansFlow.optimalRoute :

Fin 3 → List Arc

Route t1, t2 expensively and t3 on the zero-cost path: cost exactly 60.

Equations

GoemansFlow.optimalRoute i = if i = 0 then GoemansFlow.expensivePathOne else if i = 1 then GoemansFlow.expensivePathTwo else GoemansFlow.zeroCostPathThree

Instances For

source

theorem GoemansFlow.exists_capacity_good :

IsRouting allExpensiveRoute ∧ CapacityGood allExpensiveRoute

source

theorem GoemansFlow.cost_sixty_attained :

IsRouting optimalRoute ∧ CapacityGood optimalRoute ∧ routingCost optimalRoute = 60

source

theorem GoemansFlow.dgg_theorem_holds_here :

∃ (p : Fin 3 → List Arc), IsRouting p ∧ ∀ (a : Arc), unsplittableLoad demand p a ≤ fractionalFlow a + maximumDemand

Positive control. The instance does satisfy the conclusion of DGG Theorem 1.2 (the capacity clause (i) on its own): an unsplittable routing with flow_P(a) ≤ x(a) + d_max for every arc a exists. So the refutation isolates clause (ii), the cost clause — it is not an artifact of an unsatisfiable capacity requirement.

source

def GoemansFlow.allZeroCostRoute :

Fin 3 → List Arc

Route every commodity on its zero-cost path.

Equations

GoemansFlow.allZeroCostRoute = GoemansFlow.zeroCostPath

Instances For

source

theorem GoemansFlow.cost_clause_alone_satisfiable :

IsRouting allZeroCostRoute ∧ routingCost allZeroCostRoute ≤ ∑ a : Arc, arcCost a * fractionalFlow a

Positive control for the other clause. Clause (ii) of Conjecture 1.3 -- the cost clause -- is also satisfiable on its own here: the all-Z routing costs 0 ≤ 58 = c^T x. So neither clause is individually unsatisfiable at this instance; only their conjunction fails, which is what makes the instance a counterexample to Conjecture 1.3 rather than to either half of it.

source

theorem GoemansFlow.two_dmax_conclusion_holds_here :

IsRouting allZeroCostRoute ∧ (∀ (a : Arc), fractionalFlow a - 2 * maximumDemand ≤ unsplittableLoad demand allZeroCostRoute a ∧ unsplittableLoad demand allZeroCostRoute a ≤ fractionalFlow a + 2 * maximumDemand) ∧ routingCost allZeroCostRoute ≤ ∑ a : Arc, arcCost a * fractionalFlow a

No conflict with the primary source's planar theorems. Planarity is not formalized here. The instance satisfies the numerical conclusion of the planar result in arXiv:2308.02651. Theorem 1.8 of that paper grants a two-sided violation of 2·d_max together with the cost bound, and its conclusion is satisfied here: the all-Z routing keeps every arc load within 2·d_max = 30 of x on both sides and costs 0 ≤ 58. The counterexample therefore refutes the d_max grade only, exactly as Conjecture 1.3 states it.

source

theorem GoemansFlow.optimum_is_sixty :

(∀ (p : Fin 3 → List Arc), IsRouting p → CapacityGood p → 60 ≤ routingCost p) ∧ ∃ (p : Fin 3 → List Arc), IsRouting p ∧ CapacityGood p ∧ routingCost p = 60

60 is exactly the optimum: it is a lower bound and it is attained.

source

def GoemansFlow.GoemansCostConjecture (R : Type) [CommRing R] [LinearOrder R] :

Prop

Goemans' cost conjecture (Dinitz–Garg–Goemans / SSUF), Conjecture 1.3 of arXiv:2308.02651, stated over a linearly ordered commutative ring R.

Read: for every finite digraph (W, E) with arc endpoints tail, head, every source src, every finite family of commodities K with distinct terminals term k ≠ src and positive demands d k, every dmax equal to the maximum demand, every nonnegative cost vector c and every nonnegative feasible single-source flow x routing the demands, there is an unsplittable routing P (one walk per commodity) with

flow_P(a) ≤ x(a) + dmax for every arc a, and
c^T flow_P ≤ c^T x.

This form ranges over arbitrary directed graphs and omits capacities. The refutation of GoemansCostConjectureFull also supplies a simple, loopless, acyclic instance with explicit capacities, avoiding dependence on these differences from the source.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem GoemansFlow.GoemansCostConjectureFull_of_GoemansCostConjecture (R : Type) [CommRing R] [LinearOrder R] (h : GoemansCostConjecture R) :

GoemansCostConjectureFull R

The Full form is the weaker Prop. It is GoemansCostConjecture with four hypotheses added (simple, loopless, acyclic, x ≤ u), so the bare conjecture implies it. Hence ¬ GoemansCostConjectureFull is the stronger statement, and it implies ¬ GoemansCostConjecture.

source

theorem GoemansFlow.GoemansCostConjecture_int_of {R : Type} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (h : GoemansCostConjecture R) :

GoemansCostConjecture ℤ

If the conjecture held over R, it would hold over ℤ (an integral instance is an R-instance, and the conclusion pulls back along the order embedding ℤ ↪ R).

source

theorem GoemansFlow.GoemansCostConjectureFull_int_of {R : Type} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (h : GoemansCostConjectureFull R) :

GoemansCostConjectureFull ℤ

The same transfer for the literature-faithful form: if the Full conjecture held over R, it would hold over ℤ. The four extra hypotheses (simple, loopless, acyclic, x ≤ u) transfer verbatim -- the first three do not mention the ring at all, and x ≤ u pushes forward along the order embedding ℤ ↪ R.

source

theorem GoemansFlow.not_GoemansCostConjectureFull_int :

¬GoemansCostConjectureFull ℤ

Layer B (main), literature-faithful form, over ℤ. The counterexample instance discharges every hypothesis of GoemansCostConjectureFull: it is simple (arcs_simple), loopless (no_self_loops), acyclic (⟨rank, rank_arc⟩), and takes u := x (the worst case the primary source identifies), so x ≤ u holds by reflexivity.

source

theorem GoemansFlow.not_GoemansCostConjectureFull (R : Type) [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] :

¬GoemansCostConjectureFull R

Layer B (main), literature-faithful form, general coefficient ring. Goemans' cost conjecture -- capacities restored, digraph simple, loopless and acyclic -- is false over every linearly ordered commutative ring.

source

theorem GoemansFlow.not_GoemansCostConjectureFull_rat :

¬GoemansCostConjectureFull ℚ

The literature-faithful form over ℚ, the setting of Conjecture 1.3.

source

theorem GoemansFlow.goemans_cost_conjecture_false :

¬GoemansCostConjectureFull ℚ

THE HEADLINE. Goemans' cost conjecture for single-source unsplittable flow (Conjecture 1.3 of arXiv:2308.02651, the cost version of the Dinitz–Garg–Goemans theorem) is false over ℚ, in the form that keeps every piece of the literature's data: arc capacities u with x ≤ u, and a simple, loopless, acyclic digraph.

dgg_cost_conjecture_false below is the same refutation for the bare form GoemansCostConjecture and is kept as the searchable alias.

source

theorem GoemansFlow.goemans_cost_conjecture_false_real :

¬GoemansCostConjectureFull ℝ

The headline over the reals.

source

theorem GoemansFlow.not_GoemansCostConjecture_int :

¬GoemansCostConjecture ℤ

Layer B, bare form. Goemans' cost conjecture is false over ℤ.

source

theorem GoemansFlow.not_GoemansCostConjecture (R : Type) [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] :

¬GoemansCostConjecture R

Layer B, bare form, general coefficient ring. Goemans' cost conjecture is false over every linearly ordered commutative ring — in particular over ℚ, the setting of Conjecture 1.3 of arXiv:2308.02651, and over ℝ.

source

theorem GoemansFlow.dgg_cost_conjecture_false :

¬GoemansCostConjecture ℚ

The bare form over ℚ; the searchable alias of the headline goemans_cost_conjecture_false. (It also follows from the headline without re-running the instance, via GoemansCostConjectureFull_of_GoemansCostConjecture — see dgg_cost_conjecture_false_of_headline — since the Full form is the weaker Prop.)

source

theorem GoemansFlow.dgg_cost_conjecture_false_real :

¬GoemansCostConjecture ℝ

The same over the reals.

source

theorem GoemansFlow.dgg_cost_conjecture_false_of_headline :

¬GoemansCostConjecture ℚ

The headline implies the bare-form refutation, with no second appeal to the instance: the Full form is the weaker Prop, so refuting it refutes the bare one.

Documentation

LeanPool.GoemansFlow.Counterexample

A counterexample to Goemans' cost conjecture #

1. The counterexample instance #

2. Loads and costs #

3. Path completeness: the digraph has exactly six s-t_i walks #

4. Layer A: the eight-case check and the cost lower bound #

Non-vacuity and tightness #

5. Layer B: the conjecture, and its refutation #