The exact 9/10 cut bound #
Every source-sink cut in Dross's auxiliary network has capacity at least the network demand. This is the cut-side half of the max-flow construction.
theorem
LeanPool.DrossFractionalTriangleDecomposition.cut_ge_M_exact
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(h : 9 * Fintype.card V ≤ 10 * G.minDegree)
(wΔ : ℝ)
(hwΔ : 0 < wΔ)
(hbal : ∑ e ∈ G.edgeFinset, (↑(triThrough G e) * wΔ - 1) = 0)
(δ : ℝ)
(hδ0 : 0 < δ)
(hδ1 : δ ≤ 1 / 10)
(hn20 : 20 ≤ Fintype.card V)
(hmd2 : 2 ≤ G.minDegree)
(hδ_eq : ↑(Fintype.card V) - ↑G.minDegree = δ * ↑(Fintype.card V))
(hmbound :
2 * ↑G.edgeFinset.card ≤ (1 - δ + 2 * δ ^ 2) * ↑(Fintype.card V) ^ 2 + 4 + ↑(Fintype.card V) - 6 * δ * ↑(Fintype.card V))
(C : Contrib.MaxFlowMinCut.Cut (drossNet G wΔ))
: