OAI/Combinatorics/ContingencyTables/Machines/FiniteGraphRootProgram.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

A binary list program computing a component root

The graph is supplied by adjacency lists. The program makes one growth round per stored vertex, then minimizes the reached indices. No loop depends on the numeric size of an index or of an edge capacity.

  1. abbrev OAI.ContingencyTables.FiniteGraphRootProgram.GraphCode line 21
  2. abbrev OAI.ContingencyTables.FiniteGraphRootProgram.SearchState line 22
  3. abbrev OAI.ContingencyTables.FiniteGraphRootProgram.Input line 23
  4. def OAI.ContingencyTables.FiniteGraphRootProgram.indices line 25
  5. def OAI.ContingencyTables.FiniteGraphRootProgram.indicesRealizer line 27
  6. lemma OAI.ContingencyTables.FiniteGraphRootProgram.polynomial_indices line 29
  7. def OAI.ContingencyTables.FiniteGraphRootProgram.neighborHit line 34
  8. def OAI.ContingencyTables.FiniteGraphRootProgram.neighborHitRealizer line 37
  9. lemma OAI.ContingencyTables.FiniteGraphRootProgram.polynomial_neighborHit line 42
  10. def OAI.ContingencyTables.FiniteGraphRootProgram.growTest line 46
  11. def OAI.ContingencyTables.FiniteGraphRootProgram.growTestRealizer line 49
  12. lemma OAI.ContingencyTables.FiniteGraphRootProgram.polynomial_growTest line 58
  13. def OAI.ContingencyTables.FiniteGraphRootProgram.grow line 69
  14. def OAI.ContingencyTables.FiniteGraphRootProgram.growRealizer line 72
  15. lemma OAI.ContingencyTables.FiniteGraphRootProgram.polynomial_grow line 76
  16. def OAI.ContingencyTables.FiniteGraphRootProgram.advance line 81
  17. def OAI.ContingencyTables.FiniteGraphRootProgram.advanceRealizer line 84
  18. lemma OAI.ContingencyTables.FiniteGraphRootProgram.polynomial_advance line 88
  19. lemma OAI.ContingencyTables.FiniteGraphRootProgram.fold_first line 92
  20. lemma OAI.ContingencyTables.FiniteGraphRootProgram.grow_weight line 98
  21. lemma OAI.ContingencyTables.FiniteGraphRootProgram.fold_weight line 101
  22. lemma OAI.ContingencyTables.FiniteGraphRootProgram.indices_weight line 111
  23. lemma OAI.ContingencyTables.FiniteGraphRootProgram.polynomial_searchFold line 121
  24. def OAI.ContingencyTables.FiniteGraphRootProgram.prepare line 146
  25. def OAI.ContingencyTables.FiniteGraphRootProgram.prepareRealizer line 148
  26. lemma OAI.ContingencyTables.FiniteGraphRootProgram.polynomial_prepare line 151
  27. def OAI.ContingencyTables.FiniteGraphRootProgram.run line 156
  28. def OAI.ContingencyTables.FiniteGraphRootProgram.runRealizer line 159
  29. lemma OAI.ContingencyTables.FiniteGraphRootProgram.polynomial_run line 161
  30. def OAI.ContingencyTables.FiniteGraphRootProgram.reached line 164
  31. def OAI.ContingencyTables.FiniteGraphRootProgram.reachedRealizer line 166
  32. theorem OAI.ContingencyTables.FiniteGraphRootProgram.polynomial_reached line 169
  33. lemma OAI.ContingencyTables.FiniteGraphRootProgram.minimum_fold_le line 172
  34. lemma OAI.ContingencyTables.FiniteGraphRootProgram.polynomial_minimumFold line 178
  35. def OAI.ContingencyTables.FiniteGraphRootProgram.rootCode line 187
  36. def OAI.ContingencyTables.FiniteGraphRootProgram.rootCodeRealizer line 190
  37. theorem OAI.ContingencyTables.FiniteGraphRootProgram.polynomial_rootCode line 195