Reservoir

Construction of a Flow Equivalent Forest in Lean 4

Setup

1. Install elan.
2. Run lake exe cache get to not compile mathlib4 yourself.
3. Run lake build to check the project.

Theorem

For an undirected flow network , we define its flow matrix to be the matrix such that for all vertices , , the value is the max flow in from to (and is undefined along the diagonal).

For all , it holds that

In particular, given a matrix with the conditions of the right side, we can construct an undirected network with flow matrix whose underlying graph of all non-zero capacity edges is acyclic. This implies that for any undirected flow network, there is a flow network based on a forest that has the same maximum flow between any two vertices.

The main result of our project is the construction of the acyclic network for a given matrix, see FlowEquivalentForest/Flow/Matrix.lean.

Bibliography

• Gomory, Ralph E., and Tien Chung Hu. "Multi-terminal network flows." Journal of the Society for Industrial and Applied Mathematics 9.4 (1961): 551-570.