EdmondsKarpBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The shortest-augmentation bound

Charge an augmentation to a critical directed arc and its previous tail label. A repeated directed arc has strictly larger label, so the charge is injective into n×n×n.

theorem OAI.ContingencyTables.EdmondsKarpBound.shortest_trace_bound line 18
theorem OAI.ContingencyTables.EdmondsKarpBound.edmondsKarp1972Theorem1 line 45
Source documentation
Edmonds and Karp (1972), Theorem 1, in the exact integral-skew-flow specialization for the sampling and counting algorithms.
```
theorem edmondsKarp1972Theorem1 : EdmondsKarp1972Theorem1 := by
…
```