OAI/Combinatorics/StripMass/HoneycombClip.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.turnRow line 15
  2. lemma OAI.CriticalStrip.turnRow_involutive line 17
  3. def OAI.CriticalStrip.turnCell line 25
  4. lemma OAI.CriticalStrip.Diagram.Tile.turn_nonvacant line 32
  5. def OAI.CriticalStrip.HoneycombAssignment.weight line 38
  6. lemma OAI.CriticalStrip.HoneycombAssignment.turn_tile_all line 41
  7. lemma OAI.CriticalStrip.HoneycombAssignment.turn_weight line 48
  8. lemma OAI.CriticalStrip.HoneycombAssignment.turn_tileSupport line 53
  9. def OAI.CriticalStrip.HoneycombAssignment.Fits line 60
  10. lemma OAI.CriticalStrip.HoneycombAssignment.Fits.mono line 63
  11. lemma OAI.CriticalStrip.HoneycombAssignment.exists_fits line 69
  12. lemma OAI.CriticalStrip.HoneycombAssignment.Fits.vacant_left line 79
  13. lemma OAI.CriticalStrip.HoneycombAssignment.Fits.vacant_right line 85
  14. def OAI.CriticalStrip.HoneycombAssignment.leftClip line 91
  15. def OAI.CriticalStrip.HoneycombAssignment.rightClip line 94
  16. lemma OAI.CriticalStrip.HoneycombAssignment.read_leftClip line 97
  17. lemma OAI.CriticalStrip.HoneycombAssignment.read_rightClip line 104
  18. lemma OAI.CriticalStrip.HoneycombAssignment.sewn_clips line 112
  19. lemma OAI.CriticalStrip.HoneycombAssignment.clips_compatible line 122
  20. lemma OAI.CriticalStrip.TopArchConfiguration.tileSupport_finite line 164
  21. lemma OAI.CriticalStrip.TopArchConfiguration.extend_fits line 172
  22. lemma OAI.CriticalStrip.TopArchConfiguration.weight_toArch line 192
  23. lemma OAI.CriticalStrip.Diagram.Graph.glued_reach_right_boundary line 209
  24. lemma OAI.CriticalStrip.Diagram.Graph.glued_drainsAt_halves line 229
  25. lemma OAI.CriticalStrip.HoneycombAssignment.clip_occupancies line 245
  26. lemma OAI.CriticalStrip.HoneycombAssignment.clips_runs_glues line 263
  27. lemma OAI.CriticalStrip.TopArchConfiguration.extend_clips_runs line 295
  28. def OAI.CriticalStrip.SewnRectangle.leftWeights line 327
  29. def OAI.CriticalStrip.SewnRectangle.rightWeights line 330
  30. lemma OAI.CriticalStrip.SewnRectangle.north_row_tile line 333
  31. lemma OAI.CriticalStrip.SewnRectangle.runs_cut line 347
  32. def OAI.CriticalStrip.SewnRectangle.northAssignment line 359
  33. lemma OAI.CriticalStrip.SewnRectangle.northAssignment_drains line 369
  34. def OAI.CriticalStrip.SewnRectangle.northArch line 386
  35. lemma OAI.CriticalStrip.SewnRectangle.northArch_extend line 416
  36. lemma OAI.CriticalStrip.Diagram.ColumnChain.weight_ofFn line 448
  37. def OAI.CriticalStrip.windowCell line 457
  38. lemma OAI.CriticalStrip.windowCell_injective line 461
  39. lemma OAI.CriticalStrip.windowCell_range line 470
  40. lemma OAI.CriticalStrip.HoneycombAssignment.weight_window line 487
  41. lemma OAI.CriticalStrip.HoneycombAssignment.physical_tile_weight_ne_zero line 508
  42. lemma OAI.CriticalStrip.TopArchConfiguration.extend_left_north_weight line 520
  43. lemma OAI.CriticalStrip.TopArchConfiguration.extend_right_north_weight line 527
  44. lemma OAI.CriticalStrip.TopArchConfiguration.leftClip_weight line 534
  45. lemma OAI.CriticalStrip.TopArchConfiguration.rightClip_weight line 550
  46. lemma OAI.CriticalStrip.TopArchConfiguration.clips_weight line 568
  47. lemma OAI.CriticalStrip.TopArchConfiguration.clips_weight_ne_zero line 576