OAI/Combinatorics/ContingencyTables/Machines/NetworkTableProgram.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Extracting the bounded table from the executed flow

The output reads the row-to-column arcs of the computed flow. Both the matrix dimensions and the encoded entries are obtained from the input; there is no choice of a mathematical witness in the program.

  1. abbrev OAI.ContingencyTables.NetworkTableProgram.Prepared line 17
  2. abbrev OAI.ContingencyTables.NetworkTableProgram.CellInput line 18
  3. def OAI.ContingencyTables.NetworkTableProgram.cell line 20
  4. def OAI.ContingencyTables.NetworkTableProgram.cellRealizer line 24
  5. lemma OAI.ContingencyTables.NetworkTableProgram.polynomial_cell line 43
  6. def OAI.ContingencyTables.NetworkTableProgram.rowIndices line 60
  7. def OAI.ContingencyTables.NetworkTableProgram.columnIndices line 61
  8. def OAI.ContingencyTables.NetworkTableProgram.rowIndicesRealizer line 63
  9. def OAI.ContingencyTables.NetworkTableProgram.columnIndicesRealizer line 66
  10. lemma OAI.ContingencyTables.NetworkTableProgram.polynomial_rowIndices line 69
  11. lemma OAI.ContingencyTables.NetworkTableProgram.polynomial_columnIndices line 77
  12. def OAI.ContingencyTables.NetworkTableProgram.row line 85
  13. def OAI.ContingencyTables.NetworkTableProgram.rowRealizer line 88
  14. lemma OAI.ContingencyTables.NetworkTableProgram.polynomial_row line 94
  15. def OAI.ContingencyTables.NetworkTableProgram.table line 102
  16. def OAI.ContingencyTables.NetworkTableProgram.tableRealizer line 105
  17. lemma OAI.ContingencyTables.NetworkTableProgram.polynomial_table line 108
  18. def OAI.ContingencyTables.NetworkTableProgram.prepare line 112
  19. def OAI.ContingencyTables.NetworkTableProgram.prepareRealizer line 115
  20. lemma OAI.ContingencyTables.NetworkTableProgram.polynomial_prepare line 118
  21. def OAI.ContingencyTables.NetworkTableProgram.output line 121
  22. def OAI.ContingencyTables.NetworkTableProgram.outputRealizer line 122
  23. lemma OAI.ContingencyTables.NetworkTableProgram.polynomial_output line 123
  24. lemma OAI.ContingencyTables.NetworkTableProgram.signedParts_toNat line 126
  25. lemma OAI.ContingencyTables.NetworkTableProgram.cell_code line 130
  26. lemma OAI.ContingencyTables.NetworkTableProgram.output_code line 148
  27. theorem OAI.ContingencyTables.NetworkTableProgram.output_correct line 161

    Source documentation

    The computed list output encodes a table with the supplied margins and bounds whenever the concrete feasibility test accepts.

    theorem output_correct {m n : ℕ} (hEK : PublishedEdmondsKarp.EdmondsKarp1972Theorem1)
    (r : Fin m→ℕ) (c : Fin n→ℕ) (b : Fin m→Fin n→ℕ)
    (ht : NetworkFeasibilityProgram.test (data r c b)=true) :
    ∃ X, output (data r c b)=natCode X ∧ HasMargins X r c ∧ ∀ i j,X i j≤b i j := by
…

    Mentions: OAI.ContingencyTables.PublishedEdmondsKarp.EdmondsKarp1972Theorem1, OAI.ContingencyTables.NetworkFeasibilityProgram.test, OAI.ContingencyTables.NetworkTableProgram.output, OAI.ContingencyTables.HasMargins