OAI/Combinatorics/StripMass/BottomPadding.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.Diagram.realizes_padBottom_iff line 12
  2. theorem OAI.CriticalStrip.Diagram.Tile.vacant_of_three line 86
  3. theorem OAI.CriticalStrip.Diagram.Realizes.bottom_vacant line 90
  4. theorem OAI.CriticalStrip.Diagram.realizes_cons_bottom_iff line 96
  5. theorem OAI.CriticalStrip.Diagram.column_padBottom line 109
  6. theorem OAI.CriticalStrip.Diagram.Tile.identity_zero_of_south_vacant_east_occupied line 129
  7. theorem OAI.CriticalStrip.Diagram.Tile.deletion_zero_of_south_vacant_west_occupied line 135
  8. theorem OAI.CriticalStrip.Diagram.column_identity_bottom_row line 142
  9. theorem OAI.CriticalStrip.Diagram.column_deletion_bottom_col line 156
  10. def OAI.CriticalStrip.Diagram.Pairing.nonemptyPadBottom line 171
  11. def OAI.CriticalStrip.Diagram.Pairing.nonemptyBottomVacantEquiv line 174
  12. abbrev OAI.CriticalStrip.Diagram.Pairing.BottomOccupiedNonempty line 185
  13. def OAI.CriticalStrip.Diagram.Pairing.nonemptyBottomSplit line 188
  14. theorem OAI.CriticalStrip.Diagram.Pairing.nonemptyBottomSplit_inl line 194
  15. theorem OAI.CriticalStrip.Diagram.Pairing.nonemptyBottomSplit_inr line 197
  16. theorem OAI.CriticalStrip.Diagram.det_one_sub_zero_rows line 203
  17. theorem OAI.CriticalStrip.Diagram.det_one_sub_zero_cols line 215
  18. theorem OAI.CriticalStrip.Diagram.det_flat_bottom line 227
  19. def OAI.CriticalStrip.Diagram.Pairing.padTop line 254
  20. theorem OAI.CriticalStrip.Diagram.Pairing.padTop_adj_castSucc line 256
  21. theorem OAI.CriticalStrip.Diagram.Pairing.padTop_not_adj_last line 259
  22. theorem OAI.CriticalStrip.Diagram.Pairing.padTop_not_adj_last' line 264
  23. theorem OAI.CriticalStrip.Diagram.Pairing.padTop_not_occupied_last line 269
  24. theorem OAI.CriticalStrip.Diagram.Pairing.padTop_occupied_castSucc line 272
  25. theorem OAI.CriticalStrip.Diagram.Pairing.padTop_empty line 277
  26. theorem OAI.CriticalStrip.Diagram.Pairing.padTop_eq_empty line 282
  27. theorem OAI.CriticalStrip.Diagram.Pairing.padTop_restrict line 287
  28. def OAI.CriticalStrip.Diagram.Configuration.padTop line 308
  29. theorem OAI.CriticalStrip.Diagram.Configuration.padTop_last line 310
  30. theorem OAI.CriticalStrip.Diagram.Configuration.padTop_castSucc line 312
  31. def OAI.CriticalStrip.Diagram.vertexCastSucc line 317
  32. theorem OAI.CriticalStrip.Diagram.vertexCastSucc_injective line 319
  33. theorem OAI.CriticalStrip.Diagram.wiring_padTop_last line 326
  34. theorem OAI.CriticalStrip.Diagram.wiring_padTop_last_right line 342
  35. theorem OAI.CriticalStrip.Diagram.wiring_padTop_iff line 348
  36. theorem OAI.CriticalStrip.Diagram.reach_padTop_image line 353
  37. theorem OAI.CriticalStrip.Diagram.reach_padTop_iff line 367
  38. theorem OAI.CriticalStrip.Diagram.reach_padTop_last_iff line 378
  39. theorem OAI.CriticalStrip.Diagram.reach_padTop_last_right_iff line 383