### Abstract

This article formalises a proof of the maximum-flow minimal-cut theorem for networks with countably many edges. A network is a directed graph with non-negative real-valued edge labels and two dedicated vertices, the source and the sink. A flow in a network assigns non-negative real numbers to the edges such that for all vertices except for the source and the sink, the sum of values on incoming edges equals the sum of values on outgoing edges. A cut is a subset of the vertices which contains the source, but not the sink. Our theorem states that in every network, there is a flow and a cut such that the flow saturates all the edges going out of the cut and is zero on all the incoming edges. The proof is based on the paper The Max-Flow Min-Cut theorem for countable networks by Aharoni et al. Additionally, we prove a characterisation of the lifting operation for relations on discrete probability distributions, which leads to a concise proof of its distributivity over relation composition.

### License

BSD License

### History

August 13, 2021
  generalize the derivation of the characterisation for the relator of discrete probability distributions to work for the bounded and unbounded MFMC theorem (revision 3c85bb52bbe6)
December 19, 2020
  simpler proof of linkability for bounded unhindered bipartite webs, leading to a simpler proof for networks with bounded out-capacities (revision 93ca33f4d915)
September 6, 2017
  derive characterisation for the lifting operation on discrete distributions from finite version of the max-flow min-cut theorem (revision a7a198f5bab0)

### Topics

- Mathematics/Graph theory

### Session MFMC_Countable

- MFMC_Misc
- MFMC_Finite
- Matrix_For_Marginals
- MFMC_Network
- MFMC_Web
- MFMC_Reduction
- MFMC_Bounded
- MFMC_Flow_Attainability
- MFMC_Unbounded
- Max_Flow_Min_Cut_Countable
- Rel_PMF_Characterisation
- Rel_PMF_Characterisation_MFMC

### Depends on

- Formalizing the Edmonds-Karp Algorithm

### Used by

- Probabilistic while loop

### Auto-related entries

- Zeckendorf’s Theorem
- Randomised Binary Search Trees
- Sturm’s Theorem

## Cite

×

MFMC_Countable-AFP

    @article{MFMC_Countable-AFP,
      author  = {Andreas Lochbihler},
      title   = {A Formal Proof of the Max-Flow Min-Cut Theorem for Countable Networks},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/MFMC_Countable.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- May 9, 2016 : Isabelle2016