OAI/Combinatorics/StripMass/BridgeUnfold.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.raiseTriangle line 15
  2. lemma OAI.CriticalStrip.raiseTriangle_injective line 17
  3. lemma OAI.CriticalStrip.adjacent_raise line 22
  4. lemma OAI.CriticalStrip.PathBetween.raise line 26
  5. lemma OAI.CriticalStrip.PathBetween.prepend_vertex line 37
  6. def OAI.CriticalStrip.prepareBridge line 55
  7. lemma OAI.CriticalStrip.prepareBridge_injective line 58
  8. lemma OAI.CriticalStrip.prepareBridge_spec line 62
  9. lemma OAI.CriticalStrip.prepareBridge_length line 83
  10. lemma OAI.CriticalStrip.adjacent_up_other_column line 86
  11. lemma OAI.CriticalStrip.exists_rightmost_down line 94
  12. def OAI.CriticalStrip.ladderVertex line 157
  13. lemma OAI.CriticalStrip.ladderVertex_injective line 159
  14. lemma OAI.CriticalStrip.ladderVertex_adjacent line 169
  15. lemma OAI.CriticalStrip.exists_column_connector line 180
  16. lemma OAI.CriticalStrip.PathBetween.append line 225
  17. lemma OAI.CriticalStrip.PathBetween.split line 245
  18. structure OAI.CriticalStrip.BridgeCut line 267
  19. lemma OAI.CriticalStrip.exists_bridgeCut line 280
  20. lemma OAI.CriticalStrip.BridgeCut.height_pos line 293
  21. lemma OAI.CriticalStrip.BridgeCut.end_le line 295
  22. lemma OAI.CriticalStrip.BridgeCut.right_ne_nil line 298
  23. def OAI.CriticalStrip.BridgeCut.move line 306
  24. lemma OAI.CriticalStrip.BridgeCut.move_col line 309
  25. lemma OAI.CriticalStrip.BridgeCut.move_injective line 312
  26. lemma OAI.CriticalStrip.BridgeCut.moved_path line 315
  27. lemma OAI.CriticalStrip.BridgeCut.moved_ge line 326
  28. lemma OAI.CriticalStrip.BridgeCut.connector_exists line 333
  29. def OAI.CriticalStrip.BridgeCut.connector line 340
  30. lemma OAI.CriticalStrip.BridgeCut.connector_spec line 342
  31. def OAI.CriticalStrip.BridgeCut.arch line 347
  32. lemma OAI.CriticalStrip.BridgeCut.arch_path line 349
  33. lemma OAI.CriticalStrip.BridgeCut.arch_length line 370
  34. lemma OAI.CriticalStrip.BridgeCut.arch_filter_left line 380
  35. lemma OAI.CriticalStrip.BridgeCut.arch_filter_right line 398
  36. lemma OAI.CriticalStrip.BridgeCut.recover line 423
  37. def OAI.CriticalStrip.BridgePath line 437
  38. def OAI.CriticalStrip.BridgePath.cut line 442
  39. def OAI.CriticalStrip.BridgePath.toCutArch line 450
  40. lemma OAI.CriticalStrip.BridgePath.toCutArch_injective line 454
  41. lemma OAI.CriticalStrip.BridgePath.toCutArch_path line 476
  42. lemma OAI.CriticalStrip.BridgePath.rho_le_one line 490
  43. lemma OAI.CriticalStrip.BridgePath.toCutArch_weight_bound line 492
  44. theorem OAI.CriticalStrip.BridgePath.summable_weight line 505
  45. theorem OAI.CriticalStrip.summable_bridgeWeight line 514
  46. theorem OAI.CriticalStrip.stripSumsFinite line 528