structure SimpleGraph.HopcroftKarpExecution {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) : Type (max u (w + 1))

• numPhases : ℕ
• matching : Fin (self.numPhases + 1) → G.Subgraph
• isMatching (i : Fin (self.numPhases + 1)) : (self.matching i).IsMatching
• isFinalMaximum (M' : G.Subgraph) : M'.IsMatching → M'.edgeSet.ncard ≤ (self.matching ⟨self.numPhases, ⋯⟩).edgeSet.ncard
• size_strictly_increases (i : Fin self.numPhases) : (self.matching ⟨↑i, ⋯⟩).edgeSet.ncard < (self.matching ⟨↑i + 1, ⋯⟩).edgeSet.ncard
• shortestLen : Fin self.numPhases → ℕ
• shortestLen_spec (i : Fin self.numPhases) : G.shortestAugPathLength (self.matching ⟨↑i, ⋯⟩) = ↑(self.shortestLen i)
• paths (i : Fin self.numPhases) : G.VertexDisjointAugPaths (self.matching ⟨↑i, ⋯⟩) (self.shortestLen i)
• paths_maximal (i : Fin self.numPhases) : (self.paths i).IsMaximal
• isAugmentation (i : Fin self.numPhases) : IsAugmentationAlongPaths (self.matching ⟨↑i, ⋯⟩) (self.matching ⟨↑i + 1, ⋯⟩) (self.paths i)

theorem SimpleGraph.HopcroftKarpExecution.shortestLen_strict_mono {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} (exec : G.HopcroftKarpExecution) (i : Fin exec.numPhases) (hi : ↑i + 1 < exec.numPhases) : exec.shortestLen i < exec.shortestLen ⟨↑i + 1, hi⟩

theorem SimpleGraph.HopcroftKarpExecution.shortestLen_odd {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} (exec : G.HopcroftKarpExecution) (i : Fin exec.numPhases) : Odd (exec.shortestLen i)

theorem SimpleGraph.HopcroftKarpExecution.shortestLen_lower_bound {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} (exec : G.HopcroftKarpExecution) (i : Fin exec.numPhases) : 2 * ↑i + 1 ≤ exec.shortestLen i

theorem SimpleGraph.deficit_bound_from_shortest_aug_path {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} (M : G.Subgraph) (hM : M.IsMatching) (ℓ : ℕ) (hℓ : ∀ (u v : V) (p : G.Walk u v), p.IsAugmentingPath M → ℓ ≤ p.length) (M' : G.Subgraph) (hM' : M'.IsMatching) : M'.edgeSet.ncard ≤ M.edgeSet.ncard + Fintype.card V / (ℓ + 1)

theorem SimpleGraph.HopcroftKarpExecution.matching_size_growth {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} (exec : G.HopcroftKarpExecution) (i j : ℕ) (hij : i ≤ j) (hj : j ≤ exec.numPhases) : (exec.matching ⟨i, ⋯⟩).edgeSet.ncard + (j - i) ≤ (exec.matching ⟨j, ⋯⟩).edgeSet.ncard

theorem SimpleGraph.hopcroft_karp_deficit_after_sqrt_phases {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} (exec : G.HopcroftKarpExecution) (hphases : (Fintype.card V).sqrt ≤ exec.numPhases) (M' : G.Subgraph) : M'.IsMatching → M'.edgeSet.ncard ≤ (exec.matching ⟨(Fintype.card V).sqrt, ⋯⟩).edgeSet.ncard + (Fintype.card V).sqrt

theorem SimpleGraph.hopcroft_karp_phase_bound {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} (exec : G.HopcroftKarpExecution) : exec.numPhases ≤ 2 * (Fintype.card V).sqrt + 1