MaximumForestExchange.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The safe-edge invariant for the executed maximum-forest algorithm

At every step, choose a largest-capacity edge whose endpoints lie in different current components. It extends the current forest inside a maximum-weight forest. This is the exchange proof behind the binary component-search implementation; no forest is enumerated by that program.

lemma OAI.ContingencyTables.MaximumForestExchange.adj_of_reachable_of_acyclic line 23
Source documentation
In an acyclic supergraph, an edge between vertices already joined by the subgraph must itself belong to that subgraph.
```
lemma adj_of_reachable_of_acyclic {T F : SimpleGraph V} (hTF : T≤F)
    (hF : F.IsAcyclic) {u v : V} (hr : T.Reachable u v) (hf : F.Adj u v) : T.Adj u v := by
…
```
lemma OAI.ContingencyTables.MaximumForestExchange.path_crosses line 33
Source documentation
Every path between different current components contains an edge between different current components.
```
lemma path_crosses {T F : SimpleGraph V} {u v : V} (p : F.Walk u v)
    (hn : ¬T.Reachable u v) :
    ∃ a b,F.Adj a b ∧ s(a,b)∈p.edges ∧ ¬T.Reachable a b := by
…
```
lemma OAI.ContingencyTables.MaximumForestExchange.weight_delete line 44
def OAI.ContingencyTables.MaximumForestExchange.Extendible line 54
Source documentation
The current forest is contained in some globally optimal forest.
```
def Extendible (G T : SimpleGraph V) (b : Sym2 V→ℕ) : Prop :=
…
```
lemma OAI.ContingencyTables.MaximumForestExchange.bottom_extendible line 58

theorem OAI.ContingencyTables.MaximumForestExchange.safe_edge line 64

Source documentation

A greatest edge joining two current components is safe. The argument uses a maximum forest only as a witness for the invariant.

theorem safe_edge (G T : SimpleGraph V) (b : Sym2 V→ℕ)
    (hb : ∀ e∈G.edgeSet,0<b e) (hT : Extendible G T b)
    {u v : V} (he : G.Adj u v) (hn : ¬T.Reachable u v)
    (hbest : ∀ a d,G.Adj a d → ¬T.Reachable a d → b s(a,d)≤b s(u,v)) :
    Extendible G (T⊔edge u v) b := by
…

Mentions: OAI.ContingencyTables.MaximumForestExchange.Extendible

theorem OAI.ContingencyTables.MaximumForestExchange.finished line 109
Source documentation
Once no edge joins different current components, the invariant certifies global optimality of the current forest.
```
theorem finished (G T : SimpleGraph V) (b : Sym2 V→ℕ)
    (hT : Extendible G T b)
    (hn : ∀ u v,G.Adj u v → T.Reachable u v) :
    T≤G ∧ T.IsAcyclic ∧
      ∀ H : SimpleGraph V,H≤G → H.IsAcyclic → weight H b≤weight T b := by
…
```
Mentions: OAI.ContingencyTables.MaximumForestExchange.Extendible