OAI/Combinatorics/StripMass/FiniteEnds.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.PathGraph.reachable_of_odd_terminals line 15
  2. lemma OAI.CriticalStrip.Diagram.PathGraph.degree_eq_one_of_single line 32
  3. lemma OAI.CriticalStrip.Diagram.PathGraph.degree_eq_two_of_two line 42
  4. lemma OAI.CriticalStrip.Diagram.PathGraph.endpoints_connected line 55
  5. lemma OAI.CriticalStrip.Diagram.PathGraph.endpoints_connected_finite_support line 81
  6. lemma OAI.CriticalStrip.Diagram.PathGraph.drains_of_two_terminals line 122
  7. lemma OAI.CriticalStrip.Diagram.Graph.reach_exit line 150
  8. def OAI.CriticalStrip.HoneycombAssignment.restrict line 169
  9. lemma OAI.CriticalStrip.HoneycombAssignment.restrict_tile line 182
  10. lemma OAI.CriticalStrip.HoneycombAssignment.restrict_adj line 186
  11. lemma OAI.CriticalStrip.HoneycombAssignment.up_two line 198
  12. lemma OAI.CriticalStrip.HoneycombAssignment.down_two line 225
  13. lemma OAI.CriticalStrip.HoneycombAssignment.two_interior_top line 251
  14. theorem OAI.CriticalStrip.HoneycombAssignment.restrict_drains_of_two_top line 268
  15. lemma OAI.CriticalStrip.Diagram.ColumnChain.read_map line 327
  16. lemma OAI.CriticalStrip.Diagram.ColumnChain.north_shape_read line 332
  17. lemma OAI.CriticalStrip.SewnRectangle.tile_nonvacant_bounds line 352
  18. lemma OAI.CriticalStrip.SewnRectangle.finite_support line 371
  19. lemma OAI.CriticalStrip.SewnRectangle.restrict_finite_support line 387
  20. lemma OAI.CriticalStrip.SewnRectangle.north_south_occupied line 394