ForestGreedySemantics.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Correctness of the actual binary forest loop

The invariant refers to the adjacency list produced by the program. The final graph is decoded directly from that list. Optimal forests occur only as proof witnesses for the safe-edge invariant.

def OAI.ContingencyTables.ForestGreedySemantics.Catalog line 23
Source documentation
Every stored edge is valid, and every graph edge is stored in at least one orientation with its exact capacity.
```
def Catalog (G : SimpleGraph (Fin n)) (b : Sym2 (Fin n)→ℕ) (es : List Edge) : Prop :=
…
```
lemma OAI.ContingencyTables.ForestGreedySemantics.chosen_spec line 28
lemma OAI.ContingencyTables.ForestGreedySemantics.none_spec line 42
def OAI.ContingencyTables.ForestGreedySemantics.iterate line 55
lemma OAI.ContingencyTables.ForestGreedySemantics.fold_eq_iterate line 59
lemma OAI.ContingencyTables.ForestGreedySemantics.execute_iterate line 65
lemma OAI.ContingencyTables.ForestGreedySemantics.advance_none line 68
lemma OAI.ContingencyTables.ForestGreedySemantics.iterate_none line 71
lemma OAI.ContingencyTables.ForestGreedySemantics.advance_code line 76
def OAI.ContingencyTables.ForestGreedySemantics.edgeCount line 84
lemma OAI.ContingencyTables.ForestGreedySemantics.edgeCount_le line 86
lemma OAI.ContingencyTables.ForestGreedySemantics.card_add line 89

theorem OAI.ContingencyTables.ForestGreedySemantics.iterate_optimal line 101

Source documentation

A fuel count at least the number of missing unordered edges suffices for the executed loop, without any tie-breaking assumption.

theorem iterate_optimal (G T : SimpleGraph (Fin n)) (b : Sym2 (Fin n)→ℕ)
    (es : List Edge) (hC : Catalog G b es) (hb : ∀ e∈G.edgeSet,0<b e)
    (hT : Extendible G T b) (k : ℕ)
    (hbudget : Fintype.card (Sym2 (Fin n))≤edgeCount T+k) :
    ∃ F : SimpleGraph (Fin n),iterate k (graphCode T,es)=(graphCode F,es) ∧
      F≤G ∧ F.IsAcyclic ∧
        ∀ H : SimpleGraph (Fin n),H≤G → H.IsAcyclic → weight H b≤weight F b := by
…

Mentions: OAI.ContingencyTables.ForestGreedySemantics.Catalog, OAI.ContingencyTables.ForestGreedySemantics.edgeCount, OAI.ContingencyTables.ForestGreedySemantics.iterate

def OAI.ContingencyTables.ForestGreedySemantics.decoded line 132
lemma OAI.ContingencyTables.ForestGreedySemantics.decoded_graphCode line 137
lemma OAI.ContingencyTables.ForestGreedySemantics.unordered_pair_budget line 146
theorem OAI.ContingencyTables.ForestGreedySemantics.execute_optimal line 155
Source documentation
The graph is decoded from the literal result list, not selected from an existence proof.
```
theorem execute_optimal (G T : SimpleGraph (Fin n)) (b : Sym2 (Fin n)→ℕ)
    (es : List Edge) (hC : Catalog G b es) (hb : ∀ e∈G.edgeSet,0<b e)
    (hT : Extendible G T b) :
    let F := decoded (execute (graphCode T,es)).1
…
```
Mentions: OAI.ContingencyTables.ForestGreedySemantics.Catalog, OAI.ContingencyTables.ForestGreedySemantics.decoded