OAI/Combinatorics/StripMass/PatchReplacement.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.Patch.glued line 18
  2. def OAI.CriticalStrip.Diagram.Patch.compressed line 27
  3. theorem OAI.CriticalStrip.Diagram.Patch.reach_to_exterior line 35
  4. theorem OAI.CriticalStrip.Diagram.Patch.lift_local_reach line 61
  5. theorem OAI.CriticalStrip.Diagram.Patch.lift_compressed_reach line 65
  6. theorem OAI.CriticalStrip.Diagram.Patch.exterior_reach_iff line 75
  7. theorem OAI.CriticalStrip.Diagram.Patch.interior_reach_iff line 80
  8. def OAI.CriticalStrip.Diagram.Patch.drains line 92
  9. def OAI.CriticalStrip.Diagram.Patch.exteriorOutput line 95
  10. theorem OAI.CriticalStrip.Diagram.Patch.drains_glued_iff line 101
  11. structure OAI.CriticalStrip.Diagram.ConnectivityCertificate line 159
  12. theorem OAI.CriticalStrip.Diagram.ConnectivityCertificate.reaches_root line 170
  13. theorem OAI.CriticalStrip.Diagram.ConnectivityCertificate.reach_root_eq line 183
  14. theorem OAI.CriticalStrip.Diagram.ConnectivityCertificate.reach_symm line 188
  15. theorem OAI.CriticalStrip.Diagram.ConnectivityCertificate.reach_iff line 194
  16. instance OAI.CriticalStrip.Diagram.tileAdjDecidable line 204
  17. instance OAI.CriticalStrip.Diagram.tileOccupiedDecidable line 207
  18. theorem OAI.CriticalStrip.Diagram.Tile.adj_symm line 210
  19. abbrev OAI.CriticalStrip.Diagram.ThreeBox.Config line 226
  20. def OAI.CriticalStrip.Diagram.ThreeBox.row line 228
  21. def OAI.CriticalStrip.Diagram.ThreeBox.port line 229
  22. def OAI.CriticalStrip.Diagram.ThreeBox.atRow line 230
  23. def OAI.CriticalStrip.Diagram.ThreeBox.tileEdge line 232
  24. def OAI.CriticalStrip.Diagram.ThreeBox.wireEdge line 235
  25. def OAI.CriticalStrip.Diagram.ThreeBox.Adj line 237
  26. instance OAI.CriticalStrip.Diagram.ThreeBox.tileEdgeDecidable line 243
  27. instance OAI.CriticalStrip.Diagram.ThreeBox.wireEdgeDecidable line 245
  28. instance OAI.CriticalStrip.Diagram.ThreeBox.adjDecidable line 247
  29. theorem OAI.CriticalStrip.Diagram.ThreeBox.tileEdge_symm line 250
  30. theorem OAI.CriticalStrip.Diagram.ThreeBox.wireEdge_symm line 256
  31. theorem OAI.CriticalStrip.Diagram.ThreeBox.adj_symm line 261
  32. def OAI.CriticalStrip.Diagram.ThreeBox.Compatible line 271
  33. instance OAI.CriticalStrip.Diagram.ThreeBox.compatibleDecidable line 275
  34. def OAI.CriticalStrip.Diagram.ThreeBox.boundary line 279
  35. def OAI.CriticalStrip.Diagram.ThreeBox.boundaryOccupied line 280
  36. instance OAI.CriticalStrip.Diagram.ThreeBox.boundaryOccupiedDecidable line 282
  37. def OAI.CriticalStrip.Diagram.ThreeBox.boundaryAdj line 285
  38. def OAI.CriticalStrip.Diagram.ThreeBox.boundarySupport line 288
  39. structure OAI.CriticalStrip.Diagram.ThreeBox.Realizes line 293