Imports

import CLRSLean.FourthEdition.Chapter_24.Section_24_4_Push_Relabel

24.5. Relabel-to-Front

This section completes the push-relabel maximum-flow analysis begun in CLRSLean.FourthEdition.Chapter_24.Section_24_4_Push_Relabel. There we established the preflow model, the height function, and the two local operations CLRS.Chapter26.push and CLRS.Chapter26.relabel, together with the correctness certificate CLRS.Chapter26.maximal_of_no_overflow. Here we count the operations.

The generic push-relabel algorithm repeatedly picks an overflowing vertex and applies a push or a relabel. A run of the algorithm is a sequence of basic operations (BasicOp), each either a relabel of an overflowing vertex or a push from an overflowing vertex along an admissible edge. We count relabels, saturating pushes, and nonsaturating pushes over a Run, and prove the three CLRS counting bounds:

Main results:

BasicOp, Run: a single basic operation and a length-n run of the generic algorithm.
Run.height_mono: heights are nondecreasing across a run.
Run.relabel_count_bound: at most 2|V|² relabel operations total.
Run.saturating_push_count_bound: at most O(|V|·|E|) saturating pushes.
Run.nonsaturating_push_count_bound: at most O(|V|²(|V|+|E|)) nonsaturating pushes, via the potential Φ = Σ_{overflowing u} h(u).
Run.generic_step_count_bound: the combined O(V²E) bound on the number of basic operations.

These bounds hold for any run of the generic algorithm, so they apply to the relabel-to-front schedule in particular. The relabel-to-front schedule is stronger: its DISCHARGE procedure walks a per-vertex neighbor list and, on relabeling a vertex, moves it to the front of the list L. That per-vertex list discipline gives the sharper O(V³) bound:

RelabelToFrontRun: a run satisfying the discharge discipline (between two relabel operations, no vertex is the source of more than one nonsaturating push).
RelabelToFrontRun.nonsaturating_push_count_bound: at most |V|·(relabels + 1) nonsaturating pushes, i.e. O(V³).
RelabelToFrontRun.step_count_bound_V3: the relabel-to-front algorithm performs at most 9|V|³ basic operations.

Notation conventions used in this section:

φ : a preflow on the network G
h : a height function V → ℕ
V (as Fintype.card V) : the number of vertices
E (as numEdges G) : the number of directed positive-capacity edges

              set_option autoImplicit truenamespace CLRSnamespace Chapter26universe uopen Finset Classicalopen scoped BigOperatorsvariable {V : Type u} [Fintype V] [DecidableEq V] {G : FlowNetwork V}

The number of edges

The set of directed edges (u,v) with positive capacity.

noncomputable def edgeSet (G : FlowNetwork V) : Finset (V × V) :=
  (Finset.univ : Finset (V × V)).filter (fun e => 0 < G.c e.1 e.2)

The number of directed edges (positive-capacity pairs).

noncomputable def numEdges (G : FlowNetwork V) : ℕ := (edgeSet G).card

Basic operations and runs

A single basic operation of the generic push-relabel algorithm: either a relabel of an overflowing vertex u, or a push from an overflowing u along an admissible residual edge (u,v). The preflow φ and height h are the state before the operation.

inductive BasicOp (V : Type u) [Fintype V] [DecidableEq V] (G : FlowNetwork V) : Type u where
  | relabel (φ : Preflow V G) (h : V → ℕ) (u : V) (hoverflow : φ.isOverflowing u)
      (hres : ∃ v : V, φ.residualEdge u v)
      (hpre : ∀ v, φ.residualEdge u v → h u ≤ h v) : BasicOp V G
  | push (φ : Preflow V G) (h : V → ℕ) (u v : V) (hoverflow : φ.isOverflowing u)
      (hres : φ.residualEdge u v) (hadm : h u = h v + 1) : BasicOp V G

namespace BasicOp

The preflow before the operation.

def beforeφ : BasicOp V G → Preflow V G
  | .relabel φ _ _ _ _ _ => φ
  | .push φ _ _ _ _ _ _ => φ

The height function before the operation.

def beforeh : BasicOp V G → V → ℕ
  | .relabel _ h _ _ _ _ => h
  | .push _ h _ _ _ _ _ => h

The preflow after the operation.

noncomputable def resultφ : BasicOp V G → Preflow V G
  | .relabel φ _ _ _ _ _ => φ
  | .push φ _ u v hoverflow hres _ => Chapter26.push φ u v hoverflow.1 hres

The height function after the operation.

noncomputable def resulth : BasicOp V G → V → ℕ
  | .relabel φ h u _ hres _ => Chapter26.relabel φ h u hres
  | .push _ h _ _ _ _ _ => h

Whether the operation is a relabel.

def isRelabel : BasicOp V G → Bool
  | .relabel .. => true
  | .push .. => false

Whether the operation is a relabel of the specific vertex u.

def relabelOf (u : V) : BasicOp V G → Bool
  | .relabel _ _ w _ _ _ => decide (w = u)
  | .push .. => false

Whether the operation is a push along the specific edge (u,v).

def pushOn (u v : V) : BasicOp V G → Bool
  | .push _ _ a b _ _ _ => decide (a = u ∧ b = v)
  | .relabel .. => false

Whether the operation is a saturating push (the residual capacity of the edge is exhausted, i.e. cf(u,v) ≤ e(u) so δ = cf(u,v)).

noncomputable def isSaturatingPush : BasicOp V G → Bool
  | .push φ _ u v _ _ _ => decide (φ.residualCapacity u v ≤ φ.excess u)
  | .relabel .. => false

Whether the operation is a nonsaturating push (the excess is exhausted, i.e. e(u) < cf(u,v) so δ = e(u)).

noncomputable def isNonsaturatingPush : BasicOp V G → Bool
  | .push φ _ u v _ _ _ => decide (φ.excess u < φ.residualCapacity u v)
  | .relabel .. => false

A saturating push along the specific edge (u,v).

noncomputable def saturatingPushOn (u v : V) : BasicOp V G → Bool
  | .push φ _ a b _ _ _ => decide (a = u ∧ b = v ∧ φ.residualCapacity a b ≤ φ.excess a)
  | .relabel .. => false

A single operation is exactly one of relabel, saturating push, or nonsaturating push.

lemma classification (o : BasicOp V G) :
    (if o.isRelabel then 1 else 0) + (if o.isSaturatingPush then 1 else 0) +
      (if o.isNonsaturatingPush then 1 else 0) = 1 := by
  cases o with
  | relabel φ h u ho hres hpre =>
      simp [isRelabel, isSaturatingPush, isNonsaturatingPush]
  | push φ h u v ho hres hadm =>
      by_cases hsat : φ.residualCapacity u v ≤ φ.excess u
      · simp [isRelabel, isSaturatingPush, isNonsaturatingPush, hsat]
      · have hlt : φ.excess u < φ.residualCapacity u v := lt_of_not_ge hsat
        simp [isRelabel, isSaturatingPush, isNonsaturatingPush, hsat, hlt]

Relabels are characterized by the vertex they relabel.


lemma sum_relabelOf_eq_isRelabel (o : BasicOp V G) :
    (∑ u : V, (if o.relabelOf u then 1 else 0 : ℕ)) = (if o.isRelabel then 1 else 0 : ℕ) := by
  cases o with
  | relabel φ h w ho hres hpre =>
      simp only [relabelOf, isRelabel]
      rw [Finset.sum_eq_single w]
      · simp
      · intro b _ hbw
        simp [hbw.symm]
      · intro hw
        simp at hw
  | push φ h u v ho hres hadm =>
      simp [relabelOf, isRelabel]

Saturating pushes are characterized by the edge they saturate.


lemma sum_saturatingPushOn_eq (o : BasicOp V G) :
    (∑ e : V × V, (if o.saturatingPushOn e.1 e.2 then 1 else 0 : ℕ)) =
      (if o.isSaturatingPush then 1 else 0 : ℕ) := by
  cases o with
  | relabel φ h u ho hres hpre =>
      simp [saturatingPushOn, isSaturatingPush]
  | push φ h u v ho hres hadm =>
      by_cases hsat : φ.residualCapacity u v ≤ φ.excess u
      · have hcard : ((Finset.univ.filter (fun e : V × V => u = e.1 ∧ v = e.2)).card) = 1 := by
          have hf : (Finset.univ.filter (fun e : V × V => u = e.1 ∧ v = e.2)) = {(u, v)} := by
            ext e
            simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_singleton]
            constructor
            · intro h
              exact Prod.ext h.1.symm h.2.symm
            · intro h
              cases h
              exact ⟨rfl, rfl⟩
          rw [hf]
          simp
        simp [saturatingPushOn, isSaturatingPush, hsat, Finset.sum_boole, hcard]
      · simp [saturatingPushOn, isSaturatingPush, hsat]

The height of any fixed vertex is nondecreasing across a single operation.

try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
lemma height_mono (o : BasicOp V G) (u : V) : o.beforeh u ≤ o.resulth u := by
  cases o with
  | relabel φ h w ho hres hpre =>
      by_cases hwu : w = u
      · subst u
        exact le_of_lt (relabel_height_increase φ h w hres hpre)
      · try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [beforeh, resulth, relabel_eq_of_ne φ h w hres (Ne.symm hwu)]
  | push φ h u v ho hres hadm =>
      simp [beforeh, resulth]

A relabel operation strictly increases the height of the relabeled vertex.


lemma height_increase_of_relabel (o : BasicOp V G) {u : V} (hrel : o.relabelOf u = true) :
    o.beforeh u < o.resulth u := by
  cases o with
  | relabel φ h w ho hres hpre =>
      have hwu : w = u := by
        simpa [relabelOf] using (of_decide_eq_true hrel)
      subst u
      exact relabel_height_increase φ h w hres hpre
  | push φ h u v ho hres hadm =>
      simp [relabelOf] at hrel

end BasicOp

A run of the generic push-relabel algorithm: a sequence of n basic operations with the associated preflows and height functions.

structure Run (V : Type u) [Fintype V] [DecidableEq V] (G : FlowNetwork V) (n : ℕ) where
  φ : ℕ → Preflow V G
  h : ℕ → V → ℕ
  hvalid : ∀ i, IsValidHeight (φ i) (h i)
  op : ∀ i, i < n → BasicOp V G
  hop_beforeφ : ∀ i (hi : i < n), (op i hi).beforeφ = φ i
  hop_beforeh : ∀ i (hi : i < n), (op i hi).beforeh = h i
  hop_resultφ : ∀ i (hi : i < n), (op i hi).resultφ = φ (i + 1)
  hop_resulth : ∀ i (hi : i < n), (op i hi).resulth = h (i + 1)

namespace Runopen BasicOp (relabelOf pushOn saturatingPushOn isRelabel isSaturatingPush isNonsaturatingPush)

The operation at a Fin n step.

def opFin (R : Run V G n) (i : Fin n) : BasicOp V G :=
  R.op i.1 (Fin.isLt i)

The number of relabel operations in a run.

noncomputable def numRelabels (R : Run V G n) : ℕ :=
  ∑ i : Fin n, (if (R.opFin i).isRelabel then 1 else 0)

The number of saturating push operations in a run.

noncomputable def numSaturatingPushes (R : Run V G n) : ℕ :=
  ∑ i : Fin n, (if (R.opFin i).isSaturatingPush then 1 else 0)

The number of nonsaturating push operations in a run.

noncomputable def numNonsaturatingPushes (R : Run V G n) : ℕ :=
  ∑ i : Fin n, (if (R.opFin i).isNonsaturatingPush then 1 else 0)

The number of relabel operations of a specific vertex u.

noncomputable def numRelabelsOf (R : Run V G n) (u : V) : ℕ :=
  ∑ i : Fin n, (if (R.opFin i).relabelOf u then 1 else 0)

The number of saturating pushes along a specific edge (u,v).

noncomputable def numSaturatingPushesOn (R : Run V G n) (u v : V) : ℕ :=
  ∑ i : Fin n, (if (R.opFin i).saturatingPushOn u v then 1 else 0)

Height monotonicity

The height of any fixed vertex is nondecreasing across a single step.


lemma height_mono_step (R : Run V G n) (i : Fin n) (u : V) :
    R.h i.1 u ≤ R.h (i.1 + 1) u := by
  have hb := BasicOp.height_mono (R.opFin i) u
  have hb' : (R.opFin i).beforeh u = R.h i.1 u := by
    exact congrFun (R.hop_beforeh i.1 (Fin.isLt i)) u
  have hr' : (R.opFin i).resulth u = R.h (i.1 + 1) u := by
    exact congrFun (R.hop_resulth i.1 (Fin.isLt i)) u
  rw [← hb', ← hr']
  exact hb

Heights are nondecreasing across a run: i ≤ j implies h i u ≤ h j u.


lemma height_mono (R : Run V G n) {i j : ℕ} (hij : i ≤ j) (hj : j ≤ n) (u : V) :
    R.h i u ≤ R.h j u := by
  obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le hij
  induction d with
  | zero => rfl
  | succ d ih =>
      have hle := ih
      have hstep : R.h (i + d) u ≤ R.h (i + (d + 1)) u := by
        have hi : i + d < n := by omega
        simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using
          height_mono_step R ⟨i + d, hi⟩ u
      omega

Relabel count bound

The height of u strictly increases between two distinct relabel steps of u.


lemma height_strict_between_relabels_of (R : Run V G n) {i j : Fin n} (hij : i.1 < j.1)
    {u : V} (hri : (R.opFin i).relabelOf u = true) (Variable name `hrj` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hrj : (R.opFin j).relabelOf u = true) :
    R.h i.1 u < R.h j.1 u := by
  have hinc : R.h i.1 u < R.h (i.1 + 1) u := by
    have hb := BasicOp.height_increase_of_relabel (R.opFin i) hri
    rw [show R.opFin i = R.op i.1 (Fin.isLt i) from rfl] at hb
    rw [R.hop_beforeh i.1 (Fin.isLt i)] at hb
    rw [R.hop_resulth i.1 (Fin.isLt i)] at hb
    exact hb
  have hmono : R.h (i.1 + 1) u ≤ R.h j.1 u := by
    apply height_mono R
    · omega
    · omega
  omega

Each vertex is relabeled at most 2|V| times.


theorem relabel_count_bound_of (R : Run V G n) (u : V) :
    numRelabelsOf R u ≤ 2 * Fintype.card V := by
  classical
  let S : Finset (Fin n) :=
    (Finset.univ : Finset (Fin n)).filter (fun i => (R.opFin i).relabelOf u = true)
  have hcard : numRelabelsOf R u = S.card := by
    rw [numRelabelsOf]
    rw [Finset.sum_boole]
    rfl
  rw [hcard]
  let f : Fin n → ℕ := fun i => R.h i.1 u
  have hf_inj : Set.InjOn f (↑S : Set (Fin n)) := by
    intro a ha b hb hfab
    have ha' : (R.opFin a).relabelOf u = true := (Finset.mem_filter.mp ha).2
    have hb' : (R.opFin b).relabelOf u = true := (Finset.mem_filter.mp hb).2
    apply Fin.ext
    apply le_antisymm
    · by_contra hgt
      have hlt : b.1 < a.1 := by omega
      have hst := height_strict_between_relabels_of R hlt hb' ha'
      unfold f at hfab
      omega
    · by_contra hgt
      have hlt : a.1 < b.1 := by omega
      have hst := height_strict_between_relabels_of R hlt ha' hb'
      unfold f at hfab
      omega
  have hf_range : ∀ a : Fin n, a ∈ S → f a < 2 * Fintype.card V := by
    intro a ha
    have hrel' : (R.opFin a).relabelOf u = true := (Finset.mem_filter.mp ha).2
    have hoverflow : (R.φ a.1).isOverflowing u := by
      cases hop : R.opFin a with
      | relabel φ h w ho hres hpre =>
          have hwu : w = u := of_decide_eq_true (by simpa [relabelOf, hop] using hrel')
          have hbφ : φ = R.φ a.1 := by
            have h : (R.opFin a).beforeφ = R.φ a.1 := R.hop_beforeφ a.1 (Fin.isLt a)
            simpa [BasicOp.beforeφ, hop] using h
          subst u
          simpa [hbφ] using ho
      | push φ h u' v ho hres hadm =>
          simp [relabelOf, hop] at hrel'
    have hle := height_le_of_overflowing (R.φ a.1) (R.h a.1) (R.hvalid a.1) u
      hoverflow.1 hoverflow.2.2
    have hV : 0 < Fintype.card V := Fintype.card_pos_iff.mpr ⟨G.s⟩
    unfold f
    omega
  calc
    S.card = (S.image f).card := by
      exact (Finset.card_image_iff.mpr hf_inj).symm
    _ ≤ (Finset.range (2 * Fintype.card V)).card := by
      apply Finset.card_le_card
      intro x hx
      rcases Finset.mem_image.mp hx with ⟨a, ha, rfl⟩
      have hlt : f a < 2 * Fintype.card V := hf_range a (by simpa using ha)
      exact Finset.mem_range.mpr hlt
    _ = 2 * Fintype.card V := by simp

The total number of relabel operations is at most 2|V|².


theorem relabel_count_bound (R : Run V G n) :
    numRelabels R ≤ 2 * Fintype.card V * Fintype.card V := by
  have hsum : numRelabels R = ∑ u : V, numRelabelsOf R u := by
    calc
      numRelabels R = ∑ i : Fin n, (if (R.opFin i).isRelabel then 1 else 0) := rfl
      _ = ∑ i : Fin n, ∑ u : V, (if (R.opFin i).relabelOf u then 1 else 0) := by
          apply Finset.sum_congr rfl
          intro i hi
          exact (BasicOp.sum_relabelOf_eq_isRelabel (R.opFin i)).symm
      _ = ∑ u : V, ∑ i : Fin n, (if (R.opFin i).relabelOf u then 1 else 0) := by
          rw [Finset.sum_comm]
      _ = ∑ u : V, numRelabelsOf R u := rfl
  calc
    numRelabels R = ∑ u : V, numRelabelsOf R u := hsum
    _ ≤ ∑ u : V, (2 * Fintype.card V) := by
      apply Finset.sum_le_sum
      intro u _
      exact relabel_count_bound_of R u
    _ = Fintype.card V * (2 * Fintype.card V) := by simp [Finset.sum_const, This simp argument is unused:
  nsmul_eq_mul

Hint: Omit it from the simp argument list.
  simp [Finset.sum_const,̵ ̵n̵s̵m̵u̵l̵_̵e̵q̵_̵m̵u̵l̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`nsmul_eq_mul]
    _ = 2 * Fintype.card V * Fintype.card V := by rw [mul_comm]

Saturating push count bound

The exact effect of pushBy on residual capacity.

lemma pushBy_residualCapacity_eq (φ : Preflow V G) (u v : V) (huv : u ≠ v) (δ : ℝ)
    (hδ_nonneg : 0 ≤ δ) (hδ_le_excess : δ ≤ φ.excess u)
    (hδ_le_residual : δ ≤ φ.residualCapacity u v) (a b : V) :
    (pushBy φ u v huv δ hδ_nonneg hδ_le_excess hδ_le_residual).residualCapacity a b =
      φ.residualCapacity a b - (if a = u ∧ b = v then δ else 0) +
        (if a = v ∧ b = u then δ else 0) := by
  unfold pushBy Preflow.residualCapacity Flow.edgeDelta
  ring

The exact effect of push on residual capacity.

lemma push_residualCapacity_eq (φ : Preflow V G) (u v : V) (hu_ne_s : u ≠ G.s)
    (hres : φ.residualEdge u v) (a b : V) :
    (push φ u v hu_ne_s hres).residualCapacity a b =
      φ.residualCapacity a b -
        (if a = u ∧ b = v then min (φ.excess u) (φ.residualCapacity u v) else 0) +
        (if a = v ∧ b = u then min (φ.excess u) (φ.residualCapacity u v) else 0) := by
  unfold push
  exact pushBy_residualCapacity_eq φ u v (residualEdge_ne φ hres)
    (min (φ.excess u) (φ.residualCapacity u v))
    (le_min (φ.hexcess_nonneg u hu_ne_s) (le_of_lt hres)) (min_le_left _ _)
    (min_le_right _ _) a b

A push that does not run along the reverse edge (v,u) cannot increase the residual capacity of (u,v).


lemma residualCapacity_le_of_not_reverse_push (φ : Preflow V G) (a b : V) (hu_ne_s : a ≠ G.s)
    (hres : φ.residualEdge a b) (u v : V) (hnot : ¬ (a = v ∧ b = u)) :
    (push φ a b hu_ne_s hres).residualCapacity u v ≤ φ.residualCapacity u v := by
  rw [push_residualCapacity_eq φ a b hu_ne_s hres u v]
  have hno_add : (if u = b ∧ v = a then min (φ.excess a) (φ.residualCapacity a b) else 0) = 0 := by
    by_cases h : u = b ∧ v = a
    · have hrev : a = v ∧ b = u := ⟨h.2.symm, h.1.symm⟩
      exact (hnot hrev).elim
    · simp [h]
  rw [hno_add]
  by_cases h : u = a ∧ v = b
  · rcases h with ⟨hau, hbv⟩
    subst u
    subst v
    have hmin_nonneg : 0 ≤ min (φ.excess a) (φ.residualCapacity a b) :=
      le_min (φ.hexcess_nonneg a hu_ne_s) (le_of_lt hres)
    simp only [if_true, and_self]
    linarith
  · simp [h]

A residual capacity that starts at 0 and becomes positive must at some intermediate step be increased by a push along the reverse edge.


lemma exists_reverse_push_of_residual_recovery (R : Run V G n) {u v : V} {i j : ℕ}
    (hij : i + 1 ≤ j) (hj : j ≤ n) (hzero : (R.φ (i + 1)).residualCapacity u v = 0)
    (hpos : (R.φ j).residualCapacity u v > 0) :
    ∃ k : Fin n, i + 1 ≤ k.1 ∧ k.1 < j ∧ (R.opFin k).pushOn v u = true := by
  classical
  have hmain := Nat.le_induction (m := i + 1)
    (P := fun t _ => t ≤ n →
      (R.φ (i + 1)).residualCapacity u v = 0 →
      (R.φ t).residualCapacity u v > 0 →
      ∃ k : Fin n, i + 1 ≤ k.1 ∧ k.1 < t ∧ (R.opFin k).pushOn v u = true)
    (base := by
      intro _ hzero hpos
      linarith)
    (succ := by
      intro t ht ih ht_succ_n hzero hpos
      by_cases hpred : (R.φ t).residualCapacity u v > 0
      · obtain ⟨k, hk1, hk2, hk3⟩ := ih (by omega) hzero hpred
        exact ⟨k, hk1, by omega, hk3⟩
      · have hnonpos : (R.φ t).residualCapacity u v ≤ 0 := le_of_not_gt hpred
        have hpush : (R.opFin ⟨t, by omega⟩).pushOn v u = true := by
          cases hop : R.op t (by omega) with
          | relabel φ h w ho hres hpre =>
              exfalso
              have hb : R.φ t = φ := by
                simpa [BasicOp.beforeφ, hop] using (R.hop_beforeφ t (by omega)).symm
              have hr : R.φ (t + 1) = φ := by
                simpa [BasicOp.resultφ, hop] using (R.hop_resultφ t (by omega)).symm
              have hpos' : (R.φ t).residualCapacity u v > 0 := by
                rw [hb, ← hr]
                exact hpos
              linarith
          | push φ h a b ho hres hadm =>
              have hstep_pos : (R.φ (t + 1)).residualCapacity u v > 0 := by
                have hr : (R.op t (by omega)).resultφ = R.φ (t + 1) :=
                  R.hop_resultφ t (by omega)
                simpa [hop, BasicOp.resultφ, hr] using hpos
              by_contra hnot
              have hle : (R.φ (t + 1)).residualCapacity u v ≤
                  (R.φ t).residualCapacity u v := by
                have hb : (R.op t (by omega)).beforeφ = R.φ t :=
                  R.hop_beforeφ t (by omega)
                have hr : (R.op t (by omega)).resultφ = R.φ (t + 1) :=
                  R.hop_resultφ t (by omega)
                have hnot' : ¬ (a = v ∧ b = u) := by
                  intro hab
                  apply hnot
                  change (R.op t (by omega)).pushOn v u = true
                  simp [pushOn, hop, hab]
                rw [← hb, ← hr]
                simpa [BasicOp.resultφ, BasicOp.beforeφ, hop] using
                  residualCapacity_le_of_not_reverse_push φ a b ho.1 hres u v hnot'
              linarith
        refine ⟨⟨t, by omega⟩, ?_, ?_, hpush⟩
        · exact ht
        · exact Nat.lt_succ_self t)
    j hij hj hzero hpos
  exact hmain

The height of u grows by at least two between two saturating pushes along (u,v).


lemma saturating_height_increase (R : Run V G n) {u v : V} {i j : Fin n} (hij : i.1 < j.1)
    (hsat_i : (R.opFin i).saturatingPushOn u v = true)
    (hsat_j : (R.opFin j).saturatingPushOn u v = true) :
    R.h i.1 u + 2 ≤ R.h j.1 u := by
  have hadm_i : R.h i.1 u = R.h i.1 v + 1 := by
    cases hop : R.opFin i with
    | relabel φ h w ho hres hpre =>
        simp [saturatingPushOn, hop] at hsat_i
    | push φ h a b ho hres hadm =>
        have hle : a = u ∧ b = v ∧ φ.residualCapacity a b ≤ φ.excess a :=
          of_decide_eq_true (by simpa [saturatingPushOn, hop] using hsat_i)
        rcases hle with ⟨ha, hb, _⟩
        have hb_h : R.h i.1 = h := by
          have h' : (R.opFin i).beforeh = R.h i.1 := R.hop_beforeh i.1 (Fin.isLt i)
          rw [← h']
          simp [BasicOp.beforeh, hop]
        subst a; subst b
        rw [hb_h]
        exact hadm
  have hzero : (R.φ (i.1 + 1)).residualCapacity u v = 0 := by
    cases hop : R.opFin i with
    | relabel φ h w ho hres hpre =>
        simp [saturatingPushOn, hop] at hsat_i
    | push φ h a b ho hres hadm =>
        have hle : a = u ∧ b = v ∧ φ.residualCapacity a b ≤ φ.excess a :=
          of_decide_eq_true (by simpa [saturatingPushOn, hop] using hsat_i)
        rcases hle with ⟨ha, hb, hsat⟩
        have hb_φ : R.φ i.1 = φ := by
          have h' : (R.opFin i).beforeφ = R.φ i.1 := R.hop_beforeφ i.1 (Fin.isLt i)
          rw [← h']
          simp [BasicOp.beforeφ, hop]
        have hr_φ : R.φ (i.1 + 1) = (R.opFin i).resultφ := (R.hop_resultφ i.1 (Fin.isLt i)).symm
        subst a; subst b
        rw [hr_φ]
        simp [BasicOp.resultφ, hop, push_residualCapacity_eq φ u v ho.1 hres u v, hsat,
          This simp argument is unused:
  min_eq_right hsat

Hint: Omit it from the simp argument list.
  simp [BasicOp.resultφ, hop, push_residualCapacity_eq φ u v ho.1 hres u v, hsat,
            m̵i̵n̵_̵e̵q̵_̵ri̵g̵h̵t̵ ̵h̵s̵a̵t̵,̵ ̵r̵esidualEdge_ne φ hres]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`min_eq_right hsat, residualEdge_ne φ hres]
  have hpos : (R.φ j.1).residualCapacity u v > 0 := by
    cases hop : R.opFin j with
    | relabel φ h w ho hres hpre =>
        simp [saturatingPushOn, hop] at hsat_j
    | push φ h a b ho hres hadm =>
        have hle : a = u ∧ b = v := by
          have h := of_decide_eq_true (by simpa [saturatingPushOn, hop] using hsat_j)
          exact ⟨h.1, h.2.1⟩
        have hb_φ : R.φ j.1 = φ := by
          have h' : (R.opFin j).beforeφ = R.φ j.1 := R.hop_beforeφ j.1 (Fin.isLt j)
          rw [← h']
          simp [BasicOp.beforeφ, hop]
        rcases hle with ⟨ha, hb⟩
        subst a; subst b
        rw [hb_φ]
        exact hres
  obtain ⟨k, hk1, hk2, hk3⟩ := exists_reverse_push_of_residual_recovery R (by omega : i.1 + 1 ≤ j.1)
    (le_of_lt (Fin.isLt j)) hzero hpos
  have hadm_k : R.h k.1 v = R.h k.1 u + 1 := by
    cases hop : R.op k.1 (Fin.isLt k) with
    | relabel φ h w ho hres hpre =>
        simp [opFin, pushOn, hop] at hk3
    | push φ h a b ho hres hadm =>
        have hle : a = v ∧ b = u := of_decide_eq_true (by simpa [opFin, pushOn, hop] using hk3)
        have hb_h : R.h k.1 = h := by
          have h' : (R.op k.1 (Fin.isLt k)).beforeh = R.h k.1 := R.hop_beforeh k.1 (Fin.isLt k)
          rw [← h']
          simp [BasicOp.beforeh, hop]
        rcases hle with ⟨ha, hb⟩
        subst a; subst b
        rw [hb_h]
        exact hadm
  have hadm_j : R.h j.1 u = R.h j.1 v + 1 := by
    cases hop : R.opFin j with
    | relabel φ h w ho hres hpre =>
        simp [saturatingPushOn, hop] at hsat_j
    | push φ h a b ho hres hadm =>
        have hle : a = u ∧ b = v := by
          have h := of_decide_eq_true (by simpa [saturatingPushOn, hop] using hsat_j)
          exact ⟨h.1, h.2.1⟩
        have hb_h : R.h j.1 = h := by
          have h' : (R.opFin j).beforeh = R.h j.1 := R.hop_beforeh j.1 (Fin.isLt j)
          rw [← h']
          simp [BasicOp.beforeh, hop]
        rcases hle with ⟨ha, hb⟩
        subst a; subst b
        rw [hb_h]
        exact hadm
  have h_iu_ku : R.h i.1 u ≤ R.h k.1 u := height_mono R (by omega) (by omega) u
  have h_kv_jv : R.h k.1 v ≤ R.h j.1 v := height_mono R (by omega) (by omega) v
  omega

Each edge admits at most 2|V| saturating pushes.


theorem saturating_push_count_bound_on (R : Run V G n) (u v : V) :
    numSaturatingPushesOn R u v ≤ 2 * Fintype.card V := by
  classical
  let S : Finset (Fin n) :=
    (Finset.univ : Finset (Fin n)).filter (fun i => (R.opFin i).saturatingPushOn u v = true)
  have hcard : numSaturatingPushesOn R u v = S.card := by
    rw [numSaturatingPushesOn]
    rw [Finset.sum_boole]
    rfl
  rw [hcard]
  let f : Fin n → ℕ := fun i => R.h i.1 u
  have hf_inj : Set.InjOn f (↑S : Set (Fin n)) := by
    intro a ha b hb hfab
    have ha' : (R.opFin a).saturatingPushOn u v = true := (Finset.mem_filter.mp ha).2
    have hb' : (R.opFin b).saturatingPushOn u v = true := (Finset.mem_filter.mp hb).2
    apply Fin.ext
    apply le_antisymm
    · by_contra hgt
      have hlt : b.1 < a.1 := by omega
      have hst := saturating_height_increase R hlt hb' ha'
      unfold f at hfab
      omega
    · by_contra hgt
      have hlt : a.1 < b.1 := by omega
      have hst := saturating_height_increase R hlt ha' hb'
      unfold f at hfab
      omega
  have hf_range : ∀ a : Fin n, a ∈ S → f a < 2 * Fintype.card V := by
    intro a ha
    have hsat' : (R.opFin a).saturatingPushOn u v = true := (Finset.mem_filter.mp ha).2
    have hoverflow : (R.φ a.1).isOverflowing u := by
      cases hop : R.opFin a with
      | relabel φ h w ho hres hpre =>
          simp [saturatingPushOn, hop] at hsat'
      | push φ h a' b ho hres hadm =>
          have hle : a' = u := by
            have h := of_decide_eq_true (by simpa [saturatingPushOn, hop] using hsat')
            exact h.1
          have hbφ : φ = R.φ a.1 := by
            have h : (R.opFin a).beforeφ = R.φ a.1 := R.hop_beforeφ a.1 (Fin.isLt a)
            simpa [BasicOp.beforeφ, hop] using h
          subst u
          simpa [hbφ] using ho
    have hle := height_le_of_overflowing (R.φ a.1) (R.h a.1) (R.hvalid a.1) u
      hoverflow.1 hoverflow.2.2
    have hV : 0 < Fintype.card V := Fintype.card_pos_iff.mpr ⟨G.s⟩
    unfold f
    omega
  calc
    S.card = (S.image f).card := by
      exact (Finset.card_image_iff.mpr hf_inj).symm
    _ ≤ (Finset.range (2 * Fintype.card V)).card := by
      apply Finset.card_le_card
      intro x hx
      rcases Finset.mem_image.mp hx with ⟨a, ha, rfl⟩
      have hlt : f a < 2 * Fintype.card V := hf_range a (by simpa using ha)
      exact Finset.mem_range.mpr hlt
    _ = 2 * Fintype.card V := by simp

A saturating push on (u,v) requires some direction of {u,v} to have positive capacity: either (u,v) itself, or the reverse edge (v,u) (a saturating push may cancel flow on the reverse edge).


lemma saturating_pushOn_imp_cap (R : Run V G n) (u v : V) :
    numSaturatingPushesOn R u v = 0 ∨ 0 < G.c u v ∨ 0 < G.c v u := by
  classical
  by_cases hcap_uv : 0 < G.c u v
  · exact Or.inr (Or.inl hcap_uv)
  · by_cases hcap_vu : 0 < G.c v u
    · exact Or.inr (Or.inr hcap_vu)
    · left
      rw [numSaturatingPushesOn]
      rw [Finset.sum_eq_zero]
      intro i _
      by_cases hsat : (R.opFin i).saturatingPushOn u v = true
      · have hres : (R.φ i.1).residualEdge u v := by
          cases hop : R.opFin i with
          | relabel φ h w ho hres hpre =>
              simp [saturatingPushOn, hop] at hsat
          | push φ h a b ho hres hadm =>
              have hle : a = u ∧ b = v := by
                have h := of_decide_eq_true (by simpa [saturatingPushOn, hop] using hsat)
                exact ⟨h.1, h.2.1⟩
              have hbφ : φ = R.φ i.1 := by
                have h : (R.opFin i).beforeφ = R.φ i.1 := R.hop_beforeφ i.1 (Fin.isLt i)
                simpa [BasicOp.beforeφ, hop] using h
              rcases hle with ⟨ha, hb⟩
              subst a; subst b
              simpa [hbφ] using hres
        have hc_uv_nonneg : 0 ≤ G.c u v := G.hc_nonneg u v
        have hc_vu_nonneg : 0 ≤ G.c v u := G.hc_nonneg v u
        have hc_uv_zero : G.c u v = 0 := le_antisymm (le_of_not_gt hcap_uv) hc_uv_nonneg
        have hc_vu_zero : G.c v u = 0 := le_antisymm (le_of_not_gt hcap_vu) hc_vu_nonneg
        have hcap_vu : (R.φ i.1).f v u ≤ G.c v u := (R.φ i.1).hcapacity v u
        have hskew : (R.φ i.1).f u v = -((R.φ i.1).f v u) := (R.φ i.1).hskew_symm u v
        unfold Preflow.residualEdge Preflow.residualCapacity at hres
        linarith
      · simp [hsat]

The sum of f over univ, restricted by membership in s, equals the sum over s.

try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
private lemma sum_filter_univ_eq {s : Finset (V × V)} {f : V × V → ℕ} :
    (∑ x : V × V, (if x ∈ s then f x else 0)) = ∑ x ∈ s, f x := by
  classical
  have hfilter : (Finset.univ : Finset (V × V)).filter (fun x => x ∈ s) = s := by
    ext x
    simp
  try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hfilter] using (Finset.sum_filter (fun x => x ∈ s) f).symm

The sum of f over univ, restricted by swapped membership in s, equals the sum of f ∘ swap over s.

try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
private lemma sum_filter_univ_swap_eq {s : Finset (V × V)} {f : V × V → ℕ} :
    (∑ x : V × V, (if x.swap ∈ s then f x else 0)) = ∑ x ∈ s, f x.swap := by
  classical
  have hfilter : (Finset.univ : Finset (V × V)).filter (fun x => x ∈ s) = s := by
    ext x
    simp
  have h1 : (∑ x : V × V, (if x.swap ∈ s then f x else 0)) =
      ∑ x : V × V, (if x ∈ s then f x.swap else 0) := by
    exact Equiv.sum_comp (Equiv.prodComm (α := V) (β := V)) (fun x => (if x ∈ s then f x.swap else 0))
  have h2 : (∑ x : V × V, (if x ∈ s then f x.swap else 0)) = ∑ x ∈ s, f x.swap := by
    try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hfilter] using (Finset.sum_filter (fun x => x ∈ s) (fun x => f x.swap)).symm
  rw [h1, h2]

The total number of saturating pushes is at most 4|V|·|E|.


theorem saturating_push_count_bound (R : Run V G n) :
    numSaturatingPushes R ≤ 4 * Fintype.card V * numEdges G := by
  classical
  have hsum : numSaturatingPushes R = ∑ e : V × V, numSaturatingPushesOn R e.1 e.2 := by
    calc
      numSaturatingPushes R = ∑ i : Fin n, (if (R.opFin i).isSaturatingPush then 1 else 0) := rfl
      _ = ∑ i : Fin n, ∑ e : V × V, (if (R.opFin i).saturatingPushOn e.1 e.2 then 1 else 0) := by
          apply Finset.sum_congr rfl
          intro i hi
          exact (BasicOp.sum_saturatingPushOn_eq (R.opFin i)).symm
      _ = ∑ e : V × V, ∑ i : Fin n, (if (R.opFin i).saturatingPushOn e.1 e.2 then 1 else 0) := by
          rw [Finset.sum_comm]
      _ = ∑ e : V × V, numSaturatingPushesOn R e.1 e.2 := rfl
  have hle : (∑ e : V × V, numSaturatingPushesOn R e.1 e.2) ≤
      (∑ e ∈ edgeSet G, numSaturatingPushesOn R e.1 e.2) +
        (∑ e ∈ edgeSet G, numSaturatingPushesOn R e.2 e.1) := by
    calc
      (∑ e : V × V, numSaturatingPushesOn R e.1 e.2) ≤
          ∑ e : V × V, ((if e ∈ edgeSet G then numSaturatingPushesOn R e.1 e.2 else 0) +
            (if e.swap ∈ edgeSet G then numSaturatingPushesOn R e.1 e.2 else 0)) := by
        apply Finset.sum_le_sum
        intro e _
        have h := saturating_pushOn_imp_cap R e.1 e.2
        cases h with
        | inl hz => simp [hz]
        | inr hcap =>
            cases hcap with
            | inl h_uv =>
                have he : e ∈ edgeSet G := Finset.mem_filter.mpr ⟨Finset.mem_univ e, h_uv⟩
                simp [he]
            | inr h_vu =>
                have he : e.swap ∈ edgeSet G := Finset.mem_filter.mpr ⟨Finset.mem_univ e.swap, h_vu⟩
                simp [he]
      _ = (∑ e ∈ edgeSet G, numSaturatingPushesOn R e.1 e.2) +
          (∑ e ∈ edgeSet G, numSaturatingPushesOn R e.2 e.1) := by
        rw [Finset.sum_add_distrib]
        congr 1
        · exact sum_filter_univ_eq
        · exact sum_filter_univ_swap_eq
  calc
    numSaturatingPushes R = ∑ e : V × V, numSaturatingPushesOn R e.1 e.2 := hsum
    _ ≤ (∑ e ∈ edgeSet G, numSaturatingPushesOn R e.1 e.2) +
        (∑ e ∈ edgeSet G, numSaturatingPushesOn R e.2 e.1) := hle
    _ ≤ (∑ e ∈ edgeSet G, (2 * Fintype.card V)) +
        (∑ e ∈ edgeSet G, (2 * Fintype.card V)) := by
        apply Nat.add_le_add
        · apply Finset.sum_le_sum
          intro e _
          exact saturating_push_count_bound_on R e.1 e.2
        · apply Finset.sum_le_sum
          intro e _
          exact saturating_push_count_bound_on R e.2 e.1
    _ = 4 * Fintype.card V * numEdges G := by
      rw [numEdges, edgeSet]
      simp only [Finset.sum_const, nsmul_eq_mul]
      nlinarith

Potential and nonsaturating push count bound

The set of overflowing vertices of a preflow.

noncomputable def overflowSet (φ : Preflow V G) : Finset V :=
  (Finset.univ : Finset V).filter (fun u => φ.isOverflowing u)

The potential Φ = Σ_{overflowing u} h(u).

noncomputable def potential (φ : Preflow V G) (h : V → ℕ) : ℕ :=
  ∑ u ∈ overflowSet φ, h u

Sum of the single-edge skew update over the first argument.


private lemma edgeDelta_sum_first' (δ : ℝ) (u v a : V) :
    (Finset.univ : Finset V).sum (fun x => Flow.edgeDelta δ u v x a) =
      (if a = v then δ else 0) - (if a = u then δ else 0) := by
  unfold Flow.edgeDelta
  rw [Finset.sum_sub_distrib]
  have hf : (Finset.univ : Finset V).sum (fun x => if x = u ∧ a = v then δ else 0) =
      (if a = v then δ else 0) := by
    by_cases hav : a = v
    · subst a; simp
    · simp [hav]
  have hg : (Finset.univ : Finset V).sum (fun x => if x = v ∧ a = u then δ else 0) =
      (if a = u then δ else 0) := by
    by_cases hau : a = u
    · subst a; simp
    · simp [hau]
  rw [hf, hg]

Telescoping: ∑ i in range n, (f (i+1) - f i) = f n - f 0.


private lemma sum_range_sub_eq (f : ℕ → ℤ) (n : ℕ) :
    ∑ i ∈ Finset.range n, (f (i + 1) - f i) = f n - f 0 := by
  induction n with
  | zero => simp
  | succ n ih =>
      rw [Finset.sum_range_succ, ih]
      ring

The potential is bounded by 2|V|².


lemma potential_le (φ : Preflow V G) (h : V → ℕ) (hvalid : IsValidHeight φ h) :
    potential φ h ≤ 2 * Fintype.card V * Fintype.card V := by
  calc
    potential φ h = ∑ u ∈ overflowSet φ, h u := rfl
    _ ≤ ∑ u ∈ overflowSet φ, (2 * Fintype.card V) := by
      apply Finset.sum_le_sum
      intro u hu
      have hoverflow : φ.isOverflowing u := (Finset.mem_filter.mp hu).2
      have hle : h u ≤ 2 * Fintype.card V - 1 :=
        height_le_of_overflowing φ h hvalid u hoverflow.1 hoverflow.2.2
      omega
    _ = (overflowSet φ).card * (2 * Fintype.card V) := by
      simp [Finset.sum_const, This simp argument is unused:
  nsmul_eq_mul

Hint: Omit it from the simp argument list.
  simp [Finset.sum_const,̵ ̵n̵s̵m̵u̵l̵_̵e̵q̵_̵m̵u̵l̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`nsmul_eq_mul]
    _ ≤ Fintype.card V * (2 * Fintype.card V) := by
      exact Nat.mul_le_mul_right (2 * Fintype.card V) (Finset.card_le_univ (overflowSet φ))
    _ = 2 * Fintype.card V * Fintype.card V := by rw [mul_comm]

The exact change of the potential under a relabel.


private lemma potential_relabel_eq (φ : Preflow V G) (h : V → ℕ) (u : V)
    (hres : ∃ v : V, φ.residualEdge u v) (hoverflow : φ.isOverflowing u) :
    ((potential φ (relabel φ h u hres) : ℤ) - (potential φ h : ℤ)) =
      ((relabel φ h u hres u : ℕ) : ℤ) - (h u : ℤ) := by
  unfold potential overflowSet
  rw [Nat.cast_sum, Nat.cast_sum]
  rw [← Finset.sum_sub_distrib]
  rw [Finset.sum_eq_single u]
  · intro b hb hbu
    rw [relabel_eq_of_ne φ h u hres hbu]
    simp
  · intro hu
    have : u ∈ (Finset.univ : Finset V).filter (fun u => φ.isOverflowing u) :=
      Finset.mem_filter.mpr ⟨Finset.mem_univ u, hoverflow⟩
    exact (hu this).elim

A push increases the potential by at most 2|V|.

try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
lemma potential_push_le (φ : Preflow V G) (h : V → ℕ) (u v : V) (hu_ne_s : u ≠ G.s)
    (hres : φ.residualEdge u v) (hadm : h u = h v + 1) (hvalid : IsValidHeight φ h)
    (hoverflow : φ.isOverflowing u) :
    ((potential (push φ u v hu_ne_s hres) h : ℤ) - (potential φ h : ℤ)) ≤ 2 * Fintype.card V := by
  let φ' := push φ u v hu_ne_s hres
  have hsubset : overflowSet φ' ⊆ overflowSet φ ∪ {v} := by
    intro a ha
    have ha' : φ'.isOverflowing a := (Finset.mem_filter.mp ha).2
    by_cases hav : a = v
    · rw [Finset.mem_union]
      right
      try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hav]
    · rw [Finset.mem_union]
      left
      apply Finset.mem_filter.mpr
      constructor
      · exact Finset.mem_univ a
      · have hne_s : a ≠ G.s := ha'.1
        have hne_t : a ≠ G.t := ha'.2.1
        have hpos' : 0 < φ'.excess a := ha'.2.2
        have hle_excess : φ'.excess a ≤ φ.excess a := by
          unfold φ' push pushBy Preflow.excess netInflow
          rw [Finset.sum_add_distrib]
          rw [edgeDelta_sum_first' (min (∑ w : V, φ.f w u) (φ.residualCapacity u v)) u v a]
          have hno_add : (if a = v then min (∑ w : V, φ.f w u) (φ.residualCapacity u v) else 0) = 0 := by
            simp [hav]
          rw [hno_add]
          have hnonneg : 0 ≤ (if a = u then min (∑ w : V, φ.f w u) (φ.residualCapacity u v) else 0) := by
            split
            · exact le_min (φ.hexcess_nonneg u hu_ne_s) (le_of_lt hres)
            · simp
          linarith
        exact ⟨hne_s, hne_t, lt_of_lt_of_le hpos' hle_excess⟩
  have hdiff_le : ((potential φ' h : ℤ) - (potential φ h : ℤ)) ≤ (h v : ℤ) := by
    unfold potential
    have hsum_le : (∑ x ∈ overflowSet φ', h x) ≤ (∑ x ∈ overflowSet φ, h x) + h v := by
      have hle_subset : (∑ x ∈ overflowSet φ', h x) ≤ ∑ x ∈ overflowSet φ ∪ {v}, h x :=
        Finset.sum_le_sum_of_subset_of_nonneg hsubset (fun _ _ _ => Nat.zero_le _)
      have hle_union : (∑ x ∈ overflowSet φ ∪ {v}, h x) ≤ (∑ x ∈ overflowSet φ, h x) + h v := by
        have hdecomp : (∑ x ∈ overflowSet φ ∪ {v}, h x) =
            (∑ x ∈ overflowSet φ, h x) + (∑ x ∈ ({v} : Finset V) \ overflowSet φ, h x) := by
          rw [show overflowSet φ ∪ {v} = overflowSet φ ∪ (({v} : Finset V) \ overflowSet φ) by
            ext x
            by_cases hx : x ∈ overflowSet φ <;> simp [hx]]
          rw [Finset.sum_union]
          exact Finset.disjoint_sdiff
        have hle_singleton : (∑ x ∈ ({v} : Finset V) \ overflowSet φ, h x) ≤ h v := by
          have hsub : (∑ x ∈ ({v} : Finset V) \ overflowSet φ, h x) ≤ ∑ x ∈ ({v} : Finset V), h x :=
            Finset.sum_le_sum_of_subset_of_nonneg Finset.sdiff_subset (fun _ _ _ => Nat.zero_le _)
          simpa using hsub
        rw [hdecomp]
        exact Nat.add_le_add_left hle_singleton (∑ x ∈ overflowSet φ, h x)
      exact le_trans hle_subset hle_union
    have hz : ((∑ x ∈ overflowSet φ', h x : ℕ) : ℤ) ≤ ((∑ x ∈ overflowSet φ, h x : ℕ) : ℤ) + (h v : ℤ) := by
      exact_mod_cast hsum_le
    omega
  have hv_le : (h v : ℤ) ≤ 2 * Fintype.card V := by
    have hu_le : h u ≤ 2 * Fintype.card V - 1 :=
      height_le_of_overflowing φ h hvalid u hoverflow.1 hoverflow.2.2
    have hV : 0 < Fintype.card V := Fintype.card_pos_iff.mpr ⟨G.s⟩
    have hadm' : (h u : ℤ) = (h v : ℤ) + 1 := by omega
    have hu_le_z : (h u : ℤ) ≤ (2 * Fintype.card V : ℤ) := by
      have h' : h u ≤ 2 * Fintype.card V := by omega
      exact_mod_cast h'
    nlinarith
  nlinarith

A nonsaturating push decreases the potential by at least one.

try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
lemma potential_nonsaturating_push_le (φ : Preflow V G) (h : V → ℕ) (u v : V)
    (hu_ne_s : u ≠ G.s) (hres : φ.residualEdge u v) (hadm : h u = h v + 1)
    (hoverflow : φ.isOverflowing u) (hnonsat : φ.excess u < φ.residualCapacity u v) :
    ((potential (push φ u v hu_ne_s hres) h : ℤ) - (potential φ h : ℤ)) ≤ -1 := by
  let φ' := push φ u v hu_ne_s hres
  have hu_not : ¬ φ'.isOverflowing u := by
    intro h
    have hpos : 0 < φ'.excess u := h.2.2
    have hexcess : φ'.excess u = 0 := by
      unfold φ' push pushBy Preflow.excess netInflow
      rw [Finset.sum_add_distrib]
      rw [edgeDelta_sum_first' (min (∑ w : V, φ.f w u) (φ.residualCapacity u v)) u v u]
      have hmin : min (∑ w : V, φ.f w u) (φ.residualCapacity u v) = ∑ w : V, φ.f w u := by
        apply min_eq_left
        exact le_of_lt hnonsat
      rw [hmin]
      simp [residualEdge_ne φ hres]
    linarith
  have hsubset : overflowSet φ' ⊆ (overflowSet φ \ {u}) ∪ {v} := by
    intro a ha
    have ha' : φ'.isOverflowing a := (Finset.mem_filter.mp ha).2
    by_cases hav : a = v
    · rw [Finset.mem_union]
      right
      try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hav]
    · rw [Finset.mem_union]
      left
      apply Finset.mem_sdiff.mpr
      constructor
      · apply Finset.mem_filter.mpr
        constructor
        · exact Finset.mem_univ a
        · have hne_s : a ≠ G.s := ha'.1
          have hne_t : a ≠ G.t := ha'.2.1
          have hpos' : 0 < φ'.excess a := ha'.2.2
          have hle_excess : φ'.excess a ≤ φ.excess a := by
            unfold φ' push pushBy Preflow.excess netInflow
            rw [Finset.sum_add_distrib]
            rw [edgeDelta_sum_first' (min (∑ w : V, φ.f w u) (φ.residualCapacity u v)) u v a]
            have hno_add : (if a = v then min (∑ w : V, φ.f w u) (φ.residualCapacity u v) else 0) = 0 := by
              simp [hav]
            rw [hno_add]
            have hnonneg : 0 ≤ (if a = u then min (∑ w : V, φ.f w u) (φ.residualCapacity u v) else 0) := by
              split
              · exact le_min (φ.hexcess_nonneg u hu_ne_s) (le_of_lt hres)
              · simp
            linarith
          exact ⟨hne_s, hne_t, lt_of_lt_of_le hpos' hle_excess⟩
      · intro hau
        apply hu_not
        exact (Finset.mem_singleton.mp hau) ▸ ha'
  have hu_mem : u ∈ overflowSet φ := Finset.mem_filter.mpr ⟨Finset.mem_univ u, hoverflow⟩
  have hdiff_le : ((potential φ' h : ℤ) - (potential φ h : ℤ)) ≤ -1 := by
    unfold potential
    have hsum_le : (∑ x ∈ overflowSet φ', h x) + h u ≤ (∑ x ∈ overflowSet φ, h x) + h v := by
      have hle_subset : (∑ x ∈ overflowSet φ', h x) ≤ ∑ x ∈ (overflowSet φ \ {u}) ∪ {v}, h x :=
        Finset.sum_le_sum_of_subset_of_nonneg hsubset (fun _ _ _ => Nat.zero_le _)
      have hle_add : (∑ x ∈ overflowSet φ', h x) + h u ≤
          (∑ x ∈ (overflowSet φ \ {u}) ∪ {v}, h x) + h u :=
        Nat.add_le_add_right hle_subset (h u)
      have hle_union : (∑ x ∈ (overflowSet φ \ {u}) ∪ {v}, h x) ≤
          (∑ x ∈ overflowSet φ \ {u}, h x) + h v := by
        have hdecomp : (∑ x ∈ (overflowSet φ \ {u}) ∪ {v}, h x) =
            (∑ x ∈ overflowSet φ \ {u}, h x) + (∑ x ∈ ({v} : Finset V) \ (overflowSet φ \ {u}), h x) := by
          rw [show (overflowSet φ \ {u}) ∪ {v} =
              (overflowSet φ \ {u}) ∪ (({v} : Finset V) \ (overflowSet φ \ {u})) by
            ext x
            by_cases hx : x ∈ overflowSet φ \ {u} <;> simp [hx]]
          rw [Finset.sum_union]
          exact Finset.disjoint_sdiff
        have hle_singleton : (∑ x ∈ ({v} : Finset V) \ (overflowSet φ \ {u}), h x) ≤ h v := by
          have hsub : (∑ x ∈ ({v} : Finset V) \ (overflowSet φ \ {u}), h x) ≤
              ∑ x ∈ ({v} : Finset V), h x :=
            Finset.sum_le_sum_of_subset_of_nonneg Finset.sdiff_subset (fun _ _ _ => Nat.zero_le _)
          simpa using hsub
        rw [hdecomp]
        exact Nat.add_le_add_left hle_singleton (∑ x ∈ overflowSet φ \ {u}, h x)
      have hsum_sdiff : (∑ x ∈ overflowSet φ \ {u}, h x) + h u = ∑ x ∈ overflowSet φ, h x := by
        simpa using (Finset.sum_sdiff (Finset.singleton_subset_iff.mpr hu_mem) :
          (∑ x ∈ overflowSet φ \ {u}, h x) + (∑ x ∈ ({u} : Finset V), h x) = ∑ x ∈ overflowSet φ, h x)
      have hle_mid : (∑ x ∈ (overflowSet φ \ {u}) ∪ {v}, h x) + h u ≤
          (∑ x ∈ overflowSet φ, h x) + h v := by
        omega
      exact le_trans hle_add hle_mid
    have hz : ((∑ x ∈ overflowSet φ', h x : ℕ) : ℤ) + (h u : ℤ) ≤
        ((∑ x ∈ overflowSet φ, h x : ℕ) : ℤ) + (h v : ℤ) := by
      exact_mod_cast hsum_le
    have hadm' : (h u : ℤ) = (h v : ℤ) + 1 := by omega
    omega
  exact hdiff_le

The potential increases across a single step by at most the total height increase plus 2|V| times the number of saturating pushes, minus one per nonsaturating push.


private lemma potential_step_bound_tight (R : Run V G n) (i : Fin n) :
    ((potential (R.φ (i.1 + 1)) (R.h (i.1 + 1)) : ℤ) - (potential (R.φ i.1) (R.h i.1) : ℤ)) ≤
      (∑ x : V, (((R.h (i.1 + 1) x : ℕ) : ℤ) - (R.h i.1 x : ℤ))) +
      (2 * Fintype.card V : ℤ) * (if (R.opFin i).isSaturatingPush then 1 else 0) -
      (if (R.opFin i).isNonsaturatingPush then 1 else 0) := by
  cases hop : R.opFin i with
  | relabel φ h u ho hres hpre =>
      have hb_φ : φ = R.φ i.1 := by
        have h' : (R.opFin i).beforeφ = R.φ i.1 := R.hop_beforeφ i.1 (Fin.isLt i)
        rw [← h']
        simp [BasicOp.beforeφ, hop]
      have hb_h : h = R.h i.1 := by
        have h' : (R.opFin i).beforeh = R.h i.1 := R.hop_beforeh i.1 (Fin.isLt i)
        rw [← h']
        simp [BasicOp.beforeh, hop]
      have hr_φ : R.φ (i.1 + 1) = R.φ i.1 := by
        have h' : (R.opFin i).resultφ = R.φ (i.1 + 1) := R.hop_resultφ i.1 (Fin.isLt i)
        rw [← h']
        simp [BasicOp.resultφ, hop, hb_φ]
      let hres' : ∃ v : V, (R.φ i.1).residualEdge u v := by simpa [hb_φ] using hres
      have hr_h : R.h (i.1 + 1) = Chapter26.relabel (R.φ i.1) (R.h i.1) u hres' := by
        have h' : (R.opFin i).resulth = R.h (i.1 + 1) := R.hop_resulth i.1 (Fin.isLt i)
        rw [← h']
        simp [BasicOp.resulth, hop, hb_φ, hb_h]
      have hdiff := potential_relabel_eq (R.φ i.1) (R.h i.1) u hres' (by simpa [hb_φ] using ho)
      have hsum_eq : (∑ w : V, (((Chapter26.relabel (R.φ i.1) (R.h i.1) u hres' w : ℕ) : ℤ) - (R.h i.1 w : ℤ))) =
          ((Chapter26.relabel (R.φ i.1) (R.h i.1) u hres' u : ℕ) : ℤ) - (R.h i.1 u : ℤ) := by
        rw [Finset.sum_eq_single u]
        · intro b _ hbu
          rw [relabel_eq_of_ne (R.φ i.1) (R.h i.1) u hres' hbu]
          simp
        · intro hu
          simp at hu
      rw [hr_φ, hr_h, hdiff, hsum_eq]
      simp [isSaturatingPush, isNonsaturatingPush, This simp argument is unused:
  hop

Hint: Omit it from the simp argument list.
  simp [isSaturatingPush, isNonsaturatingPush,̵ ̵h̵o̵p̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hop]
  | push φ h u v ho hres hadm =>
      have hb_φ : φ = R.φ i.1 := by
        have h' : (R.opFin i).beforeφ = R.φ i.1 := R.hop_beforeφ i.1 (Fin.isLt i)
        rw [← h']
        simp [BasicOp.beforeφ, hop]
      have hb_h : h = R.h i.1 := by
        have h' : (R.opFin i).beforeh = R.h i.1 := R.hop_beforeh i.1 (Fin.isLt i)
        rw [← h']
        simp [BasicOp.beforeh, hop]
      have hr_φ : R.φ (i.1 + 1) = Chapter26.push (R.φ i.1) u v (by simpa [hb_φ] using ho.1)
          (by simpa [hb_φ] using hres) := by
        have h' : (R.opFin i).resultφ = R.φ (i.1 + 1) := R.hop_resultφ i.1 (Fin.isLt i)
        rw [← h']
        simp [BasicOp.resultφ, hop, hb_φ]
      have hr_h : R.h (i.1 + 1) = R.h i.1 := by
        have h' : (R.opFin i).resulth = R.h (i.1 + 1) := R.hop_resulth i.1 (Fin.isLt i)
        rw [← h']
        simp [BasicOp.resulth, hop, hb_h]
      have hsum_zero : (∑ w : V, (((R.h i.1 w : ℕ) : ℤ) - (R.h i.1 w : ℤ))) = 0 := by
        simp
      by_cases hsat : φ.residualCapacity u v ≤ φ.excess u
      · have hle := potential_push_le (R.φ i.1) (R.h i.1) u v (by simpa [hb_φ] using ho.1)
            (by simpa [hb_φ] using hres) (by simpa [hb_h] using hadm) (R.hvalid i.1)
            (by simpa [hb_φ] using ho)
        have hnot_lt : ¬ φ.excess u < φ.residualCapacity u v := not_lt_of_ge hsat
        rw [hr_φ, hr_h, hsum_zero]
        simp [isSaturatingPush, isNonsaturatingPush, This simp argument is unused:
  hop

Hint: Omit it from the simp argument list.
  simp [isSaturatingPush, isNonsaturatingPush, ho̵p̵,̵ ̵h̵sat, hnot_lt]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hop, hsat, hnot_lt]
        nlinarith [hle]
      · have hlt : φ.excess u < φ.residualCapacity u v := lt_of_not_ge hsat
        have hle := potential_nonsaturating_push_le (R.φ i.1) (R.h i.1) u v (by simpa [hb_φ] using ho.1)
            (by simpa [hb_φ] using hres) (by simpa [hb_h] using hadm) (by simpa [hb_φ] using ho)
            (by simpa [hb_φ] using hlt)
        rw [hr_φ, hr_h, hsum_zero]
        simp [isSaturatingPush, isNonsaturatingPush, This simp argument is unused:
  hop

Hint: Omit it from the simp argument list.
  simp [isSaturatingPush, isNonsaturatingPush, ho̵p̵,̵ ̵h̵sat, hlt]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hop, hsat, hlt]
        nlinarith [hle]

The total height increase across a run is at most 2|V| per vertex.


private lemma height_le_add_bound : ∀ (n : ℕ) (R : Run V G n) (u : V),
    R.h n u ≤ R.h 0 u + 2 * Fintype.card V := by
  intro n
  induction n with
  | zero =>
      intro R u
      omega
  | succ m ih =>
      intro R u
      let R' : Run V G m := {
        φ := R.φ
        h := R.h
        hvalid := R.hvalid
        op := fun i hi => R.op i (Nat.lt_trans hi (Nat.lt_succ_self m))
        hop_beforeφ := fun i hi => R.hop_beforeφ i (Nat.lt_trans hi (Nat.lt_succ_self m))
        hop_beforeh := fun i hi => R.hop_beforeh i (Nat.lt_trans hi (Nat.lt_succ_self m))
        hop_resultφ := fun i hi => R.hop_resultφ i (Nat.lt_trans hi (Nat.lt_succ_self m))
        hop_resulth := fun i hi => R.hop_resulth i (Nat.lt_trans hi (Nat.lt_succ_self m)) }
      have hb := ih R' u
      change R.h m u ≤ R.h 0 u + 2 * Fintype.card V at hb
      cases hop : R.op m (Nat.lt_succ_self m) with
      | relabel φ h w ho hres hpre =>
          by_cases hwu : w = u
          · subst u
            have hoverflow : (R.φ (m + 1)).isOverflowing w := by
              have hrφ : R.φ (m + 1) = φ := by
                simpa [BasicOp.resultφ, hop] using
                  (R.hop_resultφ m (Nat.lt_succ_self m)).symm
              rw [hrφ]
              exact ho
            have hle' := height_le_of_overflowing (R.φ (m + 1)) (R.h (m + 1)) (R.hvalid (m + 1)) w
              hoverflow.1 hoverflow.2.2
            omega
          · have hstep : R.h (m + 1) u = R.h m u := by
              rw [← R.hop_resulth m (Nat.lt_succ_self m), ← R.hop_beforeh m (Nat.lt_succ_self m)]
              simp [BasicOp.resulth, BasicOp.beforeh, hop, relabel_eq_of_ne φ h w hres (Ne.symm hwu)]
            omega
      | push φ h a b ho hres hadm =>
          have hstep : R.h (m + 1) u = R.h m u := by
            rw [← R.hop_resulth m (Nat.lt_succ_self m), ← R.hop_beforeh m (Nat.lt_succ_self m)]
            simp [BasicOp.resulth, BasicOp.beforeh, hop]
          omega

The potential telescopes over a run.

private lemma potential_telescope (R : Run V G n) :
    ((potential (R.φ n) (R.h n) : ℤ) = (potential (R.φ 0) (R.h 0) : ℤ) +
      ∑ i ∈ Finset.range n, (((potential (R.φ (i + 1)) (R.h (i + 1)) : ℤ) -
        (potential (R.φ i) (R.h i) : ℤ)))) := by
  have h := sum_range_sub_eq (fun i => (potential (R.φ i) (R.h i) : ℤ)) n
  omega

The total number of nonsaturating pushes is bounded by O(|V|²(|V|+|E|)).


theorem nonsaturating_push_count_bound (R : Run V G n) :
    numNonsaturatingPushes R ≤ 12 * Fintype.card V * Fintype.card V * (Fintype.card V + numEdges G) := by
  classical
  let Vc := Fintype.card V
  have htel := potential_telescope R
  have hnonneg : 0 ≤ (potential (R.φ n) (R.h n) : ℤ) := by
    exact Int.natCast_nonneg (potential (R.φ n) (R.h n))
  have hinit_ℕ : potential (R.φ 0) (R.h 0) ≤ 2 * Vc * Vc := by
    exact potential_le (R.φ 0) (R.h 0) (R.hvalid 0)
  have hrel_inc_ℕ : (∑ u : V, (R.h n u - R.h 0 u)) ≤ 2 * Vc * Vc := by
    have hbound : ∀ u, R.h n u - R.h 0 u ≤ 2 * Fintype.card V := by
      intro u
      have h : R.h n u ≤ R.h 0 u + 2 * Fintype.card V := height_le_add_bound n R u
      omega
    calc
      (∑ u : V, (R.h n u - R.h 0 u)) ≤ ∑ u : V, (2 * Fintype.card V) := by
        apply Finset.sum_le_sum
        intro u _
        exact hbound u
      _ = Fintype.card V * (2 * Fintype.card V) := by simp [Finset.sum_const, This simp argument is unused:
  nsmul_eq_mul

Hint: Omit it from the simp argument list.
  simp [Finset.sum_const,̵ ̵n̵s̵m̵u̵l̵_̵e̵q̵_̵m̵u̵l̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`nsmul_eq_mul]
      _ = 2 * Vc * Vc := by dsimp [Vc]; rw [mul_comm]
  have hsum_le : (∑ i ∈ Finset.range n,
      (((potential (R.φ (i + 1)) (R.h (i + 1)) : ℤ) - (potential (R.φ i) (R.h i) : ℤ)))) ≤
      (∑ u : V, (((R.h n u : ℕ) : ℤ) - (R.h 0 u : ℤ))) +
        (2 * Vc : ℤ) * (numSaturatingPushes R : ℤ) -
        (numNonsaturatingPushes R : ℤ) := by
    have hfin : (∑ i : Fin n,
        ((potential (R.φ (i.1 + 1)) (R.h (i.1 + 1)) : ℤ) - (potential (R.φ i.1) (R.h i.1) : ℤ))) ≤
        (∑ u : V, (((R.h n u : ℕ) : ℤ) - (R.h 0 u : ℤ))) +
          (2 * Vc : ℤ) * (numSaturatingPushes R : ℤ) -
          (numNonsaturatingPushes R : ℤ) := by
      calc
        (∑ i : Fin n,
          ((potential (R.φ (i.1 + 1)) (R.h (i.1 + 1)) : ℤ) - (potential (R.φ i.1) (R.h i.1) : ℤ))) ≤
          ∑ i : Fin n, ((∑ u : V, (((R.h (i.1 + 1) u : ℕ) : ℤ) - (R.h i.1 u : ℤ))) +
            (2 * Vc : ℤ) * (if (R.opFin i).isSaturatingPush then 1 else 0) -
            (if (R.opFin i).isNonsaturatingPush then 1 else 0)) := by
            apply Finset.sum_le_sum
            intro i _
            exact potential_step_bound_tight R i
        _ = (∑ u : V, (((R.h n u : ℕ) : ℤ) - (R.h 0 u : ℤ))) +
            (2 * Vc : ℤ) * (∑ i : Fin n, (if (R.opFin i).isSaturatingPush then 1 else 0)) -
            (∑ i : Fin n, (if (R.opFin i).isNonsaturatingPush then 1 else 0)) := by
            rw [Finset.sum_sub_distrib, Finset.sum_add_distrib]
            congr 1
            congr 1
            · rw [Finset.sum_comm]
              apply Finset.sum_congr rfl
              intro u _
              have htel_u := sum_range_sub_eq (fun i => (R.h i u : ℤ)) n
              rw [Finset.sum_fin_eq_sum_range]
              exact (Finset.sum_congr rfl (fun x hx => by
                simp [Finset.mem_range.mp hx])).trans htel_u
            · rw [← Finset.mul_sum]
        _ = (∑ u : V, (((R.h n u : ℕ) : ℤ) - (R.h 0 u : ℤ))) +
            (2 * Vc : ℤ) * (numSaturatingPushes R : ℤ) -
            (numNonsaturatingPushes R : ℤ) := by
            simp [numSaturatingPushes, numNonsaturatingPushes]
    have hfin' : (∑ i ∈ Finset.range n,
        ((potential (R.φ (i + 1)) (R.h (i + 1)) : ℤ) - (potential (R.φ i) (R.h i) : ℤ))) =
        (∑ i : Fin n,
          ((potential (R.φ (i.1 + 1)) (R.h (i.1 + 1)) : ℤ) - (potential (R.φ i.1) (R.h i.1) : ℤ))) := by
      rw [Finset.sum_fin_eq_sum_range]
      apply Finset.sum_congr rfl
      intro i hi
      simp [Finset.mem_range.mp hi]
    rw [hfin']
    exact hfin
  have hsum_cast : (∑ u : V, (((R.h n u : ℕ) : ℤ) - (R.h 0 u : ℤ))) =
      ((∑ u : V, (R.h n u - R.h 0 u) : ℕ) : ℤ) := by
    rw [Nat.cast_sum]
    apply Finset.sum_congr rfl
    intro u _
    have hmono : R.h 0 u ≤ R.h n u := height_mono R (Nat.zero_le n) (Nat.le_refl n) u
    exact (Int.ofNat_sub hmono).symm
  have hmain_ℤ : (numNonsaturatingPushes R : ℤ) ≤
      (potential (R.φ 0) (R.h 0) : ℤ) +
        (∑ u : V, (((R.h n u : ℕ) : ℤ) - (R.h 0 u : ℤ))) +
        (2 * Vc : ℤ) * (numSaturatingPushes R : ℤ) := by
    have hsum' := hsum_le
    have : (potential (R.φ 0) (R.h 0) : ℤ) + (∑ i ∈ Finset.range n,
        ((potential (R.φ (i + 1)) (R.h (i + 1)) : ℤ) - (potential (R.φ i) (R.h i) : ℤ))) ≥ 0 := by
      simpa [htel] using hnonneg
    omega
  have hmain_ℕ : numNonsaturatingPushes R ≤ 2 * Vc * Vc + (∑ u : V, (R.h n u - R.h 0 u)) +
      2 * Vc * numSaturatingPushes R := by
    have hinit_z : (potential (R.φ 0) (R.h 0) : ℤ) ≤ ((2 * Vc * Vc : ℕ) : ℤ) := by
      exact_mod_cast hinit_ℕ
    have hz : (numNonsaturatingPushes R : ℤ) ≤
        ((2 * Vc * Vc + (∑ u : V, (R.h n u - R.h 0 u)) + 2 * Vc * numSaturatingPushes R : ℕ) : ℤ) := by
      rw [hsum_cast] at hmain_ℤ
      have hcast : ((2 * Vc * numSaturatingPushes R : ℕ) : ℤ) = (2 * (Vc : ℤ)) * (numSaturatingPushes R : ℤ) := by
        norm_num
      have hcast_add : ((2 * Vc * Vc + (∑ u : V, (R.h n u - R.h 0 u)) + 2 * Vc * numSaturatingPushes R : ℕ) : ℤ) =
          ((2 * Vc * Vc : ℕ) : ℤ) + ((∑ u : V, (R.h n u - R.h 0 u) : ℕ) : ℤ) + ((2 * Vc * numSaturatingPushes R : ℕ) : ℤ) := by
        simp only [Nat.cast_add]
      nlinarith [hmain_ℤ, hinit_z, hcast, hcast_add]
    exact_mod_cast hz
  have hsat := saturating_push_count_bound R
  have hV : 1 ≤ Vc := Fintype.card_pos_iff.mpr ⟨G.s⟩
  dsimp [Vc] at hmain_ℕ hrel_inc_ℕ hsat ⊢
  nlinarith [hmain_ℕ, hrel_inc_ℕ, hsat, hV]

Every step is exactly one of relabel, saturating push, or nonsaturating push.


theorem op_count_decomp (R : Run V G n) :
    n = numRelabels R + numSaturatingPushes R + numNonsaturatingPushes R := by
  have hclass : (∑ i : Fin n, (1 : ℕ)) =
      ∑ i : Fin n, ((if (R.opFin i).isRelabel then 1 else 0) +
         (if (R.opFin i).isSaturatingPush then 1 else 0) +
         (if (R.opFin i).isNonsaturatingPush then 1 else 0)) := by
    apply Finset.sum_congr rfl
    intro i _
    exact (BasicOp.classification (R.opFin i)).symm
  calc
    n = ∑ i : Fin n, (1 : ℕ) := by simp
    _ = ∑ i : Fin n, ((if (R.opFin i).isRelabel then 1 else 0) +
           (if (R.opFin i).isSaturatingPush then 1 else 0) +
           (if (R.opFin i).isNonsaturatingPush then 1 else 0)) := hclass
    _ = numRelabels R + numSaturatingPushes R + numNonsaturatingPushes R := by
        rw [Finset.sum_add_distrib, Finset.sum_add_distrib]
        simp [numRelabels, numSaturatingPushes, numNonsaturatingPushes]

The combined O(V²E) bound on the number of basic operations of the generic push-relabel algorithm.


theorem generic_step_count_bound (R : Run V G n) :
    n ≤ 12 * Fintype.card V * Fintype.card V * Fintype.card V +
        12 * Fintype.card V * Fintype.card V * numEdges G +
        4 * Fintype.card V * numEdges G + 4 * Fintype.card V * Fintype.card V := by
  have hdecomp : n = numRelabels R + numSaturatingPushes R + numNonsaturatingPushes R :=
    op_count_decomp R
  rw [hdecomp]
  have hr : numRelabels R ≤ 2 * Fintype.card V * Fintype.card V := relabel_count_bound R
  have hs : numSaturatingPushes R ≤ 4 * Fintype.card V * numEdges G := saturating_push_count_bound R
  have hn : numNonsaturatingPushes R ≤ 12 * Fintype.card V * Fintype.card V *
      (Fintype.card V + numEdges G) := nonsaturating_push_count_bound R
  nlinarith

end Run

The relabel-to-front discharge order

namespace BasicOp

The active vertex of a basic operation: the relabeled vertex, or the source of the push.

def opVertex : BasicOp V G → V
  | .relabel _ _ u _ _ _ => u
  | .push _ _ u _ _ _ _ => u

end BasicOp

The number of directed edges is at most |V|².


theorem numEdges_le_card_mul_card (G : FlowNetwork V) :
    numEdges G ≤ Fintype.card V * Fintype.card V := by
  unfold numEdges edgeSet
  calc
    ((Finset.univ : Finset (V × V)).filter (fun e => 0 < G.c e.1 e.2)).card
        ≤ (Finset.univ : Finset (V × V)).card := Finset.card_le_card (Finset.filter_subset _ _)
    _ = Fintype.card V * Fintype.card V := by
        rw [Finset.card_univ, Fintype.card_prod]

A relabel-to-front run is a run of the generic push-relabel algorithm that respects the discharge discipline of CLRS §26.5. The DISCHARGE procedure walks current[u] through a per-vertex neighbor list N[u] and, on exhausting it, relabels u and moves it to the front of the list L. The observable consequence of that list discipline is that between two relabel operations no vertex is the source of more than one nonsaturating push, which is exactly the condition recorded here. (A nonsaturating push is the final operation of a DISCHARGE call, so the number of nonsaturating pushes equals the number of DISCHARGE calls.)

The underlying generic run.

The discharge discipline: between two relabels, no vertex is the source of more than one nonsaturating push.

              structure RelabelToFrontRun (V : Type u) [Fintype V] [DecidableEq V]
    (G : FlowNetwork V) (n : ℕ) where  run : Run V G n  discharge_discipline :
    ∀ ⦃i j : ℕ⦄ (hi : i < n) (hj : j < n) (Variable name `hij` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hij : i < j),
      (run.op i hi).isNonsaturatingPush = true →
      (run.op j hj).isNonsaturatingPush = true →
      (∀ k (hk : k < n), i < k → k < j → (run.op k hk).isRelabel = false) →
      BasicOp.opVertex (run.op i hi) ≠ BasicOp.opVertex (run.op j hj)

namespace RelabelToFrontRunvariable {V : Type u} [Fintype V] [DecidableEq V] {G : FlowNetwork V} {n : ℕ}

The set of relabel operations occurring strictly before index i.

noncomputable def relabelsBeforeSet (R : Run V G n) (i : Fin n) : Finset (Fin n) :=
  (Finset.univ : Finset (Fin n)).filter (fun k => (k : ℕ) < i.1 ∧ (R.opFin k).isRelabel = true)

The number of relabel operations occurring strictly before index i.

noncomputable def relabelsBefore (R : Run V G n) (i : Fin n) : ℕ :=
  (relabelsBeforeSet R i).card

relabelsBefore counts a subset of all relabels, so it is at most the total relabel count.


lemma relabelsBefore_le_numRelabels (R : Run V G n) (i : Fin n) :
    relabelsBefore R i ≤ Run.numRelabels R := by
  unfold relabelsBefore relabelsBeforeSet
  rw [Run.numRelabels, Finset.sum_boole]
  apply Finset.card_le_card
  intro k hk
  exact Finset.mem_filter.mpr ⟨Finset.mem_univ k, (Finset.mem_filter.mp hk).2.2⟩

The before-set is monotone in the index.

lemma relabelsBeforeSet_mono (R : Run V G n) {i j : Fin n} (hij : i.1 ≤ j.1) :
    relabelsBeforeSet R i ⊆ relabelsBeforeSet R j := by
  intro k hk
  have hk' := Finset.mem_filter.mp hk
  exact Finset.mem_filter.mpr ⟨Finset.mem_univ k, ⟨lt_of_lt_of_le hk'.2.1 hij, hk'.2.2⟩⟩

If i < j have the same relabelsBefore value, no relabel occurs strictly between them.


lemma no_relabel_between_of_relabelsBefore_eq (R : Run V G n) {i j : Fin n}
    (hij : i.1 < j.1) (h : relabelsBefore R i = relabelsBefore R j) (k : Fin n)
    (hik : i.1 < k.1) (hkj : k.1 < j.1) :
    (R.opFin k).isRelabel = false := by
  by_cases hkrel : (R.opFin k).isRelabel = true
  · have hk_in_j : k ∈ relabelsBeforeSet R j := by
      exact Finset.mem_filter.mpr ⟨Finset.mem_univ k, ⟨hkj, hkrel⟩⟩
    have hk_not_in_i : k ∉ relabelsBeforeSet R i := by
      intro hkin
      have hlt := (Finset.mem_filter.mp hkin).2.1
      omega
    have hsubset : relabelsBeforeSet R i ⊆ relabelsBeforeSet R j :=
      relabelsBeforeSet_mono R (Nat.le_of_lt hij)
    have hproper : relabelsBeforeSet R i ⊂ relabelsBeforeSet R j :=
      ⟨hsubset, fun hsup => hk_not_in_i (hsup hk_in_j)⟩
    have hlt_card : relabelsBefore R i < relabelsBefore R j := by
      unfold relabelsBefore
      exact Finset.card_lt_card hproper
    omega
  · have hfalse : (R.opFin k).isRelabel = false := by
      cases hb : (R.opFin k).isRelabel <;> simp_all
    exact hfalse

Between two relabels, two nonsaturating pushes with equal relabelsBefore values discharge distinct vertices, so equal vertices force equal indices.


lemma opVertex_inj_of_nonsat (R : RelabelToFrontRun V G n) {i j : Fin n}
    (hi : (R.run.opFin i).isNonsaturatingPush = true)
    (hj : (R.run.opFin j).isNonsaturatingPush = true)
    (hrb : relabelsBefore R.run i = relabelsBefore R.run j)
    (hvertex : BasicOp.opVertex (R.run.opFin i) = BasicOp.opVertex (R.run.opFin j)) :
    i = j := by
  by_cases hij : i.1 = j.1
  · exact Fin.ext hij
  · exfalso
    have hlt : i.1 < j.1 ∨ j.1 < i.1 := by omega
    rcases hlt with hlt | hlt
    · have hno := no_relabel_between_of_relabelsBefore_eq R.run hlt hrb
      have hdisc := R.discharge_discipline (i := i.1) (j := j.1) (Fin.isLt i) (Fin.isLt j) hlt hi hj
        (fun k hk hik hkj => hno ⟨k, hk⟩ (by simpa using hik) (by simpa using hkj))
      exact hdisc hvertex
    · have hrb' : relabelsBefore R.run j = relabelsBefore R.run i := hrb.symm
      have hno := no_relabel_between_of_relabelsBefore_eq R.run hlt hrb'
      have hdisc := R.discharge_discipline (i := j.1) (j := i.1) (Fin.isLt j) (Fin.isLt i) hlt hj hi
        (fun k hk hik hkj => hno ⟨k, hk⟩ (by simpa using hik) (by simpa using hkj))
      exact hdisc hvertex.symm

The relabel-to-front discharge order bounds the number of nonsaturating pushes by (|V|·(relabels + 1)), i.e. O(V³).


theorem nonsaturating_push_count_bound (R : RelabelToFrontRun V G n) :
    Run.numNonsaturatingPushes R.run ≤ (Run.numRelabels R.run + 1) * Fintype.card V := by
  classical
  let Rf := R.run
  let S : Finset (Fin n) :=
    (Finset.univ : Finset (Fin n)).filter (fun i => (Rf.opFin i).isNonsaturatingPush = true)
  have hS : Run.numNonsaturatingPushes Rf = S.card := by
    rw [Run.numNonsaturatingPushes, Finset.sum_boole]
    rfl
  rw [hS]
  let f : Fin n → ℕ × V := fun i => (relabelsBefore Rf i, BasicOp.opVertex (Rf.opFin i))
  have hf_inj : Set.InjOn f (↑S : Set (Fin n)) := by
    intro i hi j hj hfij
    have hi' : (Rf.opFin i).isNonsaturatingPush = true := (Finset.mem_filter.mp hi).2
    have hj' : (Rf.opFin j).isNonsaturatingPush = true := (Finset.mem_filter.mp hj).2
    have hrb : relabelsBefore Rf i = relabelsBefore Rf j := by
      exact congrArg Prod.fst hfij
    have hv : BasicOp.opVertex (Rf.opFin i) = BasicOp.opVertex (Rf.opFin j) := by
      exact congrArg Prod.snd hfij
    exact opVertex_inj_of_nonsat R hi' hj' hrb hv
  have hcard_image : S.card = (S.image f).card := by
    exact (Finset.card_image_iff.mpr hf_inj).symm
  calc
    S.card = (S.image f).card := hcard_image
    _ ≤ ((Finset.range (Run.numRelabels Rf + 1)) ×ˢ (Finset.univ : Finset V)).card := by
        apply Finset.card_le_card
        intro x hx
        rcases Finset.mem_image.mp hx with ⟨i, hiS, hxi⟩
        rw [← hxi]
        exact Finset.mem_product.mpr ⟨
          Finset.mem_range.mpr (Nat.lt_succ_of_le (relabelsBefore_le_numRelabels Rf i)),
          Finset.mem_univ (BasicOp.opVertex (Rf.opFin i))⟩
    _ = (Run.numRelabels Rf + 1) * Fintype.card V := by
        rw [Finset.card_product, Finset.card_range, Finset.card_univ]

The combined O(V²E) generic bound already bounds relabels and saturating pushes; the discharge order additionally bounds nonsaturating pushes by (|V|·(relabels + 1)). Assembled, this gives the sharper relabel-to-front O(V³) bound on the number of basic operations.

theorem step_count_bound (R : RelabelToFrontRun V G n) :
    n ≤ 2 * Fintype.card V * Fintype.card V + 4 * Fintype.card V * numEdges G +
      (2 * Fintype.card V * Fintype.card V + 1) * Fintype.card V := by
  have hdecomp := Run.op_count_decomp R.run
  have hr : Run.numRelabels R.run ≤ 2 * Fintype.card V * Fintype.card V :=
    Run.relabel_count_bound R.run
  have hs : Run.numSaturatingPushes R.run ≤ 4 * Fintype.card V * numEdges G :=
    Run.saturating_push_count_bound R.run
  have hn : Run.numNonsaturatingPushes R.run ≤
      (Run.numRelabels R.run + 1) * Fintype.card V := nonsaturating_push_count_bound R
  nlinarith

The relabel-to-front algorithm performs at most 9|V|³ basic operations.

theorem step_count_bound_V3 (R : RelabelToFrontRun V G n) :
    n ≤ 9 * Fintype.card V * Fintype.card V * Fintype.card V := by
  have h := step_count_bound R
  have hE : numEdges G ≤ Fintype.card V * Fintype.card V := numEdges_le_card_mul_card G
  have hV : 1 ≤ Fintype.card V := Fintype.card_pos_iff.mpr ⟨G.s⟩
  nlinarith

              end RelabelToFrontRunend Chapter26end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_24.Section_24_5_Relabel_To_Front.Execution

An initialized relabel-to-front execution with persistent current-neighbor lists.

Initialization writes the complete flow table and height/excess/cursor tables. The scheduler scans inactive entries and rejected neighbors, pushes using cached excess and two indexed arc writes, and relabels with a counted minimum scan. A reversed processed prefix supports constant-cost discharge completion; moving it to the front uses a counted reverse-onto loop. Relabeling immediately moves the current vertex to the front, where its discharge continues.

The ordering, quiet-prefix, and skipped-neighbor invariants are preserved by the controller itself. Its operation trace therefore satisfies the native discharge discipline without an input certificate. The native cubic operation bound proves that the concrete fuelled run terminates; its returned preflow is a maximum flow.

The work theorem counts actual initialization writes, controller/cursor visits, minimum-scan visits, and moved list cells from this run. The scalar/indexed RAM charge assigns a fixed 32-unit allowance to each such event. Exact real arithmetic and indexed tables are primitives in this model; this is not a persistent Lean function-evaluator time bound, a mutable-array refinement, or a bit-complexity claim for arbitrary real capacities.

              namespace CLRS.Chapter26.RelabelExecutionopen Finset Classicalset_option backward.isDefEq.respectTransparency falsevariable {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}noncomputable def initialFunction (G : FlowNetwork V) (u v : V) : ℝ :=
  if u = G.s then G.c G.s v else if v = G.s then -G.c G.s u else 0theorem initialFunction_skew (G : FlowNetwork V) (u v : V) :
    initialFunction G u v = -initialFunction G v u := by
  by_cases hu : u = G.s <;> by_cases hv : v = G.s <;>
    simp [initialFunction, hu, hv, G.hc_self]theorem initialFunction_capacity (G : FlowNetwork V) (u v : V) :
    initialFunction G u v ≤ G.c u v := by
  by_cases hu : u = G.s
  · subst u; simp [initialFunction]
  · by_cases hv : v = G.s
    · subst v
      simp only [initialFunction, if_neg hu, ↓reduceIte]
      linarith [G.hc_nonneg G.s u, G.hc_nonneg u G.s]
    · simpa [initialFunction, hu, hv] using G.hc_nonneg u vtheorem initialFunction_excess (G : FlowNetwork V) (u : V) (hu : u ≠ G.s) :
    netInflow (initialFunction G) u = G.c G.s u := by
  unfold netInflow
  simp [initialFunction, hu]

Indexed writes over an explicit finite enumeration. Counter increments occur at the same recursive nodes that install the returned cells.

def writeCells {ι α : Type*} [DecidableEq ι] (value : ι → α) (base : ι → α) :
    List ι → (ι → α) × Nat
  | [] => (base, 0)
  | i :: is =>
      let tail := writeCells value base is
      (Function.update tail.1 i (value i), tail.2 + 1)

              @[simp] theorem writeCells_count {ι α : Type*} [DecidableEq ι]
    (value base : ι → α) (is : List ι) : (writeCells value base is).2 = is.length := by
  induction is with
  | nil => rfl
  | cons i is ih => simpa [writeCells] using ihtheorem writeCells_value {ι α : Type*} [DecidableEq ι]
    (value base : ι → α) (is : List ι) (a : ι) :
    (writeCells value base is).1 a = if a ∈ is then value a else base a := by
  induction is with
  | nil => simp [writeCells]
  | cons i is ih => by_cases h : a = i <;> simp [writeCells, Function.update, h, ih]noncomputable def tabulate {ι α : Type*} [Fintype ι] [DecidableEq ι]
    (value : ι → α) (default : α) : (ι → α) × Nat :=
  writeCells value (fun _ => default) univ.toList@[simp] theorem tabulate_value {ι α : Type*} [Fintype ι] [DecidableEq ι]
    (value : ι → α) (default : α) : (tabulate value default).1 = value := by
  funext a; simp [tabulate, writeCells_value]@[simp] theorem tabulate_count {ι α : Type*} [Fintype ι] [DecidableEq ι]
    (value : ι → α) (default : α) : (tabulate value default).2 = Fintype.card ι := by
  simp [tabulate]noncomputable def initialCells (G : FlowNetwork V) : (V × V → ℝ) × Nat :=
  tabulate (fun p => initialFunction G p.1 p.2) 0@[simp] theorem initialCells_value (G : FlowNetwork V) (u v : V) :
    (initialCells G).1 (u,v) = initialFunction G u v := by simp [initialCells]

noncomputable def initialPreflow (G : FlowNetwork V) : Preflow V G where
  f := fun u v => (initialCells G).1 (u,v)
  hcapacity := by simpa using initialFunction_capacity G
  hskew_symm := by simpa using initialFunction_skew G
  hexcess_nonneg := by
    intro u hu
    simp only [initialCells_value]
    rw [initialFunction_excess G u hu]
    exact G.hc_nonneg G.s udef initialHeight (G : FlowNetwork V) (u : V) : Nat := if u = G.s then Fintype.card V else 0

theorem initial_valid (G : FlowNetwork V) : IsValidHeight (initialPreflow G) (initialHeight G) := by
  refine ⟨by simp [initialHeight], by simp [initialHeight, Ne.symm G.hs_ne_t], ?_⟩
  intro u v hr
  by_cases hu : u = G.s
  · subst u
    have hz : (initialPreflow G).residualCapacity G.s v = 0 := by
      simp [Preflow.residualCapacity, initialPreflow, initialFunction]
    exact (show False from by change 0 < _ at hr; rw [hz] at hr; linarith).elim
  · simp [initialHeight, hu]

Push changes only its two endpoint excesses.


theorem push_excess (φ : Preflow V G) (u v : V) (hu : u ≠ G.s)
    (hr : φ.residualEdge u v) (a : V) :
    (push φ u v hu hr).excess a = φ.excess a +
      (if a = v then min (φ.excess u) (φ.residualCapacity u v) else 0) -
      (if a = u then min (φ.excess u) (φ.residualCapacity u v) else 0) := by
  unfold push pushBy Preflow.excess netInflow
  rw [Finset.sum_add_distrib]
  have hed (δ : ℝ) : ∑ x : V, Flow.edgeDelta δ u v x a =
      (if a = v then δ else 0) - (if a = u then δ else 0) := by
    unfold Flow.edgeDelta
    rw [Finset.sum_sub_distrib]
    have hf : (∑ x : V, if x = u ∧ a = v then δ else 0) = (if a = v then δ else 0) := by
      by_cases ha : a = v
      · subst a; simp
      · simp [ha]
    have hg : (∑ x : V, if x = v ∧ a = u then δ else 0) = (if a = u then δ else 0) := by
      by_cases ha : a = u
      · subst a; simp
      · simp [ha]
    rw [hf, hg]
  rw [hed]
  ring

theorem push_valid (φ : Preflow V G) (h : V → Nat) (hv : IsValidHeight φ h)
    (u v : V) (hu : φ.isOverflowing u) (hr : φ.residualEdge u v)
    (ha : h u = h v + 1) : IsValidHeight (push φ u v hu.1 hr) h := by
  unfold push
  exact pushBy_validHeight φ h hv _ _ _ _ _ _ _ ha

theorem push_new_admissible (φ : Preflow V G) (h : V → Nat)
    (u v : V) (hu : φ.isOverflowing u) (hr : φ.residualEdge u v)
    (ha : h u = h v + 1) (a b : V)
    (hab : admissibleEdge (push φ u v hu.1 hr) h a b) : admissibleEdge φ h a b := by
  refine ⟨?_, hab.2⟩
  by_contra hn
  have hnew := pushBy_new_residualEdge φ u v (residualEdge_ne φ hr)
    (min (φ.excess u) (φ.residualCapacity u v))
    (le_min (φ.hexcess_nonneg u hu.1) (le_of_lt hr))
    (min_le_left _ _) (min_le_right _ _) hab.1 hn
  rcases hnew with ⟨rfl, rfl⟩
  have hh := hab.2
  omega

A skipped neighbor stays ineligible until this source is relabeled.

def CursorInvariant (φ : Preflow V G) (h : V → Nat) (cursor : V → List V) : Prop :=
  ∀ u v, v ∉ cursor u → φ.residualEdge u v → h u ≤ h v

              theorem cursor_push (φ : Preflow V G) (h : V → Nat) (cursor : V → List V)
    (hc : CursorInvariant φ h cursor) (u v : V) (hu : φ.isOverflowing u)
    (hr : φ.residualEdge u v) (ha : h u = h v + 1) :
    CursorInvariant (push φ u v hu.1 hr) h cursor := by
  intro a b hb hnew
  by_cases hold : φ.residualEdge a b
  · exact hc a b hb hold
  · have hrev := pushBy_new_residualEdge φ u v (residualEdge_ne φ hr)
      (min (φ.excess u) (φ.residualCapacity u v))
      (le_min (φ.hexcess_nonneg u hu.1) (le_of_lt hr))
      (min_le_left _ _) (min_le_right _ _) hnew hold
    rcases hrev with ⟨rfl, rfl⟩
    omega

theorem cursor_relabel (φ : Preflow V G) (h : V → Nat) (cursor : V → List V)
    (hc : CursorInvariant φ h cursor) (u : V) (hr : ∃ v, φ.residualEdge u v)
    (hpre : ∀ v, φ.residualEdge u v → h u ≤ h v) :
    CursorInvariant φ (relabel φ h u hr) (Function.update cursor u univ.toList) := by
  intro a b hb hab
  by_cases ha : a = u
  · subst a; simp at hb
  · have hold : b ∉ cursor a := by simpa [Function.update, ha] using hb
    have hle := hc a b hold hab
    have hup := (relabel_height_increase φ h u hr hpre).le
    rw [relabel_eq_of_ne φ h u hr ha]
    by_cases hbu : b = u
    · subst b; exact hle.trans hup
    · rwa [relabel_eq_of_ne φ h u hr hbu]def Internal (G : FlowNetwork V) (u : V) : Prop := u ≠ G.s ∧ u ≠ G.tdef Ordered (φ : Preflow V G) (h : V → Nat) (L : List V) : Prop :=
  L.Pairwise (fun a b => ¬ admissibleEdge φ h b a)structure Machine (G : FlowNetwork V) where
  φ : Preflow V G
  h : V → Nat
  excessCache : V → ℝ
  cache_correct : ∀ u, u ≠ G.s → excessCache u = φ.excess u
  valid : IsValidHeight φ h
  past : List V
  todo : List V
  nodup : (past.reverse ++ todo).Nodup
  complete : ∀ v, v ∈ past.reverse ++ todo ↔ Internal G v
  ordered : Ordered φ h (past.reverse ++ todo)
  quiet : ∀ v ∈ past.reverse, ¬ φ.isOverflowing v
  cursor : V → List V
  cursor_bound : ∀ v, (cursor v).length ≤ Fintype.card V
  skipped : CursorInvariant φ h cursordef Machine.done (s : Machine G) : List V := s.past.reversenoncomputable def selectInternal (G : FlowNetwork V) : List V → List V × Nat
  | [] => ([], 0)
  | u :: us =>
      let tail := selectInternal G us
      (if Internal G u then u :: tail.1 else tail.1, tail.2 + 1)@[simp] theorem selectInternal_value (G : FlowNetwork V) (xs : List V) :
    (selectInternal G xs).1 = xs.filter (fun v => decide (Internal G v)) := by
  induction xs with
  | nil => rfl
  | cons u us ih => by_cases hu : Internal G u <;> simp [selectInternal, hu, ih]@[simp] theorem selectInternal_count (G : FlowNetwork V) (xs : List V) :
    (selectInternal G xs).2 = xs.length := by
  induction xs with
  | nil => rfl
  | cons u us ih => simpa [selectInternal] using ih

noncomputable def initialMachine (G : FlowNetwork V) : Machine G where
  φ := initialPreflow G
  h := (tabulate (initialHeight G) 0).1
  excessCache := (tabulate (G.c G.s) 0).1
  cache_correct := by intro u hu; simpa [initialPreflow, Preflow.excess] using (initialFunction_excess G u hu).symm
  valid := by simpa using initial_valid G
  past := []
  todo := (selectInternal G univ.toList).1
  nodup := by simpa using (Finset.nodup_toList (univ : Finset V)).filter _
  complete := by simp
  ordered := by
    simp only [List.reverse_nil, List.nil_append, selectInternal_value]
    apply List.pairwise_iff_getElem.mpr
    intro i j hi hj hij hadm
    have hia : (univ.toList.filter (fun v => decide (Internal G v)))[i] ≠ G.s := by
      have hm := List.getElem_mem hi
      exact (of_decide_eq_true (List.mem_filter.mp hm).2).1
    have hja : (univ.toList.filter (fun v => decide (Internal G v)))[j] ≠ G.s := by
      have hm := List.getElem_mem hj
      exact (of_decide_eq_true (List.mem_filter.mp hm).2).1
    have he := hadm.2
    simp only [tabulate_value] at he
    change (if (univ.toList.filter (fun v => decide (Internal G v)))[j] = G.s then Fintype.card V else 0) =
      (if (univ.toList.filter (fun v => decide (Internal G v)))[i] = G.s then Fintype.card V else 0) + 1 at he
    rw [if_neg hja, if_neg hia] at he
    omega
  quiet := by simp
  cursor := (tabulate (fun _ : V => (univ.toList : List V)) []).1
  cursor_bound := by simp
  skipped := by intro u v hv; simp at hvnoncomputable def credit (s : Machine G) : Nat :=
  s.todo.length + ∑ v, (s.cursor v).lengththeorem credit_initial (G : FlowNetwork V) :
    credit (initialMachine G) ≤ Fintype.card V + Fintype.card V * Fintype.card V := by
  have hl := List.length_filter_le (fun v => decide (Internal G v)) (univ.toList : List V)
  simp only [Finset.length_toList, Finset.card_univ] at hl
  simpa [credit, initialMachine] using Nat.add_le_add_right hl (Fintype.card V * Fintype.card V)theorem ordered_push (s : Machine G) (u v : V) (hu : s.φ.isOverflowing u)
    (hr : s.φ.residualEdge u v) (ha : s.h u = s.h v + 1) :
    Ordered (push s.φ u v hu.1 hr) s.h (s.done ++ s.todo) := by
  apply s.ordered.imp
  intro a b hold hn
  exact hold (push_new_admissible s.φ s.h u v hu hr ha b a hn)

theorem current_not_done (s : Machine G) {u : V} {us : List V} (ht : s.todo = u :: us) :
    u ∉ s.done := by
  have hn := s.nodup
  rw [ht, List.nodup_append] at hn
  intro hu
  exact hn.2.2 u hu u (by simp) rfltheorem current_internal (s : Machine G) {u : V} {us : List V} (ht : s.todo = u :: us) :
    Internal G u := (s.complete u).1 (by simp [ht])

theorem push_quiet_done (s : Machine G) {u : V} {us : List V} (ht : s.todo = u :: us)
    (v : V) (hu : s.φ.isOverflowing u) (hr : s.φ.residualEdge u v)
    (ha : s.h u = s.h v + 1) :
    ∀ a ∈ s.done, ¬ (push s.φ u v hu.1 hr).isOverflowing a := by
  intro a haD hover
  have hau : a ≠ u := by intro h; subst a; exact current_not_done s ht haD
  have hav : a ≠ v := by
    intro h; subst a
    have hord := List.pairwise_append.mp s.ordered
    exact hord.2.2 v haD u (by simp [ht]) ⟨hr, ha⟩
  have he : (push s.φ u v hu.1 hr).excess a = s.φ.excess a := by
    rw [push_excess]; simp [hau, hav]
  exact s.quiet a haD ⟨hover.1, hover.2.1, by simpa [he] using hover.2.2⟩noncomputable def skipCurrent (s : Machine G) (u : V) (us : List V)
    (ht : s.todo = u :: us) (hq : ¬ s.φ.isOverflowing u) : Machine G :=
  { s with
    past := u :: s.past
    todo := us
    nodup := by simpa [ht, Machine.done, List.reverse_cons, List.append_assoc] using s.nodup
    complete := by intro v; simpa [ht, Machine.done, List.reverse_cons, List.append_assoc] using s.complete v
    ordered := by simpa [ht, Machine.done, List.reverse_cons, List.append_assoc] using s.ordered
    quiet := by
      intro v hv
      simp only [List.reverse_cons] at hv
      rcases List.mem_append.mp hv with hv | hv
      · exact s.quiet v hv
      · simpa using (List.mem_singleton.mp hv) ▸ hq }theorem credit_skip (s : Machine G) (u : V) (us : List V)
    (ht : s.todo = u :: us) (hq : ¬ s.φ.isOverflowing u) :
    credit (skipCurrent s u us ht hq) + 1 = credit s := by
  simp [credit, skipCurrent, ht]
  omega

noncomputable def advanceCursor (s : Machine G) (u v : V) (vs : List V)
    (hc : s.cursor u = v :: vs) (hn : ¬ admissibleEdge s.φ s.h u v) : Machine G :=
  { s with
    cursor := Function.update s.cursor u vs
    cursor_bound := by
      intro a
      by_cases ha : a = u
      · subst a; simp only [Function.update_self]
        have hb := s.cursor_bound u; rw [hc] at hb; simpa using Nat.le_trans (Nat.le_succ _) hb
      · simpa [Function.update, ha] using s.cursor_bound a
    skipped := by
      intro a b hb hr
      by_cases ha : a = u
      · subst a
        simp only [Function.update_self] at hb
        by_cases hbv : b = v
        · subst b
          have hv := s.valid.2.2 u v hr
          have hne : s.h u ≠ s.h v + 1 := fun he => hn ⟨hr, he⟩
          omega
        · apply s.skipped u b ?_ hr
          simp [hc, hb, hbv]
      · apply s.skipped a b ?_ hr
        simpa [Function.update, ha] using hb }

theorem credit_advanceCursor (s : Machine G) (u v : V) (vs : List V)
    (hc : s.cursor u = v :: vs) (hn : ¬ admissibleEdge s.φ s.h u v) :
    credit (advanceCursor s u v vs hc hn) + 1 = credit s := by
  unfold credit
  have hfun : (fun a => ((advanceCursor s u v vs hc hn).cursor a).length) =
      Function.update (fun a => (s.cursor a).length) u vs.length := by
    funext a
    by_cases ha : a = u <;> simp [advanceCursor, Function.update, ha]
  rw [hfun, Finset.sum_update_of_mem (Finset.mem_univ u)]
  have hs := Finset.sum_erase_add (univ : Finset V) (fun a => (s.cursor a).length) (mem_univ u)
  rw [hc] at hs
  simp only [List.length_cons] at hs
  simp only [advanceCursor]
  rw [Finset.sdiff_singleton_eq_erase]
  omega


theorem ordered_relabel (s : Machine G) (u : V) (us : List V) (ht : s.todo = u :: us)
    (hr : ∃ v, s.φ.residualEdge u v)
    (hp : ∀ v, s.φ.residualEdge u v → s.h u ≤ s.h v) :
    Ordered s.φ (relabel s.φ s.h u hr) (u :: (s.done ++ us)) := by
  have hn : (u :: (s.done ++ us)).Nodup := List.perm_middle.nodup (by simpa [ht, Machine.done] using s.nodup)
  have hnot := (List.nodup_cons.mp hn).1
  have ho : Ordered s.φ s.h (s.done ++ us) := by
    exact s.ordered.sublist (by rw [ht]; exact List.Sublist.append (List.Sublist.refl _) (List.sublist_cons_self _ _))
  apply List.Pairwise.cons
  · intro a ha hadm
    have hau : a ≠ u := by intro he; subst a; exact hnot ha
    have old := s.valid.2.2 a u hadm.1
    have inc := relabel_height_increase s.φ s.h u hr hp
    have eqn := hadm.2
    rw [relabel_eq_of_ne s.φ s.h u hr hau] at eqn
    omega
  · apply List.Pairwise.imp_of_mem _ ho
    intro a b ha hb hold hnew
    have hau : a ≠ u := by intro he; subst a; exact hnot ha
    have hbu : b ≠ u := by intro he; subst b; exact hnot hb
    apply hold
    refine ⟨hnew.1, ?_⟩
    simpa only [relabel_eq_of_ne s.φ s.h u hr hau,
      relabel_eq_of_ne s.φ s.h u hr hbu] using hnew.2

A literal residual-neighbor scan: one candidate visit at every list cell.

noncomputable def scanMinimum (φ : Preflow V G) (h : V → Nat) (u : V) :
    List V → WithTop Nat × Nat
  | [] => (⊤, 0)
  | v :: vs =>
      let tail := scanMinimum φ h u vs
      (if φ.residualEdge u v then min (h v : WithTop Nat) tail.1 else tail.1, tail.2 + 1)

              @[simp] theorem scanMinimum_visits (φ : Preflow V G) (h : V → Nat) (u : V) (vs : List V) :
    (scanMinimum φ h u vs).2 = vs.length := by
  induction vs with
  | nil => rfl
  | cons v vs ih => simpa [scanMinimum] using ihtheorem scanMinimum_value (φ : Preflow V G) (h : V → Nat) (u : V) (vs : List V) :
    (scanMinimum φ h u vs).1 = ((vs.filter fun v => decide (φ.residualEdge u v)).map h).minimum := by
  induction vs with
  | nil => simp [scanMinimum]
  | cons v vs ih => by_cases hv : φ.residualEdge u v <;> simp [scanMinimum, hv, ih, List.minimum_cons]noncomputable def scannedRelabel (φ : Preflow V G) (h : V → Nat) (u : V) : V → Nat :=
  let least := (scanMinimum φ h u univ.toList).1.untopD 0
  Function.update h u (1 + least)

theorem scannedRelabel_eq (φ : Preflow V G) (h : V → Nat) (u : V)
    (hr : ∃ v, φ.residualEdge u v) : scannedRelabel φ h u = relabel φ h u hr := by
  let S := ((univ : Finset V).filter (fun v => φ.residualEdge u v)).image h
  have hS : S.Nonempty := by
    obtain ⟨v, hv⟩ := hr
    exact ⟨h v, mem_image.mpr ⟨v, mem_filter.mpr ⟨mem_univ _, hv⟩, rfl⟩⟩
  have heq : (scanMinimum φ h u univ.toList).1 = (S.min' hS : WithTop Nat) := by
    rw [scanMinimum_value]
    apply (List.minimum_eq_coe_iff (m := S.min' hS)).mpr
    constructor
    · obtain ⟨v, hv, he⟩ := mem_image.mp (Finset.min'_mem S hS)
      exact List.mem_map.mpr ⟨v, List.mem_filter.mpr ⟨by simp, by simpa using (mem_filter.mp hv).2⟩, he⟩
    · intro a ha
      obtain ⟨v, hv, rfl⟩ := List.mem_map.mp ha
      exact Finset.min'_le S _ (mem_image.mpr ⟨v, mem_filter.mpr ⟨mem_univ _,
        by simpa using (List.mem_filter.mp hv).2⟩, rfl⟩)
  funext a
  by_cases hau : a = u
  · subst a
    simp only [scannedRelabel, heq, Function.update_self]
    calc
      _ = 1 + S.min' hS := congrArg (1 + ·) (WithTop.untopD_coe 0 (S.min' hS))
      _ = _ := by unfold relabel; simp only [↓reduceIte]; rfl
  · simp [scannedRelabel, hau, relabel_eq_of_ne φ h u hr hau]

Reverse the processed prefix directly onto the remaining suffix. Each visited cell performs one cons; no repeated append traversal is hidden in a discharge.

def reverseOnto {α : Type*} : List α → List α → List α × Nat
  | [], acc => (acc, 0)
  | a :: as, acc =>
      let tail := reverseOnto as (a :: acc)
      (tail.1, tail.2 + 1)

              @[simp] theorem reverseOnto_value {α : Type*} (xs acc : List α) :
    (reverseOnto xs acc).1 = xs.reverse ++ acc := by
  induction xs generalizing acc with
  | nil => simp [reverseOnto]
  | cons a as ih => simp [reverseOnto, ih, List.reverse_cons, List.append_assoc]@[simp] theorem reverseOnto_count {α : Type*} (xs acc : List α) :
    (reverseOnto xs acc).2 = xs.length := by
  induction xs generalizing acc with
  | nil => rfl
  | cons a as ih => simp [reverseOnto, ih]

noncomputable def relabelCurrent (s : Machine G) (u : V) (us : List V)
    (ht : s.todo = u :: us) (hu : s.φ.isOverflowing u)
    (hr : ∃ v, s.φ.residualEdge u v)
    (hp : ∀ v, s.φ.residualEdge u v → s.h u ≤ s.h v) : Machine G where
  φ := s.φ
  h := scannedRelabel s.φ s.h u
  excessCache := s.excessCache
  cache_correct := s.cache_correct
  valid := by rw [scannedRelabel_eq _ _ _ hr]; exact relabel_validHeight s.φ s.h s.valid u hu.1 hu.2.1 hr hp
  past := []
  todo := u :: (reverseOnto s.past us).1
  nodup := by simpa only [List.reverse_nil, List.nil_append, reverseOnto_value, Machine.done] using List.perm_middle.nodup (by simpa [ht, Machine.done] using s.nodup)
  complete := by intro a; simpa [ht, Machine.done, List.mem_append, or_assoc, or_left_comm] using s.complete a
  ordered := by rw [scannedRelabel_eq _ _ _ hr]; simpa [Machine.done] using ordered_relabel s u us ht hr hp
  quiet := by simp
  cursor := Function.update s.cursor u univ.toList
  cursor_bound := by intro a; by_cases ha : a = u <;> simp [Function.update, ha, s.cursor_bound]
  skipped := by rw [scannedRelabel_eq _ _ _ hr]; exact cursor_relabel s.φ s.h s.cursor s.skipped u hr hp

theorem credit_relabel (s : Machine G) (u : V) (us : List V)
    (ht : s.todo = u :: us) (hu : s.φ.isOverflowing u)
    (hr : ∃ v, s.φ.residualEdge u v)
    (hp : ∀ v, s.φ.residualEdge u v → s.h u ≤ s.h v) :
    credit (relabelCurrent s u us ht hu hr hp) ≤ credit s + 2 * Fintype.card V := by
  have hl := List.Nodup.length_le_card s.nodup
  rw [ht] at hl
  have hsum := Finset.sum_erase_add (univ : Finset V) (fun a => (s.cursor a).length) (mem_univ u)
  have hfun : (fun a => ((relabelCurrent s u us ht hu hr hp).cursor a).length) =
      Function.update (fun a => (s.cursor a).length) u (Fintype.card V) := by
    funext a; by_cases ha : a = u <;> simp [relabelCurrent, Function.update, ha]
  unfold credit
  rw [hfun, Finset.sum_update_of_mem (mem_univ u), Finset.sdiff_singleton_eq_erase]
  simp only [relabelCurrent, ht, List.length_cons, reverseOnto_value, List.length_append] at *
  omegadef pushCells (f : V → V → ℝ) (u v : V) (δ : ℝ) : V → V → ℝ :=
  Function.update (Function.update f u (Function.update (f u) v (f u v + δ)))
    v (Function.update (f v) u (f v u - δ))automatically included section variable(s) unused in theorem `CLRS.Chapter26.RelabelExecution.pushCells_eq`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter26.RelabelExecution.pushCells_eq`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter26.RelabelExecution.pushCells_eq`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`automatically included section variable(s) unused in theorem `CLRS.Chapter26.RelabelExecution.pushCells_eq`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter26.RelabelExecution.pushCells_eq`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter26.RelabelExecution.pushCells_eq`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter26.RelabelExecution.pushCells_eq`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter26.RelabelExecution.pushCells_eq`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter26.RelabelExecution.pushCells_eq`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter26.RelabelExecution.pushCells_eq`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter26.RelabelExecution.pushCells_eq`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter26.RelabelExecution.pushCells_eq`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter26.RelabelExecution.pushCells_eq`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter26.RelabelExecution.pushCells_eq`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`

automatically included section variable(s) unused in theorem `CLRS.Chapter26.RelabelExecution.pushCells_eq`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`theorem pushCells_eq (f : V → V → ℝ) (u v : V) (huv : u ≠ v) (δ : ℝ) :
    pushCells f u v δ = fun a b => f a b + Flow.edgeDelta δ u v a b := by
  funext a b
  by_cases hau : a = u <;> by_cases hav : a = v <;>
    by_cases hbu : b = u <;> by_cases hbv : b = v <;>
    simp_all [pushCells, Function.update, Flow.edgeDelta] Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`<;> ringtheorem preflow_ext {φ ψ : Preflow V G} (h : φ.f = ψ.f) : φ = ψ := by
  cases φ; cases ψ; cases h; rfl

noncomputable def cachedPush (s : Machine G) (u v : V) (hu : u ≠ G.s)
    (hr : s.φ.residualEdge u v) : Preflow V G := by
  let δ := min (s.excessCache u) (s.φ.residualCapacity u v)
  let φ' := pushBy s.φ u v (residualEdge_ne s.φ hr) δ
    (by dsimp [δ]; rw [s.cache_correct u hu]; exact le_min (s.φ.hexcess_nonneg u hu) hr.le)
    (by dsimp [δ]; rw [s.cache_correct u hu]; exact min_le_left _ _)
    (by dsimp [δ]; exact min_le_right _ _)
  let f' := pushCells s.φ.f u v δ
  have hf : f' = φ'.f := pushCells_eq s.φ.f u v (residualEdge_ne s.φ hr) δ
  exact { f := f'
          hcapacity := by rw [hf]; exact φ'.hcapacity
          hskew_symm := by rw [hf]; exact φ'.hskew_symm
          hexcess_nonneg := by rw [hf]; exact φ'.hexcess_nonneg }@[simp] theorem cachedPush_eq (s : Machine G) (u v : V) (hu : u ≠ G.s)
    (hr : s.φ.residualEdge u v) : cachedPush s u v hu hr = push s.φ u v hu hr := by
  apply preflow_ext
  simp [cachedPush, push, pushBy, pushCells_eq _ _ _ (residualEdge_ne s.φ hr), s.cache_correct u hu]noncomputable def pushedCache (s : Machine G) (u v : V) : V → ℝ :=
  let δ := min (s.excessCache u) (s.φ.residualCapacity u v)
  Function.update (Function.update s.excessCache u (s.excessCache u - δ)) v (s.excessCache v + δ)

theorem pushedCache_correct (s : Machine G) (u v : V) (hu : u ≠ G.s)
    (hr : s.φ.residualEdge u v) (a : V) (has : a ≠ G.s) :
    pushedCache s u v a = (cachedPush s u v hu hr).excess a := by
  rw [cachedPush_eq, push_excess]
  have huv := residualEdge_ne s.φ hr
  by_cases hau : a = u <;> by_cases hav : a = v <;>
    simp_all [pushedCache, Function.update, s.cache_correct]

noncomputable def pushCurrent (s : Machine G) (u : V) (us : List V) (ht : s.todo = u :: us)
    (v : V) (hu : s.φ.isOverflowing u) (hr : s.φ.residualEdge u v)
    (ha : s.h u = s.h v + 1) : Machine G := by
  let φ' := cachedPush s u v hu.1 hr
  have hvalid : IsValidHeight φ' s.h := by simpa [φ'] using push_valid s.φ s.h s.valid u v hu hr ha
  have hord : Ordered φ' s.h (s.done ++ s.todo) := by simpa [φ'] using ordered_push s u v hu hr ha
  have hquiet : ∀ a ∈ s.done, ¬ φ'.isOverflowing a := by simpa [φ'] using push_quiet_done s ht v hu hr ha
  have hskip : CursorInvariant φ' s.h s.cursor := by simpa [φ'] using cursor_push s.φ s.h s.cursor s.skipped u v hu hr ha
  exact if hnCache : s.excessCache u < s.φ.residualCapacity u v then
    let hn : s.φ.excess u < s.φ.residualCapacity u v := by simpa [s.cache_correct u hu.1] using hnCache
    { φ := φ', h := s.h, valid := hvalid
      excessCache := pushedCache s u v
      cache_correct := pushedCache_correct s u v hu.1 hr
      past := u :: s.past, todo := us
      nodup := by simpa [ht, Machine.done, List.reverse_cons, List.append_assoc] using s.nodup
      complete := by intro a; simpa [ht, Machine.done, List.reverse_cons, List.append_assoc] using s.complete a
      ordered := by simpa [ht, Machine.done, List.reverse_cons, List.append_assoc] using hord
      quiet := by
        intro a hm
        simp only [List.reverse_cons] at hm
        rcases List.mem_append.mp hm with hm | hm
        · exact hquiet a hm
        · have hau : a = u := List.mem_singleton.mp hm
          subst a
          intro hover
          have hex : φ'.excess u = 0 := by
            dsimp [φ']
            rw [cachedPush_eq, push_excess]
            simp [residualEdge_ne s.φ hr, min_eq_left hn.le]
          have hx := hover.2.2
          rw [hex] at hx
          linarith
      cursor := s.cursor, cursor_bound := s.cursor_bound, skipped := hskip }
    else
    { φ := φ', h := s.h, valid := hvalid
      excessCache := pushedCache s u v
      cache_correct := pushedCache_correct s u v hu.1 hr
      past := s.past, todo := s.todo, nodup := s.nodup, complete := s.complete,
      ordered := hord, quiet := hquiet
      cursor := s.cursor, cursor_bound := s.cursor_bound, skipped := hskip }theorem pushCurrent_φ (s : Machine G) (u : V) (us : List V) (ht : s.todo = u :: us)
    (v : V) (hu : s.φ.isOverflowing u) (hr : s.φ.residualEdge u v)
    (ha : s.h u = s.h v + 1) :
    (pushCurrent s u us ht v hu hr ha).φ = push s.φ u v hu.1 hr := by
  by_cases hn : s.φ.excess u < s.φ.residualCapacity u v <;> simp [pushCurrent, s.cache_correct u hu.1, hn]theorem pushCurrent_h (s : Machine G) (u : V) (us : List V) (ht : s.todo = u :: us)
    (v : V) (hu : s.φ.isOverflowing u) (hr : s.φ.residualEdge u v)
    (ha : s.h u = s.h v + 1) : (pushCurrent s u us ht v hu hr ha).h = s.h := by
  by_cases hn : s.φ.excess u < s.φ.residualCapacity u v <;> simp [pushCurrent, s.cache_correct u hu.1, hn]theorem pushCurrent_done_mono (s : Machine G) (u : V) (us : List V) (ht : s.todo = u :: us)
    (v : V) (hu : s.φ.isOverflowing u) (hr : s.φ.residualEdge u v)
    (ha : s.h u = s.h v + 1) :
    ∀ a ∈ s.done, a ∈ (pushCurrent s u us ht v hu hr ha).done := by
  by_cases hn : s.φ.excess u < s.φ.residualCapacity u v <;> intro a hm
  all_goals simp only [Machine.done, List.mem_reverse] at hm
  all_goals simp [pushCurrent, s.cache_correct u hu.1, hn, Machine.done, hm]theorem pushCurrent_nonsat_done (s : Machine G) (u : V) (us : List V) (ht : s.todo = u :: us)
    (v : V) (hu : s.φ.isOverflowing u) (hr : s.φ.residualEdge u v)
    (ha : s.h u = s.h v + 1) (hn : s.φ.excess u < s.φ.residualCapacity u v) :
    u ∈ (pushCurrent s u us ht v hu hr ha).done := by simp [pushCurrent, s.cache_correct u hu.1, hn, Machine.done]theorem credit_push (s : Machine G) (u : V) (us : List V) (ht : s.todo = u :: us)
    (v : V) (hu : s.φ.isOverflowing u) (hr : s.φ.residualEdge u v)
    (ha : s.h u = s.h v + 1) :
    credit (pushCurrent s u us ht v hu hr ha) ≤ credit s := by
  by_cases hn : s.φ.excess u < s.φ.residualCapacity u v <;> simp [pushCurrent, s.cache_correct u hu.1, hn, credit, ht]

One executed basic operation, including its preceding cursor/list scans.

structure BasicResult (s : Machine G) where
  op : BasicOp V G
  after : Machine G
  beforeφ : op.beforeφ = s.φ
  beforeh : op.beforeh = s.h
  resultφ : op.resultφ = after.φ
  resulth : op.resulth = after.h
  scans : Nat
  moves : Nat
  minimumVisits : Nat
  minimumVisits_eq : minimumVisits = Fintype.card V * (if op.isRelabel then 1 else 0)
  scan_credit : scans + credit after ≤ credit s + 2 * Fintype.card V * (if op.isRelabel then 1 else 0)
  move_bound : moves ≤ 2 * Fintype.card V * (if op.isRelabel then 1 else 0)
  done_mono : op.isRelabel = false → ∀ a ∈ s.done, a ∈ after.done
  nonsat_done : op.isNonsaturatingPush = true → op.opVertex ∈ after.done
  source_fresh : op.opVertex ∉ s.done

noncomputable def relabelResult (s : Machine G) (u : V) (us : List V)
    (ht : s.todo = u :: us) (hu : s.φ.isOverflowing u)
    (hr : ∃ v, s.φ.residualEdge u v)
    (hp : ∀ v, s.φ.residualEdge u v → s.h u ≤ s.h v) : BasicResult s where
  op := .relabel s.φ s.h u hu hr hp
  after := relabelCurrent s u us ht hu hr hp
  beforeφ := rfl
  beforeh := rfl
  resultφ := rfl
  resulth := (scannedRelabel_eq _ _ _ hr).symm
  scans := 0
  moves := (reverseOnto s.past us).2
  minimumVisits := (scanMinimum s.φ s.h u univ.toList).2
  minimumVisits_eq := by simp [BasicOp.isRelabel]
  scan_credit := by simpa [BasicOp.isRelabel] using credit_relabel s u us ht hu hr hp
  move_bound := by
    have hl := List.Nodup.length_le_card s.nodup
    simp only [List.length_append, List.length_reverse] at hl
    simp only [BasicOp.isRelabel, ↓reduceIte, Nat.mul_one, reverseOnto_count]
    omega
  done_mono := by simp [BasicOp.isRelabel]
  nonsat_done := by simp [BasicOp.isNonsaturatingPush]
  source_fresh := current_not_done s ht



noncomputable def pushResult (s : Machine G) (u : V) (us : List V) (ht : s.todo = u :: us)
    (v : V) (hu : s.φ.isOverflowing u) (hr : s.φ.residualEdge u v)
    (ha : s.h u = s.h v + 1) : BasicResult s where
  op := .push s.φ s.h u v hu hr ha
  after := pushCurrent s u us ht v hu hr ha
  beforeφ := rfl
  beforeh := rfl
  resultφ := (pushCurrent_φ s u us ht v hu hr ha).symm
  resulth := (pushCurrent_h s u us ht v hu hr ha).symm
  scans := 0
  moves := 0
  minimumVisits := 0
  minimumVisits_eq := by simp [BasicOp.isRelabel]
  scan_credit := by simpa [BasicOp.isRelabel] using credit_push s u us ht v hu hr ha
  move_bound := by simp
  done_mono := by intro _; exact pushCurrent_done_mono s u us ht v hu hr ha
  nonsat_done := by
    intro hn
    have hn' : s.φ.excess u < s.φ.residualCapacity u v := by
      simpa [BasicOp.isNonsaturatingPush] using hn
    exact pushCurrent_nonsat_done s u us ht v hu hr ha hn'
  source_fresh := current_not_done s ht

Pull a result back across one actual administrative cursor/list step.

noncomputable def BasicResult.prependScan {s t : Machine G}
    (hp : t.φ = s.φ) (hh : t.h = s.h)
    (hd : ∀ a ∈ s.done, a ∈ t.done) (hc : credit t + 1 = credit s)
    (r : BasicResult t) : BasicResult s where
  op := r.op
  after := r.after
  beforeφ := r.beforeφ.trans hp
  beforeh := r.beforeh.trans hh
  resultφ := r.resultφ
  resulth := r.resulth
  scans := r.scans + 1
  moves := r.moves
  minimumVisits := r.minimumVisits
  minimumVisits_eq := r.minimumVisits_eq
  scan_credit := by have h := r.scan_credit; omega
  move_bound := r.move_bound
  done_mono := by intro hn a ha; exact r.done_mono hn a (hd a ha)
  nonsat_done := r.nonsat_done
  source_fresh := by intro hs; exact r.source_fresh (hd _ hs)

              structure Finished (s : Machine G) where
  quiet : ∀ u, ¬ s.φ.isOverflowing u
  scans : Nat
  scan_bound : scans ≤ credit s

noncomputable def Finished.prependScan {s t : Machine G}
    (hp : t.φ = s.φ) (hc : credit t + 1 = credit s) (r : Finished t) : Finished s where
  quiet := by rw [← hp]; exact r.quiet
  scans := r.scans + 1
  scan_bound := by have h := r.scan_bound; omegaabbrev Next (s : Machine G) := Finished s ⊕ BasicResult s

Scan current neighbors and inactive list entries until a basic operation or a completed flow is reached. Administrative steps strictly consume credit.


noncomputable def next (s : Machine G) : Next s :=
  match ht : s.todo with
  | [] => .inl
      { quiet := by
          intro u hu
          have hm : u ∈ s.done ++ s.todo := (s.complete u).2 ⟨hu.1, hu.2.1⟩
          have hd : u ∈ s.done := by simpa [ht] using hm
          exact s.quiet u hd hu
        scans := 0
        scan_bound := Nat.zero_le _ }
  | u :: us =>
      if huCache : 0 < s.excessCache u then
        let hu : s.φ.isOverflowing u := ⟨(current_internal s ht).1, (current_internal s ht).2, by
          simpa [s.cache_correct u (current_internal s ht).1] using huCache⟩
        match hc : s.cursor u with
        | [] =>
            let hr := exists_residualEdge_of_overflowing s.φ u hu.1 hu.2.2
            let hp : ∀ v, s.φ.residualEdge u v → s.h u ≤ s.h v :=
              fun v hv => s.skipped u v (by simp [hc]) hv
            .inr (relabelResult s u us ht hu hr hp)
        | v :: vs =>
            if ha : admissibleEdge s.φ s.h u v then
              .inr (pushResult s u us ht v hu ha.1 ha.2)
            else
              let t := advanceCursor s u v vs hc ha
              match next t with
              | .inl r => .inl (r.prependScan (s := s) (t := t) rfl (credit_advanceCursor s u v vs hc ha))
              | .inr r => .inr (r.prependScan (s := s) (t := t) rfl rfl (fun _ hx => hx)
                  (credit_advanceCursor s u v vs hc ha))
      else
        let hu : ¬ s.φ.isOverflowing u := by
          intro hover; exact huCache (by simpa [s.cache_correct u hover.1] using hover.2.2)
        let t := skipCurrent s u us ht hu
        match next t with
        | .inl r => .inl (r.prependScan (s := s) (t := t) rfl (credit_skip s u us ht hu))
        | .inr r => .inr (r.prependScan (s := s) (t := t) rfl rfl
            (by intro a ha; simpa [Machine.done, t, skipCurrent, or_comm] using List.mem_cons_of_mem u (by simpa [Machine.done] using ha))
            (credit_skip s u us ht hu))
termination_by credit s
 decreasing_by
  · have h := credit_advanceCursor s u v vs hc ha
    omega
  · have h := credit_skip s u us ht hu
    omega

              inductive Trace : Machine G → Machine G → Nat → Type _
  | nil (s : Machine G) : Trace s s 0
  | cons {s t : Machine G} {n : Nat} (r : BasicResult s)
      (tail : Trace r.after t n) : Trace s t (n + 1)namespace Tracenoncomputable def state {s t : Machine G} {n : Nat} (tr : Trace s t n) : Nat → Machine G :=
  match tr with
  | .nil s => fun _ => s
  | .cons r tail => fun i => match i with | 0 => s | k + 1 => tail.state k@[simp] theorem state_zero {s t : Machine G} {n : Nat} (tr : Trace s t n) : tr.state 0 = s := by
  cases tr <;> rfl@[simp] theorem state_end {s t : Machine G} {n : Nat} (tr : Trace s t n) : tr.state n = t := by
  induction tr with
  | nil => rfl
  | cons r tail ih => exact ihnoncomputable def result {s t : Machine G} {n : Nat} (tr : Trace s t n)
    (i : Nat) (hi : i < n) : BasicResult (tr.state i) :=
  match tr with
  | .nil _ => False.elim (by omega)
  | .cons r tail => match i with
      | 0 => r
      | k + 1 => tail.result k (by omega)@[simp] theorem result_after {s t : Machine G} {n : Nat} (tr : Trace s t n)
    (i : Nat) (hi : i < n) : (tr.result i hi).after = tr.state (i + 1) := by
  induction tr generalizing i with
  | nil => omega
  | cons r tail ih =>
      cases i with
      | zero => simp [result, state]
      | succ k => exact ih k (by omega)

noncomputable def toRun {s t : Machine G} {n : Nat} (tr : Trace s t n) : Run V G n where
  φ i := (tr.state i).φ
  h i := (tr.state i).h
  hvalid i := (tr.state i).valid
  op i hi := (tr.result i hi).op
  hop_beforeφ i hi := (tr.result i hi).beforeφ
  hop_beforeh i hi := (tr.result i hi).beforeh
  hop_resultφ i hi := by rw [(tr.result i hi).resultφ, result_after]
  hop_resulth i hi := by rw [(tr.result i hi).resulth, result_after]

theorem done_mono_interval {s t : Machine G} {n : Nat} (tr : Trace s t n)
    {i j : Nat} (hij : i ≤ j) (hj : j ≤ n)
    (hn : ∀ k (hk : k < n), i ≤ k → k < j → (tr.result k hk).op.isRelabel = false) :
    ∀ a ∈ (tr.state i).done, a ∈ (tr.state j).done := by
  induction j with
  | zero =>
      have heq : i = 0 := by omega
      subst i
      exact fun _ h => h
  | succ j ih =>
      by_cases heq : i = j + 1
      · subst i; exact fun _ h => h
      · have hjn : j < n := by omega
        have hmid := ih (by omega) (by omega) (by
          intro k hk hik hkj; exact hn k hk hik (by omega))
        intro a ha
        have h := (tr.result j hjn).done_mono (hn j hjn (by omega) (by omega)) a (hmid a ha)
        simpa using h

noncomputable def toRelabelToFrontRun {s t : Machine G} {n : Nat}
    (tr : Trace s t n) : RelabelToFrontRun V G n where
  run := tr.toRun
  discharge_discipline := by
    intro i j hi hj hij hni _ hnone heq
    have hm := (tr.result i hi).nonsat_done hni
    rw [result_after] at hm
    have hmono := tr.done_mono_interval (i := i + 1) (j := j) (by omega) (by omega)
      (by intro k hk hik hkj; exact hnone k hk (by omega) hkj)
    have hin := hmono _ hm
    have heq' : (tr.result i hi).op.opVertex = (tr.result j hj).op.opVertex := heq
    rw [heq'] at hin
    exact (tr.result j hj).source_fresh hintheorem length_bound {s t : Machine G} {n : Nat} (tr : Trace s t n) :
    n ≤ 9 * Fintype.card V * Fintype.card V * Fintype.card V :=
  tr.toRelabelToFrontRun.step_count_bound_V3noncomputable def scans {s t : Machine G} {n : Nat} : Trace s t n → Nat
  | .nil _ => 0
  | .cons r tail => r.scans + tail.scansnoncomputable def moves {s t : Machine G} {n : Nat} : Trace s t n → Nat
  | .nil _ => 0
  | .cons r tail => r.moves + tail.movesnoncomputable def relabels {s t : Machine G} {n : Nat} : Trace s t n → Nat
  | .nil _ => 0
  | .cons r tail => (if r.op.isRelabel then 1 else 0) + tail.relabelstheorem relabels_eq {s t : Machine G} {n : Nat} (tr : Trace s t n) :
    tr.relabels = tr.toRun.numRelabels := by
  induction tr with
  | nil => simp [relabels, Run.numRelabels]
  | cons r tail ih =>
      simp only [relabels, Run.numRelabels, Fin.sum_univ_succ, Run.opFin, toRun, result]
      congr 1theorem scans_credit {s t : Machine G} {n : Nat} (tr : Trace s t n) :
    tr.scans + credit t ≤ credit s + 2 * Fintype.card V * tr.relabels := by
  induction tr with
  | nil => simp [scans, relabels]
  | cons r tail ih =>
      have h := r.scan_credit
      simp only [scans, relabels, Nat.mul_add]
      omegatheorem moves_bound {s t : Machine G} {n : Nat} (tr : Trace s t n) :
    tr.moves ≤ 2 * Fintype.card V * tr.relabels := by
  induction tr with
  | nil => simp [moves, relabels]
  | cons r tail ih =>
      have h := r.move_bound
      simp only [moves, relabels, Nat.mul_add]
      omeganoncomputable def minimumVisits {s t : Machine G} {n : Nat} : Trace s t n → Nat
  | .nil _ => 0
  | .cons r tail => r.minimumVisits + tail.minimumVisitstheorem minimumVisits_eq {s t : Machine G} {n : Nat} (tr : Trace s t n) :
    tr.minimumVisits = Fintype.card V * tr.relabels := by
  induction tr with
  | nil => simp [minimumVisits, relabels]
  | cons r tail ih => simp [minimumVisits, relabels, r.minimumVisits_eq, ih, Nat.mul_add]end Tracestructure Execution (s : Machine G) (fuel : Nat) where
  last : Machine G
  steps : Nat
  trace : Trace s last steps
  terminal : Option (Finished last)
  exhausted : terminal = none → steps = fuel

noncomputable def execute (s : Machine G) : (fuel : Nat) → Execution s fuel
  | 0 => ⟨s, 0, .nil s, none, fun _ => rfl⟩
  | fuel + 1 => match next s with
      | .inl fin => ⟨s, 0, .nil s, some fin, by simp⟩
      | .inr r =>
          let tail := execute r.after fuel
          { last := tail.last
            steps := tail.steps + 1
            trace := .cons r tail.trace
            terminal := tail.terminal
            exhausted := by intro hn; rw [tail.exhausted hn] }def budget (V : Type*) [Fintype V] := 9 * Fintype.card V * Fintype.card V * Fintype.card V + 1

theorem execute_terminal (s : Machine G) : (execute s (budget V)).terminal ≠ none := by
  intro hn
  have h := (execute s (budget V)).trace.length_bound
  rw [(execute s (budget V)).exhausted hn] at h
  simp only [budget] at h
  omeganoncomputable def completed (s : Machine G) : Finished (execute s (budget V)).last :=
  (execute s (budget V)).terminal.get (Option.isSome_iff_ne_none.mpr (execute_terminal s))theorem completed_excess_zero (s : Machine G) (u : V) (hs : u ≠ G.s) (ht : u ≠ G.t) :
    (execute s (budget V)).last.φ.excess u = 0 := by
  have h := (completed s).quiet u
  have hnonneg := (execute s (budget V)).last.φ.hexcess_nonneg u hs
  by_contra hn
  exact h ⟨hs, ht, lt_of_le_of_ne hnonneg (Ne.symm hn)⟩noncomputable def maximumFlow (s : Machine G) : Flow V G :=
  (execute s (budget V)).last.φ.toFlow (completed_excess_zero s)theorem maximumFlow_isMaximal (s : Machine G) : (maximumFlow s).isMaximal :=
  maximal_of_no_overflow _ _ (execute s (budget V)).last.valid (completed_excess_zero s)noncomputable def initializedFlow (G : FlowNetwork V) : Flow V G := maximumFlow (initialMachine G)theorem initialized_maximum_flow (G : FlowNetwork V) : (initializedFlow G).isMaximal :=
  maximumFlow_isMaximal _

Actual cursor advances/inactive-entry scans, plus terminal scans, list traversal on move-to-front, and a full vertex scan for each relabel. Pushes contribute one basic-operation unit. The scalar/indexed implementation expands these units below.

noncomputable def controllerWork (s : Machine G) : Nat :=
  let r := execute s (budget V)
  r.steps + r.trace.scans + (completed s).scans + r.trace.moves +
    r.trace.minimumVisits



theorem controllerWork_bound (s : Machine G) :
    controllerWork s ≤ 19 * Fintype.card V * Fintype.card V * Fintype.card V + credit s := by
  let r := execute s (budget V)
  have hn := r.trace.length_bound
  have hscan := r.trace.scans_credit
  have hfin := (completed s).scan_bound
  have hmove := r.trace.moves_bound
  have hrel : r.trace.relabels ≤ 2 * Fintype.card V * Fintype.card V := by
    rw [Trace.relabels_eq]; exact r.trace.toRun.relabel_count_bound
  change r.steps + r.trace.scans + (completed s).scans + r.trace.moves +
    r.trace.minimumVisits ≤ _
  rw [Trace.minimumVisits_eq]
  change (completed s).scans ≤ credit r.last at hfin
  nlinarith

theorem initialized_controllerWork_le (G : FlowNetwork V) :
    controllerWork (initialMachine G) ≤ 21 * Fintype.card V * Fintype.card V * Fintype.card V := by
  have h := controllerWork_bound (initialMachine G)
  have hc := credit_initial G
  have hp : 0 < Fintype.card V := Fintype.card_pos_iff.mpr ⟨G.s⟩
  have h1 : Fintype.card V ≤ Fintype.card V * Fintype.card V := Nat.le_mul_self _
  have h2 : Fintype.card V * Fintype.card V ≤ Fintype.card V * Fintype.card V * Fintype.card V :=
    Nat.le_mul_of_pos_right _ hp
  nlinarith

The initialization's actual cell writes and internal-list candidate visits.

noncomputable def initializationWork (G : FlowNetwork V) : Nat :=
  (initialCells G).2 + (tabulate (initialHeight G) 0).2 + (tabulate (G.c G.s) 0).2 +
    (tabulate (fun _ : V => (univ.toList : List V)) []).2 + (selectInternal G univ.toList).2

@[simp] theorem initializationWork_eq (G : FlowNetwork V) :
    initializationWork G = Fintype.card V * Fintype.card V + 4 * Fintype.card V := by
  simp [initializationWork, initialCells, Fintype.card_prod]
  omega

Scalar/indexed RAM charge: a fixed allowance of 32 primitive operations per cursor/list test, push/relabel dispatch, moved list cell, or minimum-scan cell. Indexed table lookup/update and exact real arithmetic are unit primitives. This is not a bound on persistent-function evaluation or machine bit complexity.

noncomputable def Trace.work {s t : Machine G} {n : Nat} : Trace s t n → Nat
  | .nil _ => 0
  | .cons r tail => 32 * (1 + r.scans + r.moves + r.minimumVisits) + tail.work

theorem Trace.work_eq {s t : Machine G} {n : Nat} (tr : Trace s t n) :
    tr.work = 32 * (n + tr.scans + tr.moves + tr.minimumVisits) := by
  induction tr with
  | nil => simp [work, scans, moves, minimumVisits]
  | cons r tail ih => simp only [work, scans, moves, minimumVisits, ih]; omega

The returned measured construction-and-run charge. The last summand includes the actual scans that discover termination and its final empty-list test.

noncomputable def initializedWork (G : FlowNetwork V) : Nat :=
  32 * initializationWork G + (execute (initialMachine G) (budget V)).trace.work +
    32 * ((completed (initialMachine G)).scans + 1)



theorem initializedWork_eq (G : FlowNetwork V) : initializedWork G =
    32 * (initializationWork G + controllerWork (initialMachine G) + 1) := by
  unfold initializedWork controllerWork
  rw [Trace.work_eq]
  dsimp only
  omega



theorem initialized_work_le_cubic (G : FlowNetwork V) :
    initializedWork G ≤ 864 * Fintype.card V * Fintype.card V * Fintype.card V := by
  rw [initializedWork_eq, initializationWork_eq]
  have h := initialized_controllerWork_le G
  have hp : 0 < Fintype.card V := Fintype.card_pos_iff.mpr ⟨G.s⟩
  have h1 : Fintype.card V ≤ Fintype.card V * Fintype.card V := Nat.le_mul_self _
  have h2 : Fintype.card V * Fintype.card V ≤ Fintype.card V * Fintype.card V * Fintype.card V :=
    Nat.le_mul_of_pos_right _ hp
  nlinarith

One concrete initialized run supplies both maximum flow and the cubic charge.

theorem initialized_correct_and_cost (G : FlowNetwork V) :
    (initializedFlow G).isMaximal ∧
      initializedWork G ≤ 864 * Fintype.card V * Fintype.card V * Fintype.card V :=
  ⟨initialized_maximum_flow G, initialized_work_le_cubic G⟩

end CLRS.Chapter26.RelabelExecution