OAI/Combinatorics/StripMass/TopPadding.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.Diagram.realizes_padTop_iff line 12
  2. theorem OAI.CriticalStrip.Diagram.Tile.vacant_of_three_top line 86
  3. theorem OAI.CriticalStrip.Diagram.Realizes.top_vacant line 90
  4. theorem OAI.CriticalStrip.Diagram.realizes_snoc_top_iff line 96
  5. theorem OAI.CriticalStrip.Diagram.column_padTop line 108
  6. theorem OAI.CriticalStrip.Diagram.Tile.deletion_zero_of_north_vacant_east_occupied line 129
  7. theorem OAI.CriticalStrip.Diagram.Tile.identity_zero_of_north_vacant_west_occupied line 135
  8. theorem OAI.CriticalStrip.Diagram.column_deletion_top_row line 141
  9. theorem OAI.CriticalStrip.Diagram.column_identity_top_col line 154
  10. def OAI.CriticalStrip.Diagram.Pairing.nonemptyPadTop line 169
  11. def OAI.CriticalStrip.Diagram.Pairing.nonemptyTopVacantEquiv line 172
  12. abbrev OAI.CriticalStrip.Diagram.Pairing.TopOccupiedNonempty line 183
  13. def OAI.CriticalStrip.Diagram.Pairing.nonemptyTopSplit line 186
  14. theorem OAI.CriticalStrip.Diagram.Pairing.nonemptyTopSplit_inl line 192
  15. theorem OAI.CriticalStrip.Diagram.Pairing.nonemptyTopSplit_inr line 195
  16. theorem OAI.CriticalStrip.Diagram.det_flat_top line 201
  17. theorem OAI.CriticalStrip.Diagram.Pairing.eq_empty_of_le_one line 226
  18. theorem OAI.CriticalStrip.Diagram.det_column_le_one line 237
  19. def OAI.CriticalStrip.Diagram.Weights.IsFlat line 242
  20. theorem OAI.CriticalStrip.Diagram.det_one_nonflat line 247
  21. theorem OAI.CriticalStrip.Diagram.vacuumRegular_one_nonflat line 271
  22. theorem OAI.CriticalStrip.Diagram.inlinePrivate0_sin_two_lambda line 282
  23. theorem OAI.CriticalStrip.Diagram.inlinePrivate0_sin_two_lambda_pos line 288
  24. theorem OAI.CriticalStrip.Diagram.inlinePrivate0_sin_three_lambda_pos line 291
  25. theorem OAI.CriticalStrip.Diagram.physicalWeights_zero line 295
  26. theorem OAI.CriticalStrip.Diagram.physicalWeights_three_lambda line 306
  27. theorem OAI.CriticalStrip.Diagram.physical_simultaneous_regular line 324
  28. def OAI.CriticalStrip.Diagram.attachEmpty line 340
  29. theorem OAI.CriticalStrip.Diagram.attachEmpty_empty line 345
  30. theorem OAI.CriticalStrip.Diagram.attachEmpty_nonempty line 349
  31. def OAI.CriticalStrip.Diagram.injectionColumn line 353
  32. def OAI.CriticalStrip.Diagram.normalizedVacuum line 357
  33. def OAI.CriticalStrip.Diagram.IsNormalizedStationary line 361
  34. theorem OAI.CriticalStrip.Diagram.column_mulVec_empty line 365
  35. theorem OAI.CriticalStrip.Diagram.column_mulVec_nonempty line 371
  36. theorem OAI.CriticalStrip.Diagram.normalizedVacuum_stationary line 378
  37. theorem OAI.CriticalStrip.Diagram.normalizedVacuum_unique line 402
  38. def OAI.CriticalStrip.Diagram.rawColumn line 432