OAI/Combinatorics/StripMass/PhysicalStationarity.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.angleScalar line 16
  2. def OAI.CriticalStrip.Diagram.angleVacuum line 21
  3. def OAI.CriticalStrip.Diagram.angleNorthSource line 24
  4. lemma OAI.CriticalStrip.Diagram.rationalAt_angle_vacuum line 27
  5. lemma OAI.CriticalStrip.Diagram.rationalAt_angle_column line 36
  6. lemma OAI.CriticalStrip.Diagram.angle_rawVacuum_stationary line 46
  7. lemma OAI.CriticalStrip.Diagram.angleVacuum_empty line 58
  8. lemma OAI.CriticalStrip.Diagram.angleVacuum_stationary line 63
  9. lemma OAI.CriticalStrip.Diagram.angleVacuum_restricted_stationary line 72
  10. lemma OAI.CriticalStrip.Diagram.continuous_angleScalar line 82
  11. lemma OAI.CriticalStrip.Diagram.continuousOn_angleVacuum line 85
  12. lemma OAI.CriticalStrip.Diagram.continuousOn_angleNorthSource line 93
  13. lemma OAI.CriticalStrip.Diagram.rationalAt_lastCoefficient line 105
  14. lemma OAI.CriticalStrip.Diagram.rationalAt_angle_sourceTransfer line 117
  15. lemma OAI.CriticalStrip.Diagram.rationalAt_angle_northSource line 128
  16. lemma OAI.CriticalStrip.Diagram.polynomialNorthSource_rational_equation line 139
  17. lemma OAI.CriticalStrip.Diagram.angle_rawNorthSource_equation line 158
  18. lemma OAI.CriticalStrip.Diagram.angleNorthSource_stationary line 183
  19. structure OAI.CriticalStrip.Diagram.Pairing.ArcAddition line 204
  20. lemma OAI.CriticalStrip.Diagram.Pairing.ArcAddition.occupied line 210
  21. lemma OAI.CriticalStrip.Diagram.Pairing.ArcAddition.old line 216
  22. lemma OAI.CriticalStrip.Diagram.Pairing.ArcAddition.arc line 220
  23. def OAI.CriticalStrip.Diagram.arcColumn line 227
  24. lemma OAI.CriticalStrip.Diagram.ArcColumn.at_a line 237
  25. lemma OAI.CriticalStrip.Diagram.ArcColumn.at_b line 238
  26. lemma OAI.CriticalStrip.Diagram.ArcColumn.at_inside line 240
  27. lemma OAI.CriticalStrip.Diagram.ArcColumn.at_old line 242
  28. lemma OAI.CriticalStrip.Diagram.ArcColumn.west line 248
  29. lemma OAI.CriticalStrip.Diagram.ArcColumn.east line 255
  30. lemma OAI.CriticalStrip.Diagram.ArcColumn.south line 263
  31. lemma OAI.CriticalStrip.Diagram.ArcColumn.north line 268
  32. lemma OAI.CriticalStrip.Diagram.ArcColumn.tile_edge line 274
  33. lemma OAI.CriticalStrip.Diagram.ArcColumn.reach_north line 277
  34. lemma OAI.CriticalStrip.Diagram.ArcColumn.reach_south line 294
  35. lemma OAI.CriticalStrip.Diagram.ArcColumn.reach_arc line 303
  36. lemma OAI.CriticalStrip.Diagram.ArcColumn.reach_old line 306
  37. def OAI.CriticalStrip.Diagram.ArcColumn.label line 310
  38. lemma OAI.CriticalStrip.Diagram.ArcColumn.edge_label line 312
  39. lemma OAI.CriticalStrip.Diagram.ArcColumn.reach_label line 340
  40. lemma OAI.CriticalStrip.Diagram.ArcColumn.no_loop line 351
  41. lemma OAI.CriticalStrip.Diagram.ArcColumn.realizes line 390
  42. lemma OAI.CriticalStrip.Diagram.Pairing.exists_arcAddition line 420
  43. def OAI.CriticalStrip.Diagram.ColumnNonnegative line 478
  44. lemma OAI.CriticalStrip.Diagram.ColumnNonnegative.column line 482
  45. lemma OAI.CriticalStrip.Diagram.ColumnNonnegative.restricted line 491
  46. lemma OAI.CriticalStrip.Diagram.ColumnNonnegative.injection line 495
  47. lemma OAI.CriticalStrip.Diagram.arcColumn_weight_pos line 499
  48. lemma OAI.CriticalStrip.Diagram.column_arc_pos line 516
  49. theorem OAI.CriticalStrip.Diagram.column_accessible line 531