OAI/Algebra/DepthFive/IsolatedFlip.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Canonical removal of isolated positions in an independent set.

The value true denotes the D type from the manuscript. The set S contains the positions allowed to flip (interior V layers), and R a b means that b is a neighbor of a. Independence is the only property of the path graph needed for the fiber calculation.

  1. def OAI.Problem335.IsolatedFlip.eligible line 22
  2. def OAI.Problem335.IsolatedFlip.flip line 26
  3. def OAI.Problem335.IsolatedFlip.unset line 30
  4. def OAI.Problem335.IsolatedFlip.removed line 33
  5. theorem OAI.Problem335.IsolatedFlip.mem_eligible line 37
  6. theorem OAI.Problem335.IsolatedFlip.eligible_subset line 44
  7. theorem OAI.Problem335.IsolatedFlip.flip_eq_of_not_mem line 49
  8. theorem OAI.Problem335.IsolatedFlip.eligible_congr line 55
  9. theorem OAI.Problem335.IsolatedFlip.eligible_flip line 73
  10. theorem OAI.Problem335.IsolatedFlip.flip_idempotent line 80
  11. theorem OAI.Problem335.IsolatedFlip.eligible_unset line 88
  12. theorem OAI.Problem335.IsolatedFlip.flip_unset line 97
  13. theorem OAI.Problem335.IsolatedFlip.removed_subset line 112
  14. theorem OAI.Problem335.IsolatedFlip.unset_flip_removed line 118
  15. theorem OAI.Problem335.IsolatedFlip.removed_unset line 126
  16. def OAI.Problem335.IsolatedFlip.fiberEquiv line 146
  17. theorem OAI.Problem335.IsolatedFlip.fiber_card line 166
  18. theorem OAI.Problem335.IsolatedFlip.fiber_sum_pow line 176
  19. theorem OAI.Problem335.IsolatedFlip.fiber_weight_sum line 194
  20. theorem OAI.Problem335.IsolatedFlip.total_weight_sum line 210
  21. theorem OAI.Problem335.IsolatedFlip.correction_removal line 237