OAI/Combinatorics/CompleteCrossing/Counting.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Cyclic gap enumeration and the exact Harary–Hill crossing-tuple count.

  1. def OAI.Paper170.naturalCrossingTuples line 19
  2. theorem OAI.Paper170.mem_naturalCrossingTuples line 22
  3. theorem OAI.Paper170.naturalCrossingTuples_card line 41
  4. abbrev OAI.Paper170.CyclicRecord line 48
  5. def OAI.Paper170.cyclicRecords line 50
  6. theorem OAI.Paper170.mem_cyclicRecords line 53
  7. def OAI.Paper170.cyclicToOrdered line 60
  8. def OAI.Paper170.orderedToCyclic line 71
  9. theorem OAI.Paper170.residueColor_shift_eq line 79
  10. theorem OAI.Paper170.cyclicToOrdered_spec line 84
  11. theorem OAI.Paper170.orderedToCyclic_bounds line 121
  12. theorem OAI.Paper170.orderedToCyclic_inverse line 128
  13. theorem OAI.Paper170.cyclicToOrdered_inverse line 139
  14. theorem OAI.Paper170.cyclicToOrdered_mem line 147
  15. theorem OAI.Paper170.orderedToCyclic_mem line 155
  16. theorem OAI.Paper170.crossingTuples_cyclic_count line 169
  17. def OAI.Paper170.startingLabels line 197
  18. theorem OAI.Paper170.startingLabels_card_eq_sum line 201
  19. theorem OAI.Paper170.startingLabels_card_odd line 211
  20. theorem OAI.Paper170.startingLabels_card_even line 223
  21. theorem OAI.Paper170.parity_partition line 234
  22. theorem OAI.Paper170.startingLabels_card_even_balanced line 243
  23. theorem OAI.Paper170.sum_parity_weights line 255
  24. theorem OAI.Paper170.startingLabels_sum_odd_gap line 267
  25. theorem OAI.Paper170.sameColorGapTuples_card_eq_sum line 284
  26. theorem OAI.Paper170.sameColorGapTuples_card line 294
  27. theorem OAI.Paper170.crossingTuples_card line 336