OAI/Combinatorics/ContingencyTables/Transport/ResidualSearch.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The computed residual search and its maximum-flow certificate

The search itself is the deterministic directed BFS. Success supplies the precise shortest simple residual path required by the published augmentation bound; failure supplies a saturated cut, hence maximality.

  1. def OAI.ContingencyTables.ResidualSearch.edge line 23
  2. def OAI.ContingencyTables.ResidualSearch.search line 26
  3. lemma OAI.ContingencyTables.ResidualSearch.route_of_fin line 29
  4. lemma OAI.ContingencyTables.ResidualSearch.route_of_residual line 45
  5. theorem OAI.ContingencyTables.ResidualSearch.search_shortest line 51
  6. def OAI.ContingencyTables.ResidualSearch.reached line 81
  7. lemma OAI.ContingencyTables.ResidualSearch.mem_reached line 84
  8. lemma OAI.ContingencyTables.ResidualSearch.source_reached line 88
  9. lemma OAI.ContingencyTables.ResidualSearch.target_not_reached line 91
  10. lemma OAI.ContingencyTables.ResidualSearch.cut_saturated line 98
  11. lemma OAI.ContingencyTables.ResidualSearch.sum_internal_zero line 109
  12. lemma OAI.ContingencyTables.ResidualSearch.value_eq_cut line 121
  13. theorem OAI.ContingencyTables.ResidualSearch.failure_maximum line 140

    Source documentation

    Failure of the actual finite BFS implies maximum flow. No max-flow/min-cut result is included in the published input.

    theorem failure_maximum (c : Capacity n) (s t : Fin n) (f : Flow n)
    (hf : Feasible c s t f) (h : search c f s t=none) : IsMaximum c s t f := by
…

    Mentions: OAI.ContingencyTables.ResidualSearch.search