OAI/Combinatorics/ContingencyTables/Rooted/ForestJoinProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Canonical adjacency-list insertion of a forest edge

Every row is rebuilt from the stored vertex range. This keeps the graph encoding canonical and bounds all intermediate lists by the vertex count.

  1. abbrev OAI.ContingencyTables.ForestJoinProgram.Input line 16
  2. abbrev OAI.ContingencyTables.ForestJoinProgram.RowInput line 17
  3. abbrev OAI.ContingencyTables.ForestJoinProgram.TestInput line 18
  4. def OAI.ContingencyTables.ForestJoinProgram.keep line 20
  5. def OAI.ContingencyTables.ForestJoinProgram.keepRealizer line 25
  6. lemma OAI.ContingencyTables.ForestJoinProgram.polynomial_keep line 42
  7. def OAI.ContingencyTables.ForestJoinProgram.vertices line 71
  8. def OAI.ContingencyTables.ForestJoinProgram.verticesRealizer line 72
  9. lemma OAI.ContingencyTables.ForestJoinProgram.polynomial_vertices line 74
  10. def OAI.ContingencyTables.ForestJoinProgram.row line 77
  11. def OAI.ContingencyTables.ForestJoinProgram.rowRealizer line 78
  12. lemma OAI.ContingencyTables.ForestJoinProgram.polynomial_row line 80
  13. def OAI.ContingencyTables.ForestJoinProgram.join line 84
  14. def OAI.ContingencyTables.ForestJoinProgram.joinRealizer line 85
  15. lemma OAI.ContingencyTables.ForestJoinProgram.polynomial_join line 87
  16. lemma OAI.ContingencyTables.ForestJoinProgram.join_length line 92
  17. lemma OAI.ContingencyTables.ForestJoinProgram.row_weight line 95
  18. lemma OAI.ContingencyTables.ForestJoinProgram.join_weight line 98
  19. lemma OAI.ContingencyTables.ForestJoinProgram.keep_code line 108
  20. lemma OAI.ContingencyTables.ForestJoinProgram.join_code line 132