
A
Formal
Proof
of
the
MaxFlow
MinCut
Theorem
for
Countable
Networks
Title: 
A Formal Proof of the MaxFlow MinCut Theorem for Countable Networks 
Author:

Andreas Lochbihler

Submission date: 
20160509 
Abstract: 
This article formalises a proof of the maximumflow minimalcut
theorem for networks with countably many edges. A network is a
directed graph with nonnegative realvalued edge labels and two
dedicated vertices, the source and the sink. A flow in a network
assigns nonnegative 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 MaxFlow MinCut 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. 
Change history: 
[20170906]:
derive characterisation for the lifting operation on discrete distributions from finite version of the maxflow mincut theorem
(revision a7a198f5bab0)
[20201219]:
simpler proof of linkability for bounded unhindered bipartite webs, leading to a simpler proof for networks with bounded outcapacities
(revision 93ca33f4d915)
[20210813]:
generalize the derivation of the characterisation for the relator of discrete probability distributions to work for the bounded and unbounded MFMC theorem
(revision 3c85bb52bbe6)

BibTeX: 
@article{MFMC_CountableAFP,
author = {Andreas Lochbihler},
title = {A Formal Proof of the MaxFlow MinCut Theorem for Countable Networks},
journal = {Archive of Formal Proofs},
month = may,
year = 2016,
note = {\url{https://isaafp.org/entries/MFMC_Countable.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
EdmondsKarp_Maxflow 
Used by: 
Probabilistic_While 
Status: [ok] 
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.

