OAI/Combinatorics/StripMass/TriplePatch.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.TriplePosition.output line 17
  2. def OAI.CriticalStrip.Diagram.TriplePosition.reachTest line 21
  3. def OAI.CriticalStrip.Diagram.TriplePosition.exteriorPredicate line 24
  4. def OAI.CriticalStrip.Diagram.TriplePosition.patchEquiv line 28
  5. lemma OAI.CriticalStrip.Diagram.TriplePosition.active_iff line 33
  6. lemma OAI.CriticalStrip.Diagram.TriplePosition.compatible_support_iff line 42
  7. lemma OAI.CriticalStrip.Diagram.TriplePosition.patchTest_realizes line 67
  8. lemma OAI.CriticalStrip.Diagram.TriplePosition.eval_patch_iff line 87
  9. lemma OAI.CriticalStrip.Diagram.TriplePosition.eval_profile_iff line 108
  10. def OAI.CriticalStrip.Diagram.Tile.mirrorPort line 125
  11. lemma OAI.CriticalStrip.Diagram.Tile.mirrorPort_involutive line 126
  12. def OAI.CriticalStrip.Diagram.Tile.mirrorPortEquiv line 128
  13. def OAI.CriticalStrip.Diagram.Tile.mirror line 131
  14. lemma OAI.CriticalStrip.Diagram.Tile.mirror_involutive line 142
  15. def OAI.CriticalStrip.Diagram.Tile.mirrorEquiv line 144
  16. lemma OAI.CriticalStrip.Diagram.Tile.mirror_adj line 146
  17. lemma OAI.CriticalStrip.Diagram.Tile.mirror_occupied line 151
  18. lemma OAI.CriticalStrip.Diagram.Tile.weight_mirror line 157
  19. def OAI.CriticalStrip.Diagram.TriplePosition.leftCircuit line 169
  20. def OAI.CriticalStrip.Diagram.TriplePosition.mirrorVertexEquiv line 173
  21. def OAI.CriticalStrip.Diagram.TriplePosition.mirrorWiring line 177
  22. def OAI.CriticalStrip.Diagram.TriplePosition.mirrorBoundary line 185
  23. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_vertex_old line 188
  24. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_vertex_zero line 190
  25. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_vertex_one line 193
  26. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_vertex_two line 196
  27. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_boundary_eq line 200
  28. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_edge_0_0 line 207
  29. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_edge_0_1 line 214
  30. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_edge_0_2 line 225
  31. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_edge_0_3 line 237
  32. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_edge_1_0 line 248
  33. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_edge_1_1 line 259
  34. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_edge_1_2 line 271
  35. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_edge_1_3 line 285
  36. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_edge_2_0 line 298
  37. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_edge_2_1 line 310
  38. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_edge_2_2 line 324
  39. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_edge_2_3 line 336
  40. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_edge_3_0 line 349
  41. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_edge_3_1 line 360
  42. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_edge_3_2 line 373
  43. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_edge_3_3 line 386
  44. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_edge_iff line 398
  45. def OAI.CriticalStrip.Diagram.TriplePosition.mirrorEquiv line 420
  46. instance OAI.CriticalStrip.Diagram.TriplePosition.mirrorWiring_symm line 430
  47. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_boundary_injective line 438
  48. def OAI.CriticalStrip.Diagram.TriplePosition.mirrorSupport line 445
  49. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_circuit_support line 449
  50. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_boundary_used line 455
  51. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_compatible_iff line 466
  52. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_eval_iff line 475