OAI/Combinatorics/ContingencyTables/Transport/FiniteGraphRootSemantics.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Exact correctness of the finite component-root program

The stored adjacency list is identified with the given finite graph. Each list growth round is the proved finite reachability growth, and the final binary minimum is the least vertex of the actual component.

  1. def OAI.ContingencyTables.FiniteGraphRootProgram.adjacencyRow line 18
  2. def OAI.ContingencyTables.FiniteGraphRootProgram.graphCode line 21
  3. lemma OAI.ContingencyTables.FiniteGraphRootProgram.graphCode_length line 23
  4. lemma OAI.ContingencyTables.FiniteGraphRootProgram.graphCode_getD line 25
  5. lemma OAI.ContingencyTables.FiniteGraphRootProgram.adjacencyRow_mem line 29
  6. lemma OAI.ContingencyTables.FiniteGraphRootProgram.grow_mem line 39
  7. lemma OAI.ContingencyTables.FiniteGraphRootProgram.grow_bound line 54
  8. lemma OAI.ContingencyTables.FiniteGraphRootProgram.fold_advance line 58
  9. lemma OAI.ContingencyTables.FiniteGraphRootProgram.iterate_mem line 68
  10. lemma OAI.ContingencyTables.FiniteGraphRootProgram.iterate_bound line 81
  11. lemma OAI.ContingencyTables.FiniteGraphRootProgram.reached_eq_iterate line 93
  12. theorem OAI.ContingencyTables.FiniteGraphRootProgram.reached_mem_iff line 98
  13. lemma OAI.ContingencyTables.FiniteGraphRootProgram.reached_bound line 103
  14. lemma OAI.ContingencyTables.FiniteGraphRootProgram.minimum_fold_le_of_mem line 107
  15. lemma OAI.ContingencyTables.FiniteGraphRootProgram.le_minimum_fold line 118
  16. theorem OAI.ContingencyTables.FiniteGraphRootProgram.rootCode_eq line 128

    Source documentation

    The executed least root agrees with the explicit mathematical selector. It does not identify that selector with a quotient choice.

    theorem rootCode_eq (v : Fin n) :
    rootCode (graphCode G,v.val)=(FiniteGraphRoots.root G v).val := by
…

    Mentions: OAI.ContingencyTables.FiniteGraphRootProgram.rootCode, OAI.ContingencyTables.FiniteGraphRootProgram.graphCode, OAI.ContingencyTables.FiniteGraphRoots.root